§E16.15Robinson 算術 Q と Peano 算術 PA

最終更新

自然数について推論するとき、外側で行う通常の自然数計算と、形式理論の内部で行う証明とを区別する必要がある。本記事では算術の一階言語と二つの理論を固定し、標準モデルが両理論のモデルであることを確認する。有限個の公理だけをもつQQと、帰納法公理スキーマを加えたPAPAは、後続する算術化の共通の基礎になる。

1 算術の言語と標準構造

定義 1.1. 算術の一階言語 (first-order language of arithmetic) を

LA={0,S,+,×}L_A=\{0,S,+,\times\}

とする。00は定数記号、SSは一項関数記号、++と×\timesは二項関数記号である。標準モデル (standard model of arithmetic) を

N=(N,0,S,+,×)\mathbb N=(\mathbb N,0,S,+,\times)

と書き、各記号を通常の零、後続者、加法、乗法として解釈する。標準自然数nnの数詞 (numeral) は

n‾=Sn0\overline n=S^n0

である。特に0‾=0\overline0=0、n+1‾=Sn‾\overline{n+1}=S\overline nである。

順序記号はLAL_Aの原始記号ではない。以後は次の略記を用いる。

x<y: ⁣ ⁣⟺∃z (y=x+Sz),x≤y: ⁣ ⁣⟺∃z (y=x+z).x<y\quad:\!\!\Longleftrightarrow\quad \exists z\,(y=x+Sz), \qquad x\le y\quad:\!\!\Longleftrightarrow\quad \exists z\,(y=x+z).

標準構造では、これらは通常の狭義順序と広義順序を表す。

2 Robinson 算術 Q

定義 2.1. Robinson 算術QQ (Robinson arithmetic Q) は、次の七式の全称閉包を公理とするLAL_A理論である。

(Q1)Sx≠0,(Q2)Sx=Sy→x=y,(Q3)x=0∨∃y x=Sy,(Q4)x+0=x,(Q5)x+Sy=S(x+y),(Q6)x×0=0,(Q7)x×Sy=(x×y)+x.\begin{array}{rll} \text{(Q1)}&Sx\ne0,&\\ \text{(Q2)}&Sx=Sy\to x=y,&\\ \text{(Q3)}&x=0\lor\exists y\,x=Sy,&\\ \text{(Q4)}&x+0=x,&\\ \text{(Q5)}&x+Sy=S(x+y),&\\ \text{(Q6)}&x\times0=0,&\\ \text{(Q7)}&x\times Sy=(x\times y)+x.& \end{array}

例えば (Q5) は文∀x∀y (x+Sy=S(x+y))\forall x\forall y\,(x+Sy=S(x+y))を表す。

(Q3) は、零でない各要素が何らかの要素の後続者であることを述べる。しかし、七公理の中に帰納法公理はない。QQが帰納法を含まないという記述は、公理集合に関するこの事実を指す。帰納法の各例がQQから導出不能であるという別の主張を、定義だけから結論することはできない。

定理 2.2.N⊨Q\mathbb N\models Qである。

証明. 任意のm,n∈Nm,n\in\mathbb Nを取る。通常の自然数では後続者m+1m+1は00ではないので (Q1) が成り立つ。m+1=n+1m+1=n+1ならm=nm=nなので (Q2) が成り立つ。m=0m=0であるか、m>0m>0ならm=(m−1)+1m=(m-1)+1であるから、 (Q3) も成り立つ。

通常の加法の定義からm+0=mm+0=mおよびm+(n+1)=(m+n)+1m+(n+1)=(m+n)+1であり、(Q4) と (Q5) が成り立つ。通常の乗法の定義からm×0=0m\times0=0およびm×(n+1)=(m×n)+mm\times(n+1)=(m\times n)+mであり、(Q6) と (Q7) が成り立つ。各確認は任意のm,nm,nについて成り立つので、七式の全称閉包をN\mathbb Nがすべて満たす。したがってN⊨Q\mathbb N\models Qである。▨

3 Peano 算術 PA

定義 3.1.φ(x,z⃗)\varphi(x,\vec z)を、表示した変数のほかにも束縛変数を含んでよい任意のLAL_A論理式とする。φ\varphiに対応する帰納法公理 (induction axiom) は、

[φ(0,z⃗)∧∀x(φ(x,z⃗)→φ(Sx,z⃗))]→∀x φ(x,z⃗)\bigl[\varphi(0,\vec z)\land \forall x\bigl(\varphi(x,\vec z)\to\varphi(Sx,\vec z)\bigr)\bigr] \to\forall x\,\varphi(x,\vec z)

の自由なパラメータz⃗\vec zに関する全称閉包である。 Peano 算術PAPA (Peano arithmetic PA) は、QQの七公理と、すべてのLAL_A論理式φ(x,z⃗)\varphi(x,\vec z)に対応する帰納法公理を公理とする。

一つの論理式ごとに一つの一階文を加えるため、帰納法は単一の公理ではなく公理スキーマである。パラメータz⃗\vec zは空でもよい。空でない場合には、その値を固定した各性質について帰納法を適用する。

定理 3.2.N⊨PA\mathbb N\models PAである。

証明.定理 2.2によりN\mathbb NはQQの七公理を満たす。任意のLAL_A論理式φ(x,z⃗)\varphi(x,\vec z)と、パラメータz⃗\vec zへの任意の割当てa⃗\vec aを固定する。対応する帰納法公理の前件がN\mathbb Nで真であると仮定する。すなわち、

N⊨φ(0,a⃗),N⊨∀x(φ(x,a⃗)→φ(Sx,a⃗))\mathbb N\models\varphi(0,\vec a), \qquad \mathbb N\models \forall x\bigl(\varphi(x,\vec a)\to\varphi(Sx,\vec a)\bigr)

とする。メタ理論における自然数nnに関する帰納法を用いる。基底n=0n=0では第1の仮定からN⊨φ(0‾,a⃗)\mathbb N\models\varphi(\overline0,\vec a)である。N⊨φ(n‾,a⃗)\mathbb N\models\varphi(\overline n,\vec a)と仮定すると、第2の仮定をnnに適用してN⊨φ(n+1‾,a⃗)\mathbb N\models\varphi(\overline{n+1},\vec a)を得る。したがってすべてのn∈Nn\in\mathbb NについてN⊨φ(n‾,a⃗)\mathbb N\models\varphi(\overline n,\vec a)である。N\mathbb Nの各要素はただ一つの標準自然数nnなので、N⊨∀x φ(x,a⃗)\mathbb N\models\forall x\,\varphi(x,\vec a)となる。

よって帰納法公理の前件が真なら結論も真である。φ\varphiとa⃗\vec aは任意だったので、N\mathbb Nは帰納法公理スキーマのすべての例を満たす。したがってN⊨PA\mathbb N\models PAである。▨

この証明で用いたnnに関する帰納法は、PAPAの内部証明ではなく、記事を記述しているメタ理論の帰納法である。モデルが公理を満たすことを外側から証明する際にメタ理論の帰納法を用いても、QQの公理集合へ帰納法が追加されるわけではない。

4 固定した数詞の計算

後続する符号化では、標準自然数について実際に終了した計算をQQの有限証明へ移す。次の補題では、m,nm,nはメタ理論で固定した標準自然数である。

補題 4.1. 任意の標準自然数m,nm,nについて、次が成り立つ。

Q⊢m‾+n‾=m+n‾,Q⊢m‾×n‾=mn‾.\begin{aligned} Q&\vdash \overline m+\overline n=\overline{m+n},\\ Q&\vdash \overline m\times\overline n=\overline{mn}. \end{aligned}

さらに、m≠nm\ne nならQ⊢m‾≠n‾Q\vdash\overline m\ne\overline nであり、m<nm<nならQ⊢m‾<n‾Q\vdash\overline m<\overline nである。

証明.nnを固定した有限回の書換えを行う。加法では (Q4) によりQ⊢m‾+0‾=m‾Q\vdash\overline m+\overline0=\overline mである。 (Q5) をnn回適用すると

m‾+n‾=Sn(m‾+0)=Snm‾=m+n‾\overline m+\overline n =S^n(\overline m+0) =S^n\overline m =\overline{m+n}

を得る。これは対象理論内の帰納法ではなく、固定したnnに応じて作る有限導出である。乗法も (Q6) から始め、(Q7) をnn回適用し、既に得た加法の計算を各段で用いればQ⊢m‾×n‾=mn‾Q\vdash\overline m\times\overline n=\overline{mn}を得る。

m<nm<nならn=m+(d+1)n=m+(d+1)を満たす標準自然数ddが存在する。加法の計算によりQ⊢n‾=m‾+Sd‾Q\vdash\overline n=\overline m+S\overline dなので、<<の定義へ存在導入してQ⊢m‾<n‾Q\vdash\overline m<\overline nを得る。

m≠nm\ne nとする。一般性を失わずm<nm<nとしてよい。m‾=n‾\overline m=\overline nを仮定し、両辺から共通するmm個のSSを (Q2) で順に除くと0=Sn−m00=S^{n-m}0を得る。最後の式は (Q1) に反する。したがってQ⊢m‾≠n‾Q\vdash\overline m\ne\overline nである。m>nm>nの場合も左右を交換した同じ有限導出による。▨

例 4.2 (内部証明と標準モデルでの真理). 標準自然数の計算2+3=52+3=5はメタ理論上の等式である。補題 4.1は、この計算から形式導出Q⊢2‾+3‾=5‾Q\vdash\overline2+\overline3=\overline5を与える。定理 2.2と健全性を介せばN⊨2‾+3‾=5‾\mathbb N\models\overline2+\overline3=\overline5も従う。三つの主張は関係するが、それぞれ自然数、形式導出、構造における充足という異なる対象を述べている。

注意 4.3 (証明、真理、外側の計算). 次の三段階を区別する。

  1. T⊢σT\vdash\sigmaは、理論TTの公理から文σ\sigmaへの有限な形式導出が存在するという構文上の主張である。
  2. N⊨σ\mathbb N\models\sigmaは、標準モデルで文σ\sigmaが真であるという意味論上の主張である。
  3. m+n=rm+n=rは、メタ理論で自然数を計算した結果に関する主張である。

N⊨T\mathbb N\models Tと健全性からT⊢σT\vdash\sigmaならN⊨σ\mathbb N\models\sigmaと移ることができる。逆向きの移行には追加の議論が必要であり、記号だけを置き換えてはならない。

5 演習

問題 5.1.

  1. (Q3) と帰納法公理スキーマが述べる内容の違いを説明せよ。
  2. φ(x,z)\varphi(x,z)に対する帰納法公理を、パラメータzzの全称閉包まで含めて書け。
  3. Q⊢3‾×2‾=6‾Q\vdash\overline3\times\overline2=\overline6の導出で (Q6)、(Q7)、加法公理をどの順に用いるかを示せ。
  4. 定理 3.2の証明で用いた帰納法が、PAPAの内部の帰納法ではない理由を説明せよ。
解答 (確認問題の解答).
  1. (Q3) は一つの要素が零であるか後続者であるかを述べる一つの一階文である。帰納法公理スキーマは、基底と後続者に関する閉性から全要素での成立を導く文を、各論理式について加える。
  2. ∀z([φ(0,z)∧∀x(φ(x,z)→φ(Sx,z))]→∀xφ(x,z))\forall z\bigl([\varphi(0,z)\land\forall x(\varphi(x,z)\to\varphi(Sx,z))]\to\forall x\varphi(x,z)\bigr)である。
  3. (Q7) を二回用いて3‾×2‾=(3‾×1‾)+3‾=((3‾×0)+3‾)+3‾\overline3\times\overline2=(\overline3\times\overline1)+\overline3=((\overline3\times0)+\overline3)+\overline3とし、(Q6) と固定数詞の加法計算で6‾\overline6へ書き換える。
  4. 証明者が外側の標準自然数nnについて行う数学的帰納法だからである。対象理論の導出列の中で帰納法公理を使用してはいない。

▨

参考文献

  1. Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001.数論の形式化、標準モデル、数詞、および帰納法公理スキーマの扱いを参考にした。
  2. Petr Hájek and Pavel Pudlák, Metamathematics of First-Order Arithmetic, Perspectives in Logic 3, Cambridge University Press, Cambridge, 2017, originally published 1993.Robinson 算術と Peano 算術の公理系の精密な定式化を参考にした。

前提記事