数学の基礎

　本稿では、等号 = を持つ古典論理 (LK) に従う理論で、定項 0 と１変項関数記号 s の他に、いくつかの関数記号 f_ι ( ι = 1 ,¼, λ ) を持ち、次のsequent群：

(A8-1)  x' = 0  ®

(A8-2)  x' = y'  ®  x = y

(A8-3)ι     ®   fι(0, u ,¼, v) = Sι

(A8-4)ι     ®   fι(x', u ,¼, v) = ( fι(x, u ,¼, v) | y)Tι

も始式として許し、更に次の推論規則：

( 帰納法 )

A , R(x) ® R(sx) , B —————————–   ( x¢A , B )  A , R(0) ® R(T ) , B

を持つ推論体系 T  を考え、これをPeano算術とよびます。ただし sT を T ' とも表わし、S_ι と T_ι は、関数記号 f_ι , f_ι+1 ,¼, f_λ を含まず、u ,¼, v （ T_ι についてはこれらに加えて x , y ）以外に変数を含まない、ある項を表わします。
　なお、ゼロ個以上の s を並べて最後に 0 を書いた s¼s0 という形の項を数字とよぶことにします。

　さて、(A8-3)_ι と (A8-4)_ι は、各関数 f_ι が帰納的関数であることを意味しています。ところで加法 + と乗法 · は帰納的関数であり、逆に付録５の結果により帰納的関数はすべてHeyting算術で扱えるので、Peano算術はHeyting算術に排中律を追加した理論とみなせることがわかります。
　ただし、Heyting算術では、帰納的関数の中にι量化記号を通じて量化記号が含まれていたり、例えば不等号 < も量化記号を含んだ命題の省略記号であったりするわけですが、本節の定義によるPeano算術では、帰納的関数を表わす関数記号には量化記号が含まれておらず、不等式 x < y も、引き算 - を帰納的な定義式 (A5-60) で定義して、その引き算を用いて表わした命題 x' - y = 0 の省略記号であるとみなせば、量化記号を含まない命題として定義することができます。

　さて、本節では、Peano算術では、次のメタ定理：

(A8-5)

T  において、変数も論理記号も含まないsequent S が証明できたときは、S は論理記号の推論規則も ( 帰納法 ) も使わずに証明できる。

が成り立つことを証明します。

　その第１ステップとして、まず閉項、すなわち変数を含まない項 T に対して、その計算値とよぶ数字 ν_T というものを、T に現れる f_ι の添字 ι の最大値 κ について順に、以下のように定義していきます。
　まず κ が 0 すなわち T の中に f_ι が全く含まれない場合は、関数記号は 0 と s のみしか含まれないので、T は数字です。ゆえにこの場合は T 自身をもって ν_T の定義とします。
　次に、ι < κ であるような添字 ι を持つ f_ι のみを含む項 T に対しては ν_T が既に定義されているものとして、f_κ を含み、ι > κ であるような添字 ι を持った f_ι を含まない項 T に対する ν_T を次のようにして定義します。
　T の標準的構成手続き（付録１参照）において、f_κ を含む一番最初の項は f_κ(W, U ,¼, V ) の形をしていて、各項 W, U ,¼, V には ι ³ κ であるような添字 ι を持つ f_ι は含まれません。
　ゆえに、これらに対する計算値 ν_W , ν_U ,¼, ν_V は既に定義できています。
　また、S_ι の u ,¼, v をそれぞれ ν_U ,¼, ν_V で置き換えて得られる項は、ι ³ κ であるような添字 ι を持つ f_ι を含まないので、この項に対する計算値 μ₀ は既に定義されています。以下帰納的に μ_k に次のように定義していきます。
　T_ι の x , y , u ,¼, v をそれぞれ 「k「 , μ_k , ν_U ,¼, ν_V で置き換えて得られる項も、やはり ι ³ κ であるような添字 ι を持つ f_ι を含まないので、この項に対する計算値も既に定義されているので、この計算値をもって μ_k+1 の定義とします。ただし 「k「 は自然数 k に対応する数字です（付録６参照）。
　そこで、T に対し、T に含まれる f_κ(W, U ,¼, V ) の部分を一斉に、「k「 が ν_W と同じ数字になるような自然数 k に対する数字 μ_k で置き換えた項を φ(T ) と書くことにします。
　T に現れる関数記号 f_κ の個数を n とすると、φ(T ) に現れる関数記号 f_κ の個数は n 未満ですから、ある i £ k に対して φ⁽ⁱ⁾(T ) は 関数記号 f_κ を含まず、従ってこれに対する計算値は既に定義されているので、この計算値をもって ν_T と定義することにします。

　さて、以上で閉項 T に対応する計算値 ν_T は定義できましたが、このとき、上記の構築の各ステップから明らかなように、

(A8-6)     ® T = νT

が、構造に関する推論規則のみを使って（従って当然 ( 帰納法 ) も使わずに）証明できます。

　さて、T  では、論理記号を含まない命題はすべて S = T の形をしているので、このような命題を等式とよぶことにします。このとき

(A8-7)

一般の命題 P に対する始式 P ® P は、すべて等式に対するこの形の始式から ( 換 ) と論理記号に関する推論規則のみによって導くことができる。

が成り立つことを証明しましょう。
　そのためには、P ® P' が証明可能なら Ø P' ® Ø P と "xP ® "xP' と $xP ® $xP' が、それぞれ Ø と " と $ の論理記号に関する推論規則のみによって証明できること、更に加えて Q ® Q' が証明可能なら P Ù Q ® P' Ù Q' と P Ú Q ® P' Ú Q' と P' Þ Q ® P Þ Q' がそれぞれ Ù と Ú と Þ の論理記号に関する推論規則のみによって証明できることを示せば十分です。
　まず P ® P' に (Ø 右) を適用すれば ® Ø P, P' が得られ、これに (換 右) と (Ø 左) を適用すれば Ø P' ® Ø P が得られます。
　また P ® P' に (" 左) を適用すれば "xP ® P' が得られ、これに (" 右) を適用すれば "xP ® "xP' が得られます。対称性により $xP ® $xP' も得られます。
　また P ® P' に (Ù 左) を適用すれば P Ù Q ® P' が得られ、同様に Q ® Q' に (Ù 左) を適用すれば P Ù Q ® Q' が得られますが、この両者に (Ù 右) を適用すれば P Ù Q ® P' Ù Q' が得られます。対称性により P Ú Q ® P' Ú Q' も得られます。
　最後に P ® P' と Q ® Q' に (Þ 左) を適用すれば P, P' Þ Q ® Q' が得られますが、これに (換 左) と (Þ 右) を適用すれば P' Þ Q ® P Þ Q' が得られます。

　さて、(A8-5) の証明に移ります。

　まず (A8-7) により、sequent S が証明可能なら、登場する P ® P の形の始式はすべて P が等式であるような S の証明文が存在することがわかります。ゆえに、今後は証明文といえば、このような証明文のみを考えることにします。ゆえに始式には論理記号が含まれないと仮定してよいことがわかります。

　次に、sequent S の証明文が与えられたとき、不要なsequentを削除したり同じsequentの列をコピーすることにより、終式 S 以外のどのsequentも、そのあとに出てくる唯一つのsequentの導出に用いられてるようにすることができます。このような証明文を証明樹とよびますが、証明樹に現れる各sequentには、それが始式でない限り、そのsequentを導出するのに用いた１個又は２個のsequentが指定できますが、この（これらの）sequentをもとのsequentの親とよび、S ' が S " の親であるとき S " は S ' の子であるといいます。
　また、証明樹に現れるsequent S ' に対し、それ自身を S ' の 0代の祖先、S ' の n 代の祖先の親を n+1 代の祖先とよび、ある n に対する S ' の n 代の祖先を、単に S ' の祖先といいます。S ' が S " の祖先であるとき S " は S ' の子孫であるといいます。

　sequent S ' が付録３の推論規則の一覧表の中の推論規則又は ( 帰納法 ) の下段であるとき、S ' の親はその推論規則の上段の形のsequentになりますが、S ' を構成する各命題 R の親とよぶ命題を次のように定義します。
　まず R が下段のsequentの A の中の左から i 番目の命題のときは、R の親は上段のsequentの A の中の左から i 番目の命題とします。A のかわりに B , C , D であっても同様です。
　また、R が ( 減 ) 又は ( 換 ) の下段のsequentの P と書かれた命題なら、R の親は上段のsequentの P と書かれた命題とします。P のかわりに Q の場合も同様です。
　また、R が ( 代 入 ) の下段のsequentの (T | x)A の中の左から i 番目の命題のときは、R の親は上段のsequentの A の中の左から i 番目の命題とします。A のかわりに B であっても同様です。
　R が上記以外の命題のときは、R の親は存在しません。
　命題の場合にも、親の逆の概念を子とよび、何代か前の親を祖先、何代か後の子を子孫とよびます。

　推論規則 ( 切 断 ) の副部（＝固有部分）の命題に含まれる論理記号の個数をこの ( 切 断 ) の次数とよびます。
　また、( 帰納法 ) に出てくる命題 R(T ) をこの ( 帰納法 ) の主部とよび、この主部の命題に含まれる論理記号の個数をこの ( 帰納法 ) の次数といいます。
　考えている証明樹に現れるsequent S ' に対し、その子孫を上段に持つような ( 切 断 ) 又は ( 帰納法 ) の次数のうちで最大のものを、このsequent S ' の高さといいます。

　与えられたsequent S の証明樹を構成する各sequent S ' に対し、その高さを n とするとき、以下の手順により順序数を順次対応させていきます。
　S ' が始式（従って論理記号は含まれない）のときは、順序数 1 を対応させる。
　S ' が、それより手前にある、順序数 α と高さ m を持つsequent S " から ( 帰納法 ) により得られた場合は、順序数 « ω · α »_m-n を対応させる。
　S ' が、それより手前にある、それぞれ順序数 α と β を持ち、共通の高さ m を持つsequent S₁ と S ₂ から ( 切 断 ) により得られた場合は、順序数 « α + β »_m-n を対応させる。
　S ' が、それより手前にある、順序数 α を持つsequent S " から ( 帰納法 ) や ( 切 断 ) 以外の推論規則により得られた場合は、順序数 α を対応させる。
　S ' が、それより手前にある、それぞれ順序数 α と β を持つsequent S₁ と S ₂ から ( 帰納法 ) や ( 切 断 ) 以外の推論規則により得られた場合は、順序数 α + β を対応させる。

　こうして次々に順序数を対応させていったとき、終式 S に対応させられた順序数のことを、この証明樹の順序数とよびます。

　以下、変数も論理記号も含まないsequent S に対し、「順序数 α を持つ S の証明樹が存在すれば、S は論理記号の推論規則も ( 帰納法 ) も使わずに証明できる。」という主張を P (α) と書いたとき、[P] が成り立つことを証明します。
　そこで、「順序数 α より小さい順序数を持つ S の証明文があれば、論理記号の推論規則も ( 帰納法 ) も使わない S の証明が存在する」と仮定して、P を順序数 α を持つ S の証明文とするとき、論理記号の推論規則も ( 帰納法 ) も使わない S の証明が存在することを示すことにします。

　まず、P の中で、ある ( 切 断 ) の副部の命題又は終式の中のある命題が、ある ( 帰納法 ) の主部である命題 R(T ) の子孫になっている場合を考えます。

（　作成中　）