§E19.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理論である。

  1. Sx≠0Sx\ne0,
  2. Sx=Sy→x=ySx=Sy\to x=y,
  3. x=0∨∃y x=Syx=0\lor\exists y\,x=Sy,
  4. x+0=xx+0=x,
  5. x+Sy=S(x+y)x+Sy=S(x+y),
  6. x×0=0x\times0=0,
  7. x×Sy=(x×y)+xx\times Sy=(x\times y)+x.

例えば(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は空でもよい。空でない場合には、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で真であると仮定する。すなわち、

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

とする。メタ理論における自然数nnに関する帰納法を用いる。基底n=0n=0では条件 (a)からN⊨φ(0‾,a⃗)\mathbb N\models\varphi(\overline0,\vec a)である。N⊨φ(n‾,a⃗)\mathbb N\models\varphi(\overline n,\vec a)と仮定すると、条件 (b)を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. QQの公理から(Q3)を除いた六つの公理と、すべての帰納法公理とからなる理論をPA−PA^-とする。PA−⊢∀x (x=0∨∃y x=Sy)PA^-\vdash\forall x\,(x=0\lor\exists y\,x=Sy)であることを示せ。また、(Q3)を除いたQQの六つの公理だけからはこの文が導出されないことを、台集合N≥0×{0,1}\N\times\{0,1\}の構造を用いて示せ。
  2. φ(x,z)\varphi(x,z)に対する帰納法公理を、パラメータzzの全称閉包まで含めて書け。
  3. Q⊢3‾×2‾=6‾Q\vdash\overline3\times\overline2=\overline6の導出で(Q6)、(Q7)、加法公理をどの順に用いるかを示せ。
  4. 帰納法公理を用いて、PA⊢∀x (0+x=x)PA\vdash\forall x\,(0+x=x)とPA⊢∀x∀y (Sx+y=S(x+y))PA\vdash\forall x\forall y\,(Sx+y=S(x+y))を示せ。
解答 (確認問題の解答).

  1. φ(x)=(x=0∨∃y x=Sy)\varphi(x)=(x=0\lor\exists y\,x=Sy)とおく。等号の反射律からPA−⊢0=0PA^-\vdash0=0であり、選言の導入によりPA−⊢φ(0)PA^-\vdash\varphi(0)である。また反射律からPA−⊢Sx=SxPA^-\vdash Sx=Sxであり、存在導入によりPA−⊢∃y Sx=SyPA^-\vdash\exists y\,Sx=Sy、選言の導入によりPA−⊢φ(Sx)PA^-\vdash\varphi(Sx)を得る。弱化によりPA−⊢φ(x)→φ(Sx)PA^-\vdash\varphi(x)\to\varphi(Sx)であり、この導出の依存前提は文だけであるから一般化してPA−⊢∀x (φ(x)→φ(Sx))PA^-\vdash\forall x\,(\varphi(x)\to\varphi(Sx))を得る。パラメータのないφ\varphiに対応する帰納法公理[φ(0)∧∀x(φ(x)→φ(Sx))]→∀x φ(x)[\varphi(0)\land\forall x(\varphi(x)\to\varphi(Sx))]\to\forall x\,\varphi(x)へ modus ponens を適用するとPA−⊢∀x φ(x)PA^-\vdash\forall x\,\varphi(x)である。

    次に、台集合M=N≥0×{0,1}M=\N\times\{0,1\}上にLAL_A構造を定める。0M=(0,0)0^M=(0,0)、SM(n,i)=(n+1,i)S^M(n,i)=(n+1,i)とする。加法は、x∈Mx\in Mとm∈N≥0m\in\Nについて

    x+M(m,0)=(SM)m(x),x+M(m,1)=(m,1)x+^M(m,0)=(S^M)^m(x),\qquad x+^M(m,1)=(m,1)

    と定める。乗法は、各x∈Mx\in Mについてx×M(0,0)=0Mx\times^M(0,0)=0^M、x×M(0,1)=0Mx\times^M(0,1)=0^Mとし、x×M(m+1,i)=(x×M(m,i))+Mxx\times^M(m+1,i)=(x\times^M(m,i))+^Mxによってmmについての再帰で定める。(Q1)はSMS^Mの値の第一成分が正であることから、(Q2)はSMS^Mが単射であることから成り立つ。(Q4)はx+M(0,0)=xx+^M(0,0)=xによる。(Q5)は、y=(m,0)y=(m,0)ならば両辺が(SM)m+1(x)(S^M)^{m+1}(x)であり、y=(m,1)y=(m,1)ならば両辺が(m+1,1)(m+1,1)であることから成り立つ。(Q6)と(Q7)は乗法の定義そのものである。よってMMは六つの公理を満たす。一方、(0,1)≠0M(0,1)\neq0^Mであり、SMS^Mの値はすべて第一成分が正であるから(0,1)(0,1)はSMS^Mの値でない。したがってM⊭∀x (x=0∨∃y x=Sy)M\not\models\forall x\,(x=0\lor\exists y\,x=Sy)であり、健全性により六つの公理からこの文は導出されない。

  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. 第一の文について、φ(x)=(0+x=x)\varphi(x)=(0+x=x)とおく。(Q4)の全称閉包へ全称具体化を適用してPA⊢0+0=0PA\vdash0+0=0である。次に、(Q5)からPA⊢0+Sx=S(0+x)PA\vdash0+Sx=S(0+x)であり、前提0+x=x0+x=xと関数合同公理からS(0+x)=SxS(0+x)=Sxを得るので、等号の推移律によりPA∪{0+x=x}⊢0+Sx=SxPA\cup\{0+x=x\}\vdash0+Sx=Sxである。演繹定理によりPA⊢φ(x)→φ(Sx)PA\vdash\varphi(x)\to\varphi(Sx)であり、PAPAは文からなるので一般化してPA⊢∀x (φ(x)→φ(Sx))PA\vdash\forall x\,(\varphi(x)\to\varphi(Sx))を得る。φ\varphiに対応する帰納法公理と modus ponens によりPA⊢∀x (0+x=x)PA\vdash\forall x\,(0+x=x)である。

    第二の文について、ψ(y,x)=(Sx+y=S(x+y))\psi(y,x)=(Sx+y=S(x+y))とし、xxをパラメータとしてyyについて帰納法を用いる。(Q4)を二度用いるとSx+0=SxSx+0=Sxかつx+0=xx+0=xであり、後者と関数合同公理からS(x+0)=SxS(x+0)=Sxであるから、PA⊢ψ(0,x)PA\vdash\psi(0,x)である。前提ψ(y,x)\psi(y,x)のもとで、(Q5)によりSx+Sy=S(Sx+y)Sx+Sy=S(Sx+y)であり、前提と関数合同公理によりS(Sx+y)=SS(x+y)S(Sx+y)=SS(x+y)である。一方、(Q5)によりx+Sy=S(x+y)x+Sy=S(x+y)であるから、関数合同公理によりS(x+Sy)=SS(x+y)S(x+Sy)=SS(x+y)である。等号の対称律と推移律によりSx+Sy=S(x+Sy)Sx+Sy=S(x+Sy)、すなわちψ(Sy,x)\psi(Sy,x)を得る。演繹定理と一般化によりPA⊢∀y (ψ(y,x)→ψ(Sy,x))PA\vdash\forall y\,(\psi(y,x)\to\psi(Sy,x))であり、パラメータxxをもつ帰納法公理の全称閉包をxxで具体化して modus ponens を適用するとPA⊢∀y ψ(y,x)PA\vdash\forall y\,\psi(y,x)を得る。xxはPAPAの文に自由に現れないので一般化してPA⊢∀x∀y (Sx+y=S(x+y))PA\vdash\forall x\forall y\,(Sx+y=S(x+y))である。

    この導出はPAPAの帰納法公理を一行として含む有限列であり、定理 3.2の証明で用いた、標準自然数についてのメタ理論の帰納法とは異なる。

▨

参考文献

  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 算術の公理系の精密な定式化を参考にした。

前提記事