Robinson算術

同義語：Robinson arithmeticRobinsonの算術ロビンソン算術Robinson's Q

概要

Robinson算術（Robinson arithmetic）とは、言語 $\{0,S,+,\cdot,<\}$ で後者関数の単射性、$0$ が後者でないこと、$0$ 以外が後者であること、和と積の再帰の式、大小の定義の 8 個の文を公理とする一階の理論 $\mathsf Q$ であり、Peano 算術から帰納法を除いたものである。有界な量化だけの文は真なら $\mathsf Q$ で証明でき、偽なら否定が証明でき、存在量化を前に付けた $\Sigma_1$ 文も標準モデルで真ならすべて $\mathsf Q$ で証明できる。したがって $\mathsf Q$ を含む無矛盾な理論が証明する $\Pi_1$ 文は真であり、$\mathsf Q$ は不完全性定理や決定不能性の定理が当てはまる代表的な弱い理論になっている。一方 $0+x=x$ や和の可換性は証明できない。

$$\newcommand{C}[0]{\mathbb{C}} \newcommand{div}[0]{\mathbin{÷}} \newcommand{N}[0]{\mathbb{N}} \newcommand{Q}[0]{\mathbb{Q}} \newcommand{R}[0]{\mathbb{R}} \newcommand{Z}[0]{\mathbb{Z}} $$

前提知識: 一階述語論理, Peano算術, 自然数

Peano算術 $\mathsf{PA}$ から帰納法の公理をすべて取り除くと、後者関数・和・積・大小についての 8 個の文だけが残る。これを Robinson算術（Robinson arithmetic）といい、$\mathsf Q$ と書く。公理が有限個しかなく、$0+x=x$ や $x+y=y+x$ のような自然数の基本法則すら証明できない、非常に弱い理論である。
それでも $\mathsf Q$ は、具体的な数についての計算、たとえば「$2+2=4$」「$7$ は素数である」「$n^2+1$ が素数になる $n\le10^{6}$ がある」のような、有限の計算で確かめられる真の文を証明する。正確には、存在量化をいくつか前に付けた有界な文（$\Sigma_1$ 文）のうち真なものはすべて $\mathsf Q$ で証明できる。この性質は、計算可能な関数がすべて $\mathsf Q$ で表現できること（rem-q-cited）とともに、$\mathsf Q$ を含む理論に Gödelの不完全性定理 や決定不能性の定理が当てはまる土台になる。$\mathsf Q$ はこれらの定理が成り立つ代表的な弱い理論である。
この記事では、$\mathsf Q$ を定義し、数項についての計算と大小の補題（lem-q-numerals）を示したうえで、$\mathsf Q$ が真の $\Sigma_1$ 文をすべて証明すること（thm-q-sigma1）と、その帰結として $\mathsf Q$ を含む無矛盾な理論が証明する $\Pi_1$ 文は真であること（cor-q-pi1）を証明する。また、$\mathsf Q$ のモデルを作って $0+x=x$ と和の可換性が証明できないこと（ex-q-model）を確かめ、公理 1・2・3・8 のどれを外しても $\Sigma_1$ 完全性が成り立たなくなることを反例で示す。

定義

算術の言語を $L_A=\{0,S,+,\cdot,<\}$ とする（$0$ は定数記号、$S$ は 1 変数の関数記号、$+$ と $\cdot$ は 2 変数の関数記号、$<$ は 2 変数の関係記号）。自然数 $n$ に対し、$S$ を $n$ 個並べた項 $S\cdots S0$ を $n$ の 数項 といい、$\underline n$ と書く。$\mathbb N$ に通常の $0$、$n\mapsto n+1$、和・積・大小を入れた構造を 標準モデル といい、$\mathfrak N$ と書く。変数を含まない項を 閉項 といい、閉項 $t$ の $\mathfrak N$ での値を $t^{\mathfrak N}$ と書く。

Robinson算術

次の 8 個の文を公理とする理論を Robinson算術 といい、$\mathsf Q$ と書く。

  1. $\forall x\forall y\,(Sx=Sy\to x=y)$
  2. $\forall x\,\lnot(0=Sx)$
  3. $\forall x\,(\lnot x=0\to\exists y\,x=Sy)$
  4. $\forall x\,(x+0=x)$
  5. $\forall x\forall y\,(x+Sy=S(x+y))$
  6. $\forall x\,(x\cdot0=0)$
  7. $\forall x\forall y\,(x\cdot Sy=x\cdot y+x)$
  8. $\forall x\forall y\,\bigl(x< y\leftrightarrow\exists z\,(Sz+x=y)\bigr)$
    $L_A$ の理論 $T$ が $\mathsf Q$ の 8 個の公理をすべて導出するとき、$T$ は $\mathsf Q$ を含む という。

これは Peano算術 の定義「Peano算術」と Gödelの不完全性定理 の定義「Robinson の算術と Peano 算術」の $\mathsf Q$ と同じものである（OLT26 Definition 33.5、p. 524）。名前は Raphael Robinson にちなむ（同書 §35.1、p. 552）。公理 1〜3 は $S$ が単射で $0$ を値にとらず、$0$ 以外の元は後者であることを、4〜7 は和と積の再帰的な定義を、8 は大小を和で定義することを述べる。8 個の文はどれも $\mathfrak N$ で真なので、$\mathfrak N$ は $\mathsf Q$ のモデルであり、健全性定理 により $\mathsf Q$ は無矛盾である。$\mathsf Q$ に帰納法の公理図式を加えたものが $\mathsf{PA}$ なので、$\mathsf{PA}$ は $\mathsf Q$ を含む。
$\mathsf Q$ が扱える文の範囲を測るために、量化の範囲が項で抑えられた論理式を考える。

$\Delta_0$ 論理式・$\Sigma_1$ 論理式・$\Pi_1$ 論理式

変数 $x$ と、$x$ を含まない項 $t$ について、$\forall x\,(x< t\to\varphi)$ を $\forall x< t\,\varphi$、$\exists x\,(x< t\land\varphi)$ を $\exists x< t\,\varphi$ と書き、有界な量化 という。

  1. 原子論理式から、$\lnot,\land,\lor,\to$ と有界な量化だけで作られる論理式を $\Delta_0$ 論理式 という。
  2. $\Delta_0$ 論理式 $\psi$ と $k\ge0$ について、$\exists x_1\cdots\exists x_k\,\psi$ の形の論理式を $\Sigma_1$ 論理式、$\forall x_1\cdots\forall x_k\,\psi$ の形の論理式を $\Pi_1$ 論理式 という。

$k=0$ を許しているので、$\Delta_0$ 論理式は $\Sigma_1$ 論理式でも $\Pi_1$ 論理式でもある。$\Sigma_1$ 文 $\exists\vec x\,\psi$ の否定は $\Pi_1$ 文 $\forall\vec x\,\lnot\psi$ と論理的に同値である（$\lnot\psi$ も $\Delta_0$）。OLT26 Definition 35.33（p. 569）は量化を 1 つに限っているが、以下の議論は同じである。

有界な文で書ける性質
  1. 「$x$ は素数である」は $\Delta_0$ 論理式 $\mathrm{Pr}(x):=\underline1< x\land\forall y< x\,\forall z< x\,\lnot(y\cdot z=x)$ で書ける（$x>1$ のとき、$y,z< x$ で $yz=x$ となるのは、$x$ が $1$ と $x$ 以外の約数をもつときに限る）。
  2. 「$n^2+1$ が素数になる $n\le10^6$ がある」は、閉項 $t$ を $10^6+1$ の数項として $\exists n< t\,\mathrm{Pr}(n\cdot n+\underline1)$ と書ける $\Delta_0$ 文である。
  3. Goldbach 予想「$2$ より大きい偶数は 2 つの素数の和である」は、$\forall x\,\bigl(\underline1< x\to\exists p< \underline2\cdot x\,\exists q< \underline2\cdot x\,(\mathrm{Pr}(p)\land\mathrm{Pr}(q)\land p+q=\underline2\cdot x)\bigr)$ と書ける $\Pi_1$ 文である。

数項の計算と大小

数項の計算と大小

自然数 $m,n$ と閉項 $s,t$ について、次が成り立つ。

  1. $\mathsf Q\vdash t=\underline{t^{\mathfrak N}}$。
  2. $m\ne n$ なら $\mathsf Q\vdash\lnot\,\underline m=\underline n$。
  3. $m< n$ なら $\mathsf Q\vdash\underline m<\underline n$。
  4. $\mathsf Q\vdash\forall x\,\bigl(x<\underline n\leftrightarrow x=\underline0\lor x=\underline1\lor\cdots\lor x=\underline{n-1}\bigr)$。$n=0$ では右辺を偽の文とし、$\mathsf Q\vdash\forall x\,\lnot\,x< 0$ と読む。
  5. $s^{\mathfrak N}\ge t^{\mathfrak N}$ なら $\mathsf Q\vdash\lnot\,s< t$。
理論の外での帰納法

1・2：Peano算術 の命題「数項の計算」の 1 は、公理 4〜7 だけを使って $\mathsf Q\vdash\underline a+\underline b=\underline{a+b}$、$\mathsf Q\vdash\underline a\cdot\underline b=\underline{ab}$ を示し、同じ命題の 2 はこの補題の 2 そのものである。この補題の 1 は、それと等号の規則を使った $t$ の構成についての帰納法で得られる（$t=Ss'$ なら、$\underline{s'^{\mathfrak N}}$ に $S$ を付けた項が $\underline{t^{\mathfrak N}}$ である）。
3：$c:=n-m-1$ とおく。$S\underline c$ は項として $\underline{c+1}$ なので、1 により $\mathsf Q\vdash S\underline c+\underline m=\underline{c+1+m}=\underline n$ であり、公理 8 により $\mathsf Q\vdash\underline m<\underline n$ である。
4：$n$ についての（理論の外での）帰納法による。以下は $\mathsf Q$ の中での推論である。
$n=0$：$x< 0$ とすると、公理 8 により $Sz+x=0$ となる $z$ がある。公理 3 により $x=0$ または $x=Sw$ となる $w$ がある。$x=0$ なら公理 4 により $Sz=0$、$x=Sw$ なら公理 5 により $S(Sz+w)=0$ で、どちらも公理 2 に反する。
$n$ から $n+1$：$x< S\underline n\leftrightarrow(x<\underline n\lor x=\underline n)$ を示せば、帰納法の仮定と合わせて主張を得る。
($\Rightarrow$) $Sz+x=S\underline n$ とする。$x=0$ の場合、$n=0$ なら $x=\underline n$、$n\ge1$ なら 3 により $x<\underline n$ である。$x=Sw$ の場合、公理 5 により $S(Sz+w)=S\underline n$、公理 1 により $Sz+w=\underline n$ で、公理 8 により $w<\underline n$ である。帰納法の仮定により $w=\underline k$ となる $k< n$ があり、$x=S\underline k=\underline{k+1}$ である。$k+1=n$ なら $x=\underline n$、$k+1< n$ なら 3 により $x<\underline n$ である。
($\Leftarrow$) $x<\underline n$ なら帰納法の仮定により $x=\underline k$（$k< n$）で、3 により $\underline k<\underline{n+1}$ である。$x=\underline n$ なら 3 により $\underline n<\underline{n+1}$ である。
5：$a:=s^{\mathfrak N}$、$b:=t^{\mathfrak N}$ とおく。1 により $\mathsf Q\vdash s< t\leftrightarrow\underline a<\underline b$ で、4 により $\underline a<\underline b$ は $\underline a=\underline k$（$k< b$）の選言と同値である。$a\ge b> k$ なので 2 により各 $\underline a=\underline k$ は否定でき、$\mathsf Q\vdash\lnot\,s< t$ である。$\square$

Peano算術 の命題「数項の計算」の 3 は 4 の $\to$ の向きを $\mathsf{PA}$ で述べたもので、上の証明はそれが帰納法の公理なしに $\mathsf Q$ で証明できることを示している（OLT26 Lemmas 35.23–35.24、p. 564）。4 は、$\mathsf Q$ のどのモデルでも、$\underline n$ より小さい元は $\underline 0,\dots,\underline{n-1}$ だけであることを意味する。

主定理：$\Sigma_1$ 完全性

$\Delta_0$ 文の判定

$\sigma$ を $\Delta_0$ 文とする。$\mathfrak N\models\sigma$ なら $\mathsf Q\vdash\sigma$ であり、$\mathfrak N\not\models\sigma$ なら $\mathsf Q\vdash\lnot\sigma$ である。

有界な量化を有限個の場合に分ける

$\sigma$ に現れる論理記号（$\lnot,\land,\lor,\to$ と量化記号）の個数についての帰納法で、2 つの主張を同時に示す。
原子文. $\sigma$ が $s=t$ のとき：$s^{\mathfrak N}=t^{\mathfrak N}$ なら lem-q-numerals の 1 と等号の規則により $\mathsf Q\vdash s=t$、そうでなければ 1・2 により $\mathsf Q\vdash\lnot\,s=t$ である。$\sigma$ が $s< t$ のとき：$s^{\mathfrak N}< t^{\mathfrak N}$ なら 1・3 により $\mathsf Q\vdash s< t$、そうでなければ 5 により $\mathsf Q\vdash\lnot\,s< t$ である。
結合子. たとえば $\sigma=\lnot\tau$ なら、$\sigma$ が真のとき $\tau$ は偽で、帰納法の仮定により $\mathsf Q\vdash\lnot\tau$、すなわち $\mathsf Q\vdash\sigma$ であり、$\sigma$ が偽のとき $\mathsf Q\vdash\tau$ なので $\mathsf Q\vdash\lnot\sigma$ である。$\land,\lor,\to$ も、両辺の真偽に応じて帰納法の仮定の結論を命題論理で組み合わせればよい。
有界な量化. $\sigma=\forall x< t\,\varphi(x)$ とする。$\sigma$ は文なので $t$ は閉項であり、$n:=t^{\mathfrak N}$ とおく。lem-q-numerals の 1・4 と等号の規則により
$$ \mathsf Q\vdash\sigma\leftrightarrow\varphi(\underline0)\land\varphi(\underline1)\land\cdots\land\varphi(\underline{n-1}) $$
である（$n=0$ なら右辺は真の文で、$\sigma$ も $\mathfrak N$ で真）。各 $\varphi(\underline k)$ は論理記号が $\sigma$ より少ない $\Delta_0$ 文である。$\sigma$ が真ならすべての $\varphi(\underline k)$（$k< n$）が真で、帰納法の仮定によりすべて証明でき、$\mathsf Q\vdash\sigma$ である。$\sigma$ が偽なら、ある $k< n$ で $\varphi(\underline k)$ が偽なので $\mathsf Q\vdash\lnot\varphi(\underline k)$ となり、$\mathsf Q\vdash\lnot\sigma$ である。$\exists x< t\,\varphi(x)$ も、右辺を選言に替えて同じように示せる。$\square$

$\mathsf Q$ の $\Sigma_1$ 完全性

$\mathfrak N$ で真な $\Sigma_1$ 文は、すべて $\mathsf Q$ で証明できる。したがって $\mathsf Q$ を含む理論もそれらをすべて証明する。

証拠を数項で入れる

$\sigma=\exists x_1\cdots\exists x_k\,\psi(x_1,\dots,x_k)$（$\psi$ は $\Delta_0$）が $\mathfrak N$ で真なら、$\mathfrak N\models\psi(\underline{n_1},\dots,\underline{n_k})$ となる自然数 $n_1,\dots,n_k$ がある（$\mathfrak N$ の元 $n$ は数項 $\underline n$ の値である）。$\psi(\underline{n_1},\dots,\underline{n_k})$ は $\Delta_0$ 文なので、thm-q-delta0 により $\mathsf Q$ で証明でき、存在量化の導入で $\mathsf Q\vdash\sigma$ を得る。$\square$

この定理は OLT26 Theorem 35.38（p. 571）にある。$\mathfrak N$ は $\mathsf Q$ のモデルなので、逆に $\mathsf Q$ で証明できる文は $\mathfrak N$ で真である。よって $\Sigma_1$ 文については「$\mathfrak N$ で真」と「$\mathsf Q$ で証明できる」が一致する。ex-q-hierarchy の 2 の文は $\mathsf Q$ で証明できる（$n=1$ で $n^2+1=2$ が素数）。

$\mathsf Q$ を含む無矛盾な理論の $\Pi_1$ 文

$T$ を $\mathsf Q$ を含む無矛盾な $L_A$ の理論とする。$T$ で証明できる $\Pi_1$ 文は、すべて $\mathfrak N$ で真である。

$\pi=\forall\vec x\,\psi$（$\psi$ は $\Delta_0$）が $T$ で証明でき、$\mathfrak N$ で偽だとする。すると $\exists\vec x\,\lnot\psi$ は $\mathfrak N$ で真な $\Sigma_1$ 文なので、thm-q-sigma1 により $T$ で証明できる。これは $\lnot\pi$ と論理的に同値なので、$T$ は $\pi$ と $\lnot\pi$ を証明して矛盾する。$\square$

たとえば Goldbach 予想（ex-q-hierarchy の 3）が偽なら、その否定は $\mathsf Q$ で証明できる。逆に、$\mathsf Q$ を含む無矛盾な理論で Goldbach 予想が証明されれば、それは本当に正しい。一方、$\Pi_1$ 文は真でも $\mathsf Q$ で証明できるとは限らない（次節）。

$\mathsf Q$ の弱さ

$\mathsf Q$ で証明できないことを示すには、健全性定理 により、その文が偽になる $\mathsf Q$ のモデルを作ればよい。

和が可換でない $\mathsf Q$ のモデル

相異なる新しい元 $a,b$ をとり、台集合を $M:=\mathbb N\cup\{a,b\}$ とする。$\mathbb N$ の上では $S$・和・積を通常どおりとし、$n\in\mathbb N$ について次のように定める。
$$ Sa=a,\quad Sb=b,\qquad a+n=a,\quad b+n=b,\quad n+a=b,\quad n+b=a, $$
$$ a+a=b,\quad b+b=a,\quad a+b=a,\quad b+a=b. $$
積は $x\cdot0=0$ とし、$n\ge1$ について $a\cdot n=b$、$b\cdot n=a$、$y\in\{a,b\}$ について $0\cdot y=0$、$n\cdot y=y$、$a\cdot y=b$、$b\cdot y=a$ とする。$<$ は公理 8 の右辺で、$x< y\iff$「$Sz+x=y$ となる $z\in M$ がある」と定める。
このとき $M$ は $\mathsf Q$ のモデルで、$0+a=b\ne a=a+0$ である。よって $M$ では $\forall x\,(0+x=x)$ と $\forall x\forall y\,(x+y=y+x)$ がどちらも偽であり、$\mathsf Q$ はこの 2 つの文を証明しない。どちらも $\mathsf{PA}$ では証明できる（Peano算術 の定理「$\mathsf{PA}$ が証明する基本法則」の (A1)・(A4)）。

公理の確かめを開く

公理 1：$S$ は $\mathbb N$ の上で単射で、$\mathbb N$ の元を $\mathbb N\setminus\{0\}$ に移し、$a,b$ を動かさない。公理 2：$0$ はどの元の後者でもない。公理 3：$n\ge1$ は $S(n-1)$、$a=Sa$、$b=Sb$ である。公理 4：$x+0=x$ は表から分かる。公理 5：$y=n$ で $x\in\mathbb N$ なら通常の等式、$x\in\{a,b\}$ なら $x+(n+1)=x=Sx=S(x+n)$。$y\in\{a,b\}$ なら $Sy=y$ で、$x+y\in\{a,b\}$ は $S$ で動かないので両辺は $x+y$ に等しい。公理 6 は定義である。

公理 7：$y=n$ で $x\in\mathbb N$ なら通常の等式である。$x=a$ のとき $a\cdot1=b=0+a=a\cdot0+a$、$n\ge1$ なら $a\cdot(n+1)=b=b+a=a\cdot n+a$。$x=b$ のとき $b\cdot1=a=0+b$、$n\ge1$ なら $b\cdot(n+1)=a=a+b$。$y\in\{a,b\}$ なら $Sy=y$ なので $x\cdot y=x\cdot y+x$ を確かめればよく、$x=0$ では $0=0+0$、$x=n\ge1$ では $y+n=y$、$x=a$ では $b+a=b$、$x=b$ では $a+b=a$ である。公理 8 は $<$ の定め方による。

和の表は OLT26 Example 26.9（p. 398）のもので、同書は積を定めていないので、ここでは公理 6・7 を満たすように積を補った。数項どうしの $\underline m+\underline n=\underline n+\underline m$ は真な $\Delta_0$ 文なので、thm-q-delta0 によりどれも $\mathsf Q$ で証明できる。$\mathsf Q$ はすべての数値例を証明するのに、それらをまとめた全称文は証明しない。$\forall x\,(0+x=x)$ は真な $\Pi_1$ 文なので、thm-q-sigma1 を $\Pi_1$ 文に広げることはできない。ほかにも、元を 1 つだけ付け加えたモデルから $\mathsf Q$ が $\forall x\,\lnot(x=Sx)$ と $\forall x\,\lnot\,x< x$ を証明しないことが分かる（Peano算術 の例「$\mathsf Q$ のモデルで $\mathsf{PA}$ のモデルでないもの」、Gödelの不完全性定理 の例「「$x=Sx$ となる $x$ はない」という文」）。

反例：公理を 1 つ外す

$\mathsf Q$ の公理のうち、和と積の再帰の式 4〜7 以外の 1 つを外すと、thm-q-sigma1 は成り立たなくなる。1 行目は ex-q-model による。2 行目以降の各行の構造は外した公理以外の 7 個を満たし（$<$ は公理 8 を外す行以外では公理 8 の右辺で解釈する）、右の列の真な $\Delta_0$ 文が偽になるので、健全性により残りの公理からその文は証明できない。

外す条件反例成り立たなくなること
thm-q-sigma1 の、文が $\Sigma_1$ であること$\Pi_1$ 文 $\forall x\,(0+x=x)$ と ex-q-model の $M$真な文が $\mathsf Q$ で証明できること
公理 1（$S$ は単射）$\{0,1\}$ で $S(0)=S(1)=1$、和は $\min(x+y,1)$、積は通常の積$\lnot\,\underline1=\underline2$ が証明できること
公理 2（$0$ は後者でない）1 元集合 $\{0\}$ で $S(0)=0$、和と積は $0$$\lnot\,\underline0=\underline1$ が証明できること
公理 3（$0$ 以外は後者）$\mathbb N$ に新しい元の列 $c_0,c_1,\dots$ を加えた構造$\forall x<\underline1\,(x=0)$ が証明できること
公理 8（大小の定義）$\mathfrak N$ で $<$ を空の関係に替えたもの$\underline0<\underline1$ が証明できること
反例の確かめ
各行の確かめを開く

1 行目：ex-q-model のとおりである。

2 行目：公理 2（$S(x)=1\ne0$）、3（$0$ でない元は $1=S(0)$）、4・6 は明らかである。公理 5：$x+S(y)=\min(x+1,1)=1=S(x+y)$。公理 7：$x\cdot S(y)=x$ で、$x\cdot y+x$ は $x=0$ なら $0$、$x=1$ なら $\min(y+1,1)=1$。$\underline1=S(0)=1$、$\underline2=S(1)=1$ なので $\underline1=\underline2$ が成り立つ。

3 行目：$S(0)=0$ は単射で、$0$ でない元はないので公理 3 は自明に成り立ち、4〜7 は $0=0$ である。$\underline1=S(0)=0$ なので $\underline0=\underline1$ が成り立つ。

4 行目：$n\in\mathbb N$ について $\lvert n\rvert:=n$、$\lvert c_k\rvert:=k$ とおき、$S(n)=n+1$、$S(c_k)=c_{k+1}$、$x+y:=S^{\lvert y\rvert}(x)$（$S$ を $\lvert y\rvert$ 回）、$x\cdot y:=m_{\lvert y\rvert}(x)$（$m_0(x):=0$、$m_{j+1}(x):=m_j(x)+x$）と定める。$S$ は単射で $0$ を値にとらず（公理 1・2）、$\lvert0\rvert=0$、$\lvert Sy\rvert=\lvert y\rvert+1$ から公理 4〜7 が成り立つ。$c_0$ は $0$ でなくどの元の後者でもないので公理 3 だけが成り立たない。$S(0)+c_0=S^0(S(0))=\underline1$ なので $c_0<\underline1$ で、$c_0\ne0$ だから $\forall x<\underline1\,(x=0)$ は偽である。

5 行目：公理 1〜7 は $\mathfrak N$ で成り立ち、$<$ が空なので $\underline0<\underline1$ は偽である。

表現可能性と決定不能性

$\Sigma_1$ 完全性は、$\mathsf Q$ を含む理論で計算を扱う議論の土台になる。この記事では証明しないが、次が成り立つ。

$\mathsf Q$ についての主な定理
  1. 計算可能な関数・関係はすべて $\mathsf Q$ で表現可能である（Gödelの不完全性定理 の定義「表現可能性」の意味。OLT26 Theorem 35.2（p. 553）、Theorem 35.29（p. 567））。
  2. $\mathsf Q$ を含む無矛盾な理論は、どれも決定可能でない（OLT26 Theorem 36.5、p. 575）。とくに $\mathsf Q$ 自身が決定可能でない（同 Theorem 35.30、p. 568）。この性質を、$\mathsf Q$ は 本質的に決定不能 であるという。
  3. $\mathsf Q$ を含む無矛盾な理論で、決定可能な公理系をもつものは完全でない（同 Theorem 37.7、p. 585）。

2・3 は、1 と対角化関数の計算可能性を認めれば Gödelの不完全性定理 の定理「Q を含む無矛盾な理論の決定不能性」「第1不完全性定理」で証明されている。$\mathsf Q$ の公理は有限個なので、その連言を $\sigma_{\mathsf Q}$ とすると、$\mathsf Q\vdash\psi$ と「$\sigma_{\mathsf Q}\to\psi$ が妥当」が同値になり、2 から一階論理の妥当性も決定可能でないことが従う（Churchの定理(一階論理の決定不能性)、決定可能な理論 の系「算術の言語の妥当な文」、OLT26 Corollary 35.31、p. 568）。これに対し、積をもたない自然数の和の理論は決定可能である（Presburger算術 の定理「Presburger 算術の決定可能性」）。
thm-q-delta0 のような計算の事実は帰納法なしで証明できるので、不完全性定理は「帰納法が強すぎるから」ではなく、有限の計算を表せることそのものから起こる。一方、ex-q-model が示すように、$\mathsf Q$ は全称的な法則をほとんど証明しないので、算術の定理を実際に展開するには Peano算術 のような帰納法をもつ理論を使う。

参照箇所

  • OLT26 Definition 33.5（p. 524、$\mathsf Q$）。§35.1（p. 552、名前の由来）。Lemmas 35.23–35.24（p. 564、$\lnot\,x< 0$ と $x<\underline{n+1}$ の場合分け）。Definitions 35.32–35.33（p. 569、有界な量化と $\Delta_0$・$\Sigma_1$・$\Pi_1$）、Lemmas 35.34–35.37（pp. 569–570）、Theorem 35.38（p. 571、$\Sigma_1$ 完全性）。Example 26.9（p. 398、和が可換でないモデル）。Theorems 35.2・35.29・35.30・36.5・37.7 と Corollary 35.31（上の rem-q-cited）。

関連項目

参考文献

Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する

Mathpediaを支援する
Robinson算術