Finite Groups Fun 有限群 あるいは ちょこっと計算ファンの日記 このページをアンテナに追加 RSSフィード

2011-10-19

数学基礎論講義をこっそり読む(その7)

Part Bに入りました。いよいよ算術です。なぜか新井敏康著『数学基礎論』ではPAオンリーでロビンソンの算術Qは出てきません。

算術Qで不思議なのはやはり、p.69の でしょうか。公理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)

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


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


Qの超準モデルの作り方:


領域として、普通の自然数の集合¥mathbb{N}に2つの異なる点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)は成立していない。(ちなみにn<A,n<Bが成立しており、A,Bは無限大のようなものと考えられる。ただし、A<B,B<Aも成立しており、< は実は順序関係になっていない。)

とまあ、このモデルを見る限り、「一般化された問題が解けない小学生」というよりも「超準元をうまく統制できていない管理職」という感じでしょうか。超準元を排除するような公理があればいいのですが…それは少なくとも一階論理ではできないらしい…

また、¥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)が証明できればよい。



より、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).



Q¥vdash ¥forall x(x=0¥vee ¥neg(0<x)の証明:


0<xは定義により、¥exists y (x=S(y)+0)すなわち¥exists y(x=S(y))である。



また、次の公式を(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). □

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/kazu_FGF/20111019/1319036528