数学 › 数理論理学と型理論 › ゲーデルの不完全性定理

ペアノ算術 PA とロビンソン算術 Q

定義 2.2（「ゲーデルの不完全性定理」§2）

言語を LA={0,S,+,⋅}\mathcal{L}_A=\{0,S,+,\cdot\} とする（00 は定数、SS は 1 変数関数記号、++ と ⋅\cdot は 2 変数関数記号）。x<yx < y は ∃z (x+Sz=y)\exists z\,(x+Sz=y) の、x≤yx\le y は ∃z (x+z=y)\exists z\,(x+z=y) の略記とする。自然数 nn に対し数項 n‾\overline{n} を S⋯S⏟n 個0\underbrace{S\cdots S}_{n\ \text{個}}0 で定める。

ロビンソン算術 QQ は次の 7 つの公理からなる。

(Q1) ∀x (Sx≠0)(Q2) ∀x∀y (Sx=Sy→x=y)(Q3) ∀x (x≠0→∃y (x=Sy))(Q4) ∀x (x+0=x)(Q5) ∀x∀y (x+Sy=S(x+y))(Q6) ∀x (x⋅0=0)(Q7) ∀x∀y (x⋅Sy=x⋅y+x)\begin{aligned} &\text{(Q1)}\ \forall x\,(Sx\ne 0) &&\text{(Q2)}\ \forall x\forall y\,(Sx=Sy\to x=y)\\ &\text{(Q3)}\ \forall x\,(x\ne 0\to\exists y\,(x=Sy)) &&\text{(Q4)}\ \forall x\,(x+0=x)\\ &\text{(Q5)}\ \forall x\forall y\,(x+Sy=S(x+y)) &&\text{(Q6)}\ \forall x\,(x\cdot 0=0)\\ &\text{(Q7)}\ \forall x\forall y\,(x\cdot Sy=x\cdot y+x) && \end{aligned}

ペアノ算術 PA\mathrm{PA} は QQ から (Q3) を除いたものに、次の帰納法図式を加えた理論である：自由変数を持つ各論理式 φ(x,y)\varphi(x,\boldsymbol{y}) に対し

∀y[(φ(0,y)∧∀x (φ(x,y)→φ(Sx,y)))→∀x φ(x,y)]\forall\boldsymbol{y}\Big[\big(\varphi(0,\boldsymbol{y})\wedge\forall x\,(\varphi(x,\boldsymbol{y})\to\varphi(Sx,\boldsymbol{y}))\big)\to\forall x\,\varphi(x,\boldsymbol{y})\Big]

を公理とする。

本文で読む（前後の説明と例）→

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。

これを使っている定理

証明で明示的に参照している定理は、まだありません。

関連するノック 1 問