数学の基礎

　数学理論はすべて命題と呼ばれる文字列によって記述されます。したがって、まず命題とはどういう文字列のことなのかということをきちんと定義しなければなりません。
　そこで、まず最初に、文字列の構成要素である文字について、これを次の a ~ f のいずれかのことであると定義します：

1. 　変数と呼ばれる文字。通常はラテン文字やギリシャ文字が使われますが、それらにいくつかダッシュを付けたものも使われます。いずれにせよいくら文字列を書いても、そこに現われない新しい変数があるということが本質です（このことを“変数は無限に用意されている”ということにします）。
   
   
2. 　文字 £。
   
   
3. 　関数記号と呼ばれるいくつかの文字。それぞれの関数記号には引数の個数というものが決まっていて、ゼロの場合もありうるものとします（ゼロの場合を定項と呼ぶこともあります）。
   
   
4. 　述語記号と呼ばれるいくつかの文字。それぞれの述語記号にも引数の個数というものが決まっていて、ゼロの場合もありうるものとします。
   
   
5. 　論理接続詞と呼ばれるいくつかの文字。それぞれの論理接続詞にも引数の個数というものが決まっていて、ゼロの場合もありうるものとします。
   
   
6. 　量化記号と呼ばれるいくつかの文字。これらは、項型と呼ばれるものと命題型と呼ばれるものの２種類があり、そのそれぞれに対し、引数が項であるものと命題であるものがあります。

　 変数と £ 以外の文字を記号、論理接続詞と量化記号を総称して論理記号といいます。また、文字をいくつか並べ、それらのうちいくつかの文字同士を鎖とよばれる線で結んだものを文字列とよびます。また、引数の個数が n の記号は n変項であるともいいます。
　更に、文字列のうち、変数、関数記号、項型量化記号のいずれかで始まるものを項型文字列とよび、述語記号、論理接続詞、命題型量化記号のいずれかで始まるものを命題型文字列とよぶことにします。

　また、κ を量化記号、x を変数、S を文字列とするとき、まず κ と S を順に並べた文字列 κS を作り、S の中の x をすべて冒頭の κ と鎖で結んでから、文字 x をすべて £ で置き換えて得られる文字列を κxS と表すことにします。この文字列には変数 x は現れていません。
　通常の定義では κ ，x ，S をただ並べた文字列を考え、x を束縛変数と呼ぶのですが、あとで式の代入という操作を考える際に、束縛変数という概念があると、煩わしい制約条件を課さなければならず、これを避けるため、Bourbakiに従ってこのようなテクニックを用います。
　とはいっても、現実に数学の理論を文字列によって記述する際は、文字列 κxS を鎖を用いて正直に表現することはありません。この鎖を使うという定義は、あくまで文字列に関する議論（超数学）を行なう際に煩わしさを避けるための方便に過ぎません。なお、鎖はどの文字とどの文字を結んでいるかだけが問題なので、鎖に“形状”の違い（例えばカドの有無等）があっても、他の要素が同じ文字列は同一の文字列とみなします。

　さて、文字列からなる列は、その構成要素である各文字列 S が次のいずれかの条件を満たすとき論理式の構成手続きといいます：

1. 　S は変数である。
   
   
2. 　S は、それより手前に現れる項型文字列 T₁ ,¼, T_n を n変項の関数記号 f に続けて並べて得られる文字列 f T₁¼T_n である。
   
   
3. 　S は、それより手前に現れる項型文字列 T₁ ,¼, T_n を n変項の述語記号 p に続けて並べて得られる文字列 pT₁¼T_n である。
   
   
4. 　S は、それより手前に現れる命題型文字列 P₁ ,¼, P_n を n変項の論理接続詞 s に続けて並べて得られる文字列 sP₁¼P_n である。
   
   
5. 　S は、それより手前に現れる項型文字列 T と、引数が項であるような量化記号 κ と変数 x から得られる文字列 κxT である。
   
   
6. 　S は、それより手前に現れる命題型文字列 P と、引数が命題であるような量化記号 κ と変数 x から得られる文字列 κxP である。
   
   

　論理式の構成手続きの構成要素になることができる文字列を論理式とよび、項（命題）型文字列であるような論理式を項（命題）とよびます。

　上の定義は、記号を式の頭に置くポーランド式と呼ばれている流儀を採用しており、これだと括弧を用いる必要がありません。ただこの記法で実際に数学を記述すると、式が見難いものとなってしまうので、現実には例えば f T₁¼T_n と書くかわりに括弧やカンマを用いて f(T₁ ,¼, T_n ) と書いたり、引数が2個の場合は例えば sPQ と書くかわりに、2つの文字列の途中に記号を置いて (P) s (Q) のように書いたり、更に紛れのない場合は P s Q のように書いたりします。
　ただ、論理式に関する議論（超数学）を行なうときは、括弧の概念がない方が議論しやすいので、以下では項や命題は本来ポーランド式で書かれているものとして議論を展開することにします。

　上記の定義から明らかに、以下の主張が成立します：

(1-1a)   変数1個からなる文字列は項である。

(1-1b)   n変項の関数記号 f に続けてn個の項 T1 ,¼, Tn を並べた文字列 f T1¼Tn は項である。

(1-1c)   n変項の述語記号 p に続けてn個の項 T1 ,¼, Tn を並べた文字列 pT1¼Tn は命題である。

(1-1d)   n変項の論理接続詞 s に続けてn個の命題 P1 ,¼, Pn を並べた文字列 sP1¼Pn は命題である。

(1-1e)   τ を引数が項（命題）であるような項型の量化記号、x を変数、S を項（命題）とするとき、τxS は項である。

(1-1f)   π を引数が項（命題）であるような命題型の量化記号、x を変数、S を項（命題）とするとき、πxS は命題である。

　x を変数、S , T を文字列とするとき、S の中の x のところを一斉に T で置き換えて得られる文字列を (T | x)S と書き、S の x に T を代入した文字列 とよぶことにします。x が S に現れなければ、明らかに (T | x)S は S 自身です。

　さて、C を論理式の構成手続きとし、x を変数、y を C に現れない変数とするとき、C の x を一斉に y に置き換えて得られる文字列の列 ( y | x)C はやはり論理式の構成手続きです。
　実際、C の各構成要素 S に対し、( y | x)S を S' と書くとき、これが上の A~F のいずれかを満たすことを順に確かめていきます。
　まず S が変数 z なら S' は y 又は z ですから、やはり変数です。
　次に、S が引数の個数がnの関数記号、述語記号又は論理接続詞 λ と、C で S より手前に現れる論理式 S₁ ,¼, S_n を並べて得られる λS₁¼S_n ならば、S' は λS'₁¼S'_n です。
　最後に S が量化記号 κ と変数 z と C で S より手前に現れる論理式 U による κzU である場合を考えます。
　もし z が x なら、S には x が現れないので S' は S 自身であり、これは κyU' とも書くことができます。
　また z が x でなくかつ y なら、仮定により y が U に現れないので S は κU であり、従って S' は κU' で、x が U' に現れないことから、これは κxU' とも書くことができます。
　最後に z が x でも y でもなければ、S' は κzU' です。
　以上で主張は確かめられました。
　なお、上記のような変数の置き換えを退避変換と呼ぶことにしましょう。

　この結果を用いて、S を論理式とするとき、変数 x を項 T で置き換えた (T | x)S がやはり論理式であることを示すことができます。
　実際、C を論理式の構成手続き、S をその任意の構成要素とし、C に、T に現れない変数への退避変換を何回か（0回でもよい）施したものを C ' とするとき、その S に対応する構成要素 S' から作った (T | x)S' が必ず論理式になることを、各構成要素 S について順に確かめていきます。
　まず、S が変数なら、S' も変数ですからそれを y とすると、(T | x)S' は y 又は T で、従って項です。
　次に、S が引数の個数がnの関数記号、述語記号又は論理接続詞 λ と、C で S より手前に現れる論理式 S₁ ,¼, S_n を並べて得られる λS₁¼S_n ならば、S' は λS'₁¼S'_n です。ゆえに (T | x)S'_i を S"_i と書けば、(T | x)S' は λS"₁¼S"_n で、従ってこれは論理式です。
　最後に S が量化記号 κ と変数 y と C で S より手前に現れる論理式 U による κyU である場合は、S' はある変数 z により κzU' と書けます。
　このとき、C にも T にも現れず、上記の退避変換に登場する変数とも x とも異なる変数 u を取ると、(u | z)U' は C ' から更に変数 z を u に退避変換して得られる C " の U に対応する文字列であり、U は C で S より手前に現れる文字列ですから、仮定により (u | z)U' の x を T に置き換えた文字列 (T | x)(u | z)U' は論理式です。ゆえにそれに量化記号を付けた κu(T | x)(u | z)U' すなわち (T | x)κzU' すなわち (T | x)S' は論理式です。
　以上で S が項（命題）なら (T | x)S も項（命題）であることが確かめられました。

　次に推論とよばれるプロセスを定義します。
　P₁ ,¼, P_n と R を命題とするとき（ただし n は 0 でもよい）、これらをカンマと記号 ® で繋げて得られる文字列 P₁ ,¼, P_n ® R をsequentとよび、その ® の左側にある命題群を仮定、右側にある命題 R を結論といいます。また、各sequentに対し、その仮定の中に現れる変数を定数といい、現れない変数を自由変数といいます。

　さて、sequentを推論規則とよばれる規則に従って並べたものを証明文とよび、記号と推論規則の一式を与えたものを理論といいます。また、ある理論における証明文に現れることができるsequentを、その理論の定理といい、その任意の証明文を、そのsequentの証明といいます。

　そこで、推論規則の具体例を提示しましょう。次の推論規則は構造に関する推論規則とよばれているもので、これらの推論規則を持つ理論を論理的な理論とよぶことにします：

( 同 一 )	証明文に既に書かれているsequentと同じsequentを証明文の最後に追加することができる。
( 仮 定 )	結論が仮定の中に現れている任意のsequentは、証明文の最後に追加することができる。
( 増 )	証明文に既に書かれているsequentの仮定に任意の命題を追加して得られるsequentを証明文の最後に追加することができる。
( 減 )	証明文に既に書かれているsequentの仮定に同一の命題が２回以上現れているとき、その中の一つを削除したsequentを証明文の最後に追加することができる。
( 換 )	証明文に既に書かれているsequentの仮定の中の任意の２つの命題を入れ替えたsequentを証明文の最後に追加することができる。
( 切 断 )	ある命題群 P1 ,¼, Pn を仮定にもち、Q を結論に持つsequentと、最初の命題群に Q を追加した仮定を持ち、R を結論に持つsequentが共に証明文に書かれているとき、最初の命題群を仮定に持ち、R を結論に持つsequentを証明文の最後に追加することができる。
( 代 入 )	証明文に既に書かれているsequentのある変数を一斉にある項で置き換えたsequentを、同証明文の最後に追加することができる。

　上記の推論規則は言葉で書かれているのでわかりにくい面もあります。そこで、推論規則を図式で表した推論図というものを導入しましょう。
　これは、横線を一本引き、その上にいくつかのsequentを並べ、横線の下に一個のsequentを書いたもので、横線の上を上段、横線の下を下段とよびますが、“上段のsequentがすべて証明文に現れている場合は、下段のsequentを最後に付け加えることができる”という意味の推論規則を表すものです。この推論図を使って上記の構造に関する推論規則を書き下すと、次のようになります：

( 同 一 )	Γ ® P ———– Γ ® P
( 仮 定 )	Γ, P ® P
( 増 )	Γ ® Q ————– Γ, P ® Q
( 減 )	Γ, P, P ® Q —————– Γ, P ® Q
( 換 )	Γ, P, Δ, Q, Θ ® R ———————— Γ, Q, Δ, P, Θ ® R
( 切 断 )	Γ ® P Γ, P ® Q ————– Γ ® Q
( 代 入 )	Γ ® P ———————— (T | x)Γ ® (T | x)P

　ただし、P , Q , R はいずれも任意の命題を、T は任意の項を、x は任意の変数を、Γ , Δ , Θ はいずれも複数の命題（空でもよい）をカンマで区切って並べたものを表します。また、２番目の ( 仮 定 ) は、上段が空なので、横線を省略しました。
　さて、( 同 一 ) は、「一度正しくなった定理はずっと正しいままである」ことを意味し、( 仮 定 ) は、「正しいと仮定した命題は正しい」ことを意味し、( 増 ) は「正しい定理は仮定を追加しても正しい」ことを意味し、( 減 ) は「同じ仮定を２個以上置いても同じことである」ことを意味し、( 換 ) は「仮定は順序に関係ない」ことを意味し、( 切 断 ) は「既に正しいとわかった命題は仮定に追加してもかまわない」ことを意味し、( 代 入 ) は「定理の変数を任意の項で置き換えてもやはり正しい」ことを意味していますから、内容的にはいずれも“自明”な推論規則であるといえます。
　事実、sequent や変数という概念と、それらに対する上記の推論規則は、形式化の原理ともいうべき指導原理によって“導出”することができます（付録２参照）。

　さて、次に具体的な論理記号と、その論理記号に関する推論規則を導入することにします。

　最初は引数の個数が 2 の論理接続詞 Ù で、ÙPQ のかわりに P Ù Q と書くことにし、これに関する推論規則は以下のとおりです：

( Ù 導入)	Γ ® P Γ ® Q —————– Γ ® P Ù Q
( Ù 消去)	Γ ® P Ù Q —————– Γ ® P	Γ ® P Ù Q —————– Γ ® Q

　次は、引数の個数が 2 の論理接続詞 Ú で、ÚPQ のかわりに P Ú Q と書くことにし、これに関する推論規則は以下のとおりです：

( Ú 導入)	Γ ® P —————– Γ ® P Ú Q	Γ ® Q —————– Γ ® P Ú Q
( Ú 消去)	Γ ® P Ú Q Γ, P ® R Γ, Q ® R —————– Γ ® R

　次は、引数の個数が 2 の論理接続詞 Þ で、ÞPQ のかわりに P Þ Q と書くことにし、これに関する推論規則は以下のとおりです：

( Þ 導入)	Γ, P ® Q —————– Γ ® P Þ Q
( Þ 消去)	Γ ® P Þ Q Γ ® P —————– Γ ® Q

　次は、引数が命題であるような命題型量化記号 " で、"xP に関する推論規則は以下のとおりです：

( " 導入)	Γ ® P ————– Γ ® "xP	( x¢Γ )
( " 消去)	Γ ® "xP —————— Γ ® (T | x)P

　ただし ( " 導入) の横の但し書き x¢Γ は、x が Γ の中に現れない変数であることを意味します。

　次は、引数が命題であるような命題型量化記号 $ で、$xP に関する推論規則は以下のとおりです：

( $ 導入)	Γ ® (T | x)P —————— Γ ® $xP
( $ 消去)	Γ ® $xP Γ, P ® Q ————— Γ ® Q	( x¢Γ, Q )

　ただし ( $ 導入) の横の但し書き x¢Γ, Q は、x が Γ にも Q にも現れない変数であることを意味します。

　以上の論理記号と推論規則を持つ論理的な理論を最小論理といい、最小論理に、引数の個数が 0 の論理接続詞 ^ を、次の推論規則：

( ^ 消去)

Γ ® ^ ———– Γ ® P

と共に追加した理論を直観主義論理といいます。

　さて、上記の P Ù Q , P Ú Q , P Þ Q , "xP , $xP , ^ は、順にそれぞれ“命題 P と命題 Q が共に証明された”という事実、“命題 P と命題 Q の少なくとも一方が証明された”という事実、“命題 P を仮定に追加したら、命題 Q が証明された”という事実、“命題 P が自由変数 x に対して証明された”という事実、“命題 P の変数 x に、ある項を代入した命題が証明された”という事実、“証明され得ない命題である”という事実を形式化の原理によって一つの命題として表わしたものであるということが“導かれ”ます（付録２参照）。
　そこで、実際に推論を展開するときには、日常言語を流用して、P Ù Q のことを「P かつ Q」とも書き、P Ú Q のことを「P 又は Q」とも書き、P Þ Q のことを「P ならば Q」とも書き、"xP のことを「任意の x に対して P」とも書き、$xP のことを「P を満たす x が存在する」とも書き、^ のことを「矛盾」とも書くことにします。

　なお、( ~ 導入) と書かれた推論規則を、当該論理記号の導入規則、( ~ 消去) と書かれた推論規則を、当該論理記号の消去規則とよびます。

　ところで、実際に推論を行う際に、いつも仮定を含むsequentをいちいち書き下すのは煩わしいことです。
　そこで、sequentを用いずに、証明の冒頭で、ある命題群 Γ を公理であると宣言して、以後はその公理のもとで成り立つ命題のみを書き下していき、それらの命題のことを、公理系 Γ のもとでの定理とよぶ、という流儀の推論体系を考え、これを自然推論と名付けます（これに対し、sequentを用いる証明方法をsequent計算といいます）。
　自然推論では、一般に異なる公理系のもとでの推論を同時並行で行い、ある公理系 Γ のもとでの推論に、別の公理系のもとでの推論結果を利用することがあります。例えば、公理系 Γ のもとで推論しているとき、一時的に Γ に命題 P を追加した公理系 Γ, P のもとでの議論に“移る”ことを、「P と仮定する」という言い方で示唆し、その移動後の公理系のもとで命題 Q が得られたことを、推論図などでは P├ Q と表現します（なお、P├ Q の推論が終わって、もとの公理系での推論に戻るとき、その戻ったことを一々断らないのが普通です）。

　sequent計算による証明を自然推論による証明に変換するのは簡単で、次々に得られていくsequent Γ ® P に対し、Γ を公理系に持つ自然推論での証明文に P を定理として追加していく、というプロセスを続けていけばよいのです。
　逆に、自然推論における証明をsequent計算による証明に変換するには、この逆の行為、すなわち自然推論において、公理系 Γ のもとで P が定理として得られたら、sequent Γ ® P を新たに定理として追加していけばよいわけです。

　さて、上で挙げた論理記号に関する推論規則を自然推論に対する推論規則として書き直せば、次の表のようになります：

記号	Ù	Ú	Þ	"	$	^
導 入 規 則	P Q ——— P Ù Q	P ——— P Ú Q     Q ——— P Ú Q	P├ Q ———– P Þ Q	P ——— (x¢As)   "xP	(T | x)P ———— $xP	ナ シ
消 去 規 則	P Ù Q ——— P     P Ù Q ——— Q	P Ú Q P├ R Q├ R ———– R	P Þ Q P ———– Q	"xP ———— (T | x)P	$xP  P├ Q ———– (x¢As, Q )      Q	^ —— P

　ただし、( " 導入) と ( $ 消去) における但し書き中の As は、推論を行っているときの公理系 Γ を意味します。

　さて、( Ú 消去) は場合分けの方法とも呼ばれ、自然推論では“P 又は Q である。P のときは … R となり、Q のときも … R となり、いずれにせよ R が成り立つ。”というような言い回しによって、この推論規則を使っていることを示唆します。
　また ( Þ 消去) は三段論法とも呼ばれています。
　また ( $ 消去) は x を補助定数とする補助定数の方法とも呼ばれ、自然推論では“P を満たす x が存在する。そこでそのようなものの一つ x をとると … Q が成り立つ。これは x によらないので Q は証明された。”というような言い回しによって、この推論規則を使っていることを示唆します。

　P を命題とするとき、命題 P Þ ^ のことを ØP と略記することにします。これは「P と仮定すると矛盾する」言い換えると「P が正しいということはありえない」ということを意味するので、ØP のことを P でない とも呼びます。このとき、直観主義論理では、メタ定理として次が成り立ちます：

( Ø 導入)	P├ Q P├ ØQ ———— ØP
(弱Ø消去)	P ØP ——– Q

　ただし、これらの“図式”は、( Ø 導入) が P├ Q と P├ ØQ が成り立てば ØP が導けることを、(弱Ø消去) が P と ØP が成り立てば Q が導けることをそれぞれ意味しています。
　実際、P├ Q と P├ ØQ が成り立つ、すなわち P を仮定すると Q と ØQ すなわち Q Þ ^ が成り立つならば、(Þ消去) により ^ が得られ、これは P├ ^ を意味しますから、(Þ導入) により P Þ ^ すなわち ØP が得られることを意味します。
　また、P と ØP すなわち P Þ ^ が得られれば、(Þ消去) により ^ が得られ、更に (^消去) を用いれば Q が得られます。

　ところで、Ø を省略記号ではなく、引数の個数が 1 の論理接続詞で、上の二つを Ø に関する推論規則だと見なすこともできます。このように、Ø を本来記号と見なした場合、逆に論理記号 ^ の方を、勝手に選んだ命題 R に対する R Ù (ØR) の省略記号であると見なすことができます。
　実際、R Ù (ØR) と ( Ù 消去) により R と ØR が得られ、(弱Ø消去) により勝手な命題 P が導かれ、これは ( ^ 消去) に他ならないからです。

　次に、いわゆる二重否定 ØØP について考えてみましょう。これは ^ で表現すれば、(P Þ ^) Þ ^ 、すなわち「P を仮定して矛盾するなら（P を仮定しなくても）矛盾する」という意味で、これは要するに「P を正しいと見なしても、そのことで新たな矛盾を生むことはない」ということですから、そういう場合にも P を正しいということにしてしまおう、という立場も考えられます。
　そこで、直観主義論理の論理記号に、引数の個数が 1 の（P Þ ^ の省略記号としてではない）論理接続詞 Ø を加え、推論規則に (Ø導入) と次の (Ø消去) を加えた推論体系を古典論理といいます：

( Ø 消去)

ØØP ——— P

　この推論規則は二重否定の消去とも呼ばれますが、この (Ø消去) を用いると (弱Ø消去) が導かれることや、二重否定の消去と同等な他の推論規則については第３節で論じます。

　なお、次節以降で実際に推論を展開していくわけですが、本稿では古典論理のような“正しいと仮定しても矛盾を生じない”だけの命題を正しいことにしてしまうというような緩い立場はとらず、断りない限り、直観主義論理をベースに理論を展開します。更に、後で集合の概念を導入しますが、その場合も、数学のデファクト・スタンダードであるZF集合論やBG集合論ではなく、形式上の観点から根拠が正当化される公理のみを仮定するという立場をとります。このような数学を構成主義数学といい、様々なバリエーションがありますが、本稿の理論展開はそのようなものの一つです。