数学基礎論講義をこっそり読む（その７） - Finite Groups Fun 有限群あるいはちょこっと計算ファンの日記

Part Bに入りました。いよいよ算術です。なぜか新井敏康著『数学基礎論』ではPAオンリーでロビンソンの算術Qは出てきません。
算術Qで不思議なのはやはり、p.69の $Q\nvdash\forall x (0+x=x)$ でしょうか。公理A4で $\forall x (x+0=x)$ があるので、これは加法の交換法則の特殊なもの $\forall x (0+x=x+0)$ すら成立していないことも意味しています。
$\forall x (0+x=x)$ が証明できないことを示すには超準モデルを作ります。このモデルは次の本を参考にしました。（別の形の反例のモデルが田中一之著『数の体系と超準モデル』にもありました。うわ、これのamazon.co.jpでの中古本の値段がすごいことに…復刊ドットコム行きになってますね。がんばれ裳華房さん！）

An Introduction to Goedel's Theorems (Cambridge Introductions to Philosophy)

作者: Peter Smith
出版社/メーカー: Cambridge University Press
発売日: 2007/07/26
メディア: ペーパーバック
クリック: 10回
この商品を含むブログ (2件) を見る

私もこの本をつい先日入手したばかりで目を通した内にも入ってませんが、定義や証明の背景について饒舌に語ってくれているようです。しかし、侮るなかれ、証明は省略はあるもののそれなりにしっかりしていて、ちまたのゲーデル理論解説本とは一線を画し、数学書と言ってもいいぐらいです。著者自身が前書きで『本書のちょっとくだけた語りに惑わされて、いそいでななめ読みしようとするなかれ』と警告していて、じっくり読むようにと勧めています。amazon.comでの評判も高く、副読本によさげです。

$Q$ の超準モデルの作り方：

領域として、普通の自然数の集合 $\mathbb{N}$ に２つの異なる点 $A,B$ を付け加えた集合とする。以下、自然数に値をとる変数を $n$ とし、一般に何でも取りうる変数を $x$ とする。

$S$ については、 $S(n)=n+1$ , $S(A)=A$ , $S(B)=B$ と定義する。

足し算は、整数については通常の加法とし、 $A+x=A$ , $B+x=B$ , $n+A=B$ , $n+B=A$ と定義する。

掛け算は、整数については通常の乗法とし、 $A\cdot x=A$ , $B\cdot x=B$ （ただし、 $x=0$ のときは $A\cdot 0=B\cdot 0=0$ とする）, $n\cdot A=A$ , $n\cdot B=B$ と定義する。

この様に定義すると、このモデルはQの公理をすべて満たすが、 $0+A=B$ となっており、 $\forall x (0+x=x)$ は成立していない。（ちなみに[tex:n

とまあ、このモデルを見る限り、「一般化された問題が解けない小学生」というよりも「超準元をうまく統制できていない管理職」という感じでしょうか。超準元を排除するような公理があればいいのですが…それは少なくとも一階論理ではできないらしい…
また、 $\neg\forall x (0+x=x)$ は標準モデルで成立しないので、結局 $\forall x (0+x=x)$ は、肯定も否定もQでは証明できない命題になっています。

定理5.1は、項の等式について以前に気にしていたことに関連することで、私の思い込みでなくてよかったという感じです。

最後に定理5.2についてのメモです。

$Q\vdash \forall x\neg(x<0)$ の証明：

$x<0$ の定義により、任意の $x$ , $y$ について、 $\vdash \neg(0=S(y)+x)$ が証明できればよい。

$\frac{\displaystyle\frac{\displaystyle\frac{x=S(z)\quad [0=S(y)+x]_{1}}{0=S(y)+S(z)}}{0=S(S(y)+z)}\quad \frac{\forall x \neg (S(x)=0)\quad \mbox{:A2}}{\neg(S(S(y)+z)=0)}}{\displaystyle\frac{\bot}{\neg(0=S(y)+x)}\quad 1}$

より、 $x=S(z)\rightarrow \neg(0=S(y)+x)$ . これの対偶をとって、 $0=S(y)+x \rightarrow \neg(x=S(z))$ . さらに $z$ について一般化して、 $0=S(y)+x \rightarrow \forall z \neg(x=S(z))$ . これの対偶をとると $\exists z (x=S(z))\rightarrow \neg(0=S(y)+x)$ .

[tex:Q\vdash \forall x(x=0\vee \neg(0

また、次の公式を(2-2)の証明中に使うと便利です。

$Q\vdash \forall x(x+\bar{m} = \overbrace{SS\cdots S}^{m}(x) )$ の証明：

$m$ に関する帰納法。 $m=0$ のときは $x=x$ なので成立。
$m+1$ のとき、 $x+\bar{m+1}=x+S(\bar{m})=S(x+\bar{m})=S(\overbrace{SS\cdots S}^{m}(x))=\overbrace{SS\cdots S}^{m+1}(x)$ . □