ゲーデルの不完全性定理

ゲーデルの不完全性定理の証明のアイデアが知りたいと思い、適当な入門書(基礎論の教科書ではないです。)を読んでいるのですが、

まず、定理の主張が「形式的体系Tで通常の自然数を含み、強い意味で無矛盾であり、そこにおける公理や推論規則は帰納的に定義されているかまたはその数が有限であるようなもの、においては文GでGも￢Gも証明できないものが存在する。」

とあるのですが、形式的体系Tがなにを意味しているのかがよくわかりません。これは、形式的と書いてあるのだから文字通り「意味を考えない記号の世界(記号の集まりと、記号を並べて得られる列を変形するいくつかの規則)」と考えればよいのでしょうか？

それで、もう一つ質問があるのですが、

まず、準備として記号
￢,∧,∨,→,∃,∀,(,),0,',+,×,=,x,y,zを用意して、
x,y,zを変数記号と呼びます。

それで、項を次のように定義します。
(i) 0,x,y,zは項。
(ii) t,sが項であるとき、'(t),+(t,s),×(t,s)は項。
(iii)このようにして得られるものだけが項。
(iV)'(t),+(t,s),×(t,s)を簡単にそれぞれt',t+s,t×sと記したりする。また、0',0'',0''',…をそれぞれ1,2,3,…と記す。
また、項tを上の記号の括弧としてではなく、見易さのための補助記号としての(,)を用いることにより、しばしばt(x,y,z)と記したりする。

次に論理式を次のように定義します。
(i)t,sが項のとき、t=sは論理式。
(ii)φとψが論理式でxが変数記号のとき、(￢φ),(φ∧ψ),(φ∨ψ),(φ→ψ),(∀xφ),(∃xφ)は論理式。
(iii)このようにして得られるもののみが論理式
(iV)見易さのために括弧を適当に省略して論理式を記すこともある。

以上により、与えられた記号列が項か論理式かそれ以外のものか判定できるようになります。

準備した記号￢,∧,∨,→,∃,∀,(,),0,',+,×,=,x,y,zを普通に解釈することで、論理式の意味を考えることができるようになります。
ただし、'は後者関数と解釈します。

次に、￢,∧,∨,→,∃,∀,(,),0,',+,×,=,x,y,zに
素数2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53を割り当てます。
記号列が与えられたとき、各記号を上記の対応に従い素数n_1,n_2,n_3,…に置き換え、2^(n_1)*3^(n_2)*5^(n_3)*…を対応させます。対応する数をゲーデル数と呼びます。

以上で準備は終わりで、
質問ができるのですが、

「mがTのある論理式のゲーデル数である」という非形式的な主張は
mを素因数分解して各素数の指数を調べることである論理式のゲーデル数であるかどうかがチェックできるので、解釈すると「mがTのある論理式のゲーデル数である」という意味になる論理式が作れる、とあるのですが"具体的"にはどのようにして作るのでしょうか？
私は、論理式の定義が再起的であるから、「mがTのある論理式のゲーデル数であるかどうか」をコンピュータに判定させること(とてつもなく時間がかかりそうですが)可能だと思うので上のような論理式は作れると思うのですが、実際に作るとどんな論理式になるのか興味があります。

No.5 回答者： vba5129 回答日時： 2008/04/20 23:59

細かい点に間違いがあるかも知れませんがご容赦ください。

またご指摘頂ければ幸いです。
「自然数mが論理式のゲーデル数である」という命題はpを素数とすると，mを素因数分解したときのpの指数を調べなければなりませんので，次の命題を形式化しなければならないはずです。
「pが素数である」
「mを素因数分解したときのpの指数がnである」

最初の方は簡単だと思われますので，後者の方を少しだけ述べます。
準備として,次の命題がそれぞれ右の様に形式化できます。
a|b（自然数bが自然数aで割り切れる） : ∃c (a×c=b)
自然数bが自然数aで割り切れ,商がcである：a×c=b
a<b ： ∃c ( S(c) + a = b )

これから「mを素因数分解したときのpの指数がnである」という命題を形式的に表現しますが，まずその方針を述べます。mが何回pで割り切れるかを調べれば良いのですが，簡単の為pがmの素因数でない場合を省いて考えます。
　t, a_1, a_2, ... , a_t が存在し
　m=a_1, a_1=p×a_2, a_2=p×a_3, .. ,a_i=p×a_(i+1), ... ,a_(t-1)=p×a_t であり
　￢(p|a_t)のとき，
　t-1 が求める指数になりますね。

ここで次の事実を用います。

ゲーデルのβ関数と呼ばれる3変数関数β(c,d,i)があって（2変数のものもあるようです），
命題 a=β(c,d,i) は体系内の論理式として表現でき，
任意の自然数の有限列 t, a_1, a_2, ... ,a_t に対して，ある自然数c,dが存在し
t = β(c,d,0), a_i = β(c,d,i) (for all i ≦ t)
となる。

これを用いますと，
∃（t,a_1,a_2,...,a_t）と書くことが体系内で出来なくても
∃c ∃d ( m=β(c,d,0) ∧ ∀i ( i<t → β(c,d,i) = p×β (c,d,i+1)) ∧ (n+1=t) )
と書くことによって求める命題が体系内で表現できたことになります。

目的の「自然数mが論理式のゲーデル数である」という命題ですが，論理式を構成しているのは述語「　=　」とその両辺の項が基本ですから，まず，「自然数mが項のゲーデル数である」という命題を term(m) とするとき，これを表現する必要があると思われます。項というのは ((x+y)×(S(S(z))))の様に構成されるものですから，n<t なるnについて term(n)が定義されたとすると，nの表す記号列を[n]で表すと，
term(t) :
　t は それ自身新しい変数のゲーデル数であるか，
　∃r ( r<t ∧ term(r) ∧ tは記号列(S([r]))のゲーデル数) であるか，
　以下同様

の様にすれば良いと思われます。この様に帰納的に定義されている場合β関数を用いて表現できそうです。

これが問題なければ，目的の「自然数mが論理式のゲーデル数である」という命題も同様の手法で表現できると思われます。

No.4 回答者： tgb 回答日時： 2008/03/21 21:17

たびたびの誤りで申し訳ありません。

以下のように訂正をお願い致します。

C2:
(b∈R)
→
(　　　　　　　　-------->(b∈K)∨を削除、以下でａをｂに変更
(∃f∃g(
((f∈K∧g∈K)∧((b=[f=g])))
∨((f∈R∧g∈R)∧
((b=[f∧g])∨(b=[f∨g)])∨(b=[f→g])∨(b=[￢f]))
∨((f∈H∧g∈R)∧
((b=[f∀g])∨(b=[f∃g])) -------->[f∃g)]を[f∃g]に変更
))
)

No.3 回答者： tgb 回答日時： 2008/03/21 11:56

誤りに気づいたので申し訳ありませんが訂正させて頂きたいと思います。

(1)全論理式の集合を定義してこれを利用するもの
において前回のK、Rでは
[(iii)このようにして得られるものだけが項(論理式)]
と言う条件が考慮されていない事になります。
これを考慮するためには、以下のように変更すればよいと思います。
(もっとうまい方法があるかも知れませんが、ここでは、単純に余分な要素を含ませないような操作を追加しています)


C1:
(a∈K)
→
((a∈H)∨
(∃f∃g(
((f∈K∨f∈H)∧(g∈K∨g∈H))∧
((a=['(f)])∨(a=[+(f,g)])∨(a=[X(f,g)]))
))
)
C2:
(b∈R)
→
((b∈K)∨
(∃f∃g(
((f∈K∧g∈K)∧((a=[f=g])))
∨((f∈R∧g∈R)∧
((a=[f∧g])∨(a=[f∨g)])∨(a=[f→g])∨(a=[￢f]))
∨((f∈H∧g∈R)∧
((a=[f∀g])∨(a=[f∃g)]))
))
)
記号列を[]で囲んでいます。
言葉で説明すると、例えばC1については、
K(項)に余分なものを紛れ込ませないために最小の記号列の場合にはHに属するよう制約を設けています。最小でない場合は必ずより小さなK内の記号列を使って規則で許されているパターンのいずれかで表されるとしています。最小であるか否かは単純に２つのケース(最小or最小でない)を"∨"で結んでおけば自動的にどちらかに割り振ってもらえるとしています。C2についても同様な考え方です。



求める論理式は
∃K∃R∀x∀y∀u∀v∀a∀b∀Φ((t∈R)∧K0∧K1∧K2∧K3∧R0∧R1∧R2∧R3∧R4∧R5∧R6∧C1∧C2)

※f,gはa,bに依存して決まります。

No.2 回答者： tgb 回答日時： 2008/03/19 22:38

＞「作れる論理式は」は「Tでの論理式全体」にかかっているのですか？

＞それとも、「何でも良く特別のものではありません。」にかかっているのですか？
両方にかかっているつもりでした。
しかし、誤解に基づいていたので今となっては意味を成しません。
誤解の根本は
「mがTのある論理式(a)のゲーデル数である」という意味になる論理式(b)が作れる
の中の論理式に対し、私は
a=bで共にTの中での論理式と考えていました。おまけに、
「mがTのある論理式(a)のゲーデル数である」という[ような](<--[意味になる])論理式(b)が作れる
と修正解釈してしまいました。
このような解釈には無理があるようで、回答するときもご質問の意図がはっきりしないと考えていました。この場合、問題が単純になるので質問者さんが何か勘違いしている可能性があると考えたのですが、私の誤りでした。お礼欄を読んで、御質問の趣旨が論理式(b)はT内と言う事ではなく、「mがTのある論理式(a)のゲーデル数である」と言う内容を一般的な意味での論理式(即ち論理式(b))で表現できないかと問うている事が理解できました。


そこで、改めて本題ですが、
「mがTのある論理式(a)のゲーデル数である」
と言うのは数値と記号列の変換がゲーデル数の考えにより一意に変換できる事を考えると
「ｔがTのある論理式である」
と置き換えてこれを論理式(b)で表現する問題に置き換えても本質的には同じでしょう。
(ゲーデル数のアイデアが秀逸で上の変換が簡単になるようになっている)
以下では、この変更された問題を考えてみます。

先ず論理式での表現として様々な方法があるだろうと思われます。
質問者さんはすっきりした表現を望んでおられると思いますが、そういう訳にも行かず、どうにか思いついたものを書いてみます。

(1)全論理式の集合を定義してこれを利用するもの
ｍに対応する記号列をｔとします。
H=｛0,x,y,z｝
K0：(u∈H)→(u)∈K
K1：(u∈K)→('(u))∈K
K2：(u∈K∧v∈K)→(+(u,v))∈K
K3：(u∈K∧v∈K)→(X(u,v))∈K
R0：(x∈K∧y∈K)→(ｘ＝ｙ)∈R
R1：(x∈R∧y∈R)→(ｘ∧ｙ)∈R
R2：(x∈R∧y∈R)→(ｘ∨ｙ)∈R
R3：(x∈R∧y∈R)→(ｘ→ｙ)∈R
R4：(x∈R)→(￢ｘ)∈R
R5：(x∈H∧Φ∈R)→(∀xΦ)∈R
R6：(x∈H∧Φ∈R)→(∃xΦ)∈R
　　※以上では論理式と記号列がごっちゃになっていますのでご注意！
　　(最左の→の右側の()内が記号列です)

∃K∃R∀x∀y∀u∀v∀Φ((t∈R)∧K0∧K1∧K2∧K3∧R0∧R1∧R2∧R3∧R4∧R5∧R6)
これは実質的には再帰的にKおよびRを定義してそのRに対してt∈Rであるとしています。
UとKを一緒くたにして定義しているのが気持ち悪いので何らかの改良を加えた方がよいかも知れません。

(2)与えられた記号列が論理式である事を判定する関数を定義してこれを利用するもの
関数を利用した表現を考えてみます。
記号列ｔを与えて論理式であるかどうか判定して1(論理式の場合)または0(論理式でない場合)を
返す関数Fを再帰的に定義し、
F(t)=0
を論理式とします。
先ず"(",")"は省略を許さないものとします。省略があるなら前もって省略のない記号列に変換しておく事を前提として考える事にします。
●項に関する関数K(t)について
K(t)をtの判定ノより1(項である場合)または0(項でない場合)を
返す関数とします。
ｔのいちばん外側の括弧に着目して
1：t='(tn)の場合
2：t=+(tl,tr)の場合
3：t=X(tl,tr)の場合
0：上のいずれでもない
に分類されます。
0の場合：
　tが0,x,y,zのいずれかならK(t)=1
　そうでなければK(t)=0
1の場合：
　ｔからtnを取り出して
　K(tｎ)=0ならK(t)=0
　K(tｎ)=1ならK(t)=1
2,3の場合：
　ｔからtl,trを取り出して
　K(tl)=1かつK(tr)=1ならK(t)=1
　そうでないならK(t)=0
●次にK(t)を利用して論理式に関する関数F(t)を定義します。
ｔのいちばん外側の括弧に着目して
1：t=￢(tn)の場合
2：t=(tl∧tr),t=(tl∨tr),t=(tl→tr)の場合
3：t=(∀x(tn)),t=(∃x(tn))の場合
4：t=(tl=tr)の場合
0：上のいずれでもない
に分類されます。
0の場合：
　F(t)=0
1,3の場合：
　tからtnを取り出してF(tn)=1ならF(t)=1
　そうでなければF(t)=0
2の場合：
　ｔからtl,trを取り出して
　F(tl)=1かつF(tr)=1ならF(t)=1
　そうでないならF(t)=0
4の場合：
　ｔからtl,trを取り出して
　K(tl)=1かつK(tr)=1ならF(t)=1
　そうでないならF(t)=0
●以上でF(t)が定義できたのでこのように定義された関数に対し、
　F(t)=1
　が論理式となります。

No.1 回答者： tgb 回答日時： 2008/03/18 22:08

以下のコメントは質問に関連した深い知識に基づいて書いたものではなく、質問文の内容に基づいて考えられる事を書いたものです。

＞実際に作るとどんな論理式になるのか興味があります
とありますが、作れる論理式はＴでの論理式全体ということであって、論理式の生成規則に従って作られるものであれば何でも良く特別のものではありません。と言うか、記号列全体の集合を自然数の部分集合(ゲーデル数からなる集合)に対応させるのがゲーデル数の考え方のようです。論理式になるかならないかはｍがゲーデル数であることをチェックした上で(ｍに対応する論理式があるための必要条件)、更にｍがゲーデル数であるならｍに対応する記号列が一意に決定できるのでその記号列が論理式としての条件を満たすか否か論理式の生成規則に照らし合わせるチェックを重ねて行う事によって決定されると思います。

・自然数の集合　<-->　？？？
・ゲーデル数の集合　<-->　記号列全体の集合
・対応する論理式が存在するようなゲーデル数の集合　<-->　論理式となる記号列の集合

自然数ｍが与えられたとき、
ｍがゲーデル数であるか否かは素因数分解により簡単に(アルゴリズムとして簡単に)チェックできます。
ｍがゲーデル数ならそれに対応する記号列が決まります(その記号列は先の素因数分解によりそのまま記号列に置き換えられます)。
記号列をチェックする事によりその記号列が論理式であるか否かが決定されます。

例えば、
例１：
　ｍ＝２＾２３・３＾４１・５＾２３
はゲーデル数である事が分かり、対応する記号列は
　０＝０
です。この記号列は論理式の生成規則に照らして論理式である事が分かります。
(論理式の生成規則によって生成される任意の論理式に対してゲーデル数が計算でき、
論理式から計算されるゲーデル数に対応する記号列としては元の論理式が得られます。)
例２：
　ｍ＝２＾２３
はゲーデル数であり、対応する記号列は
　０
となりますが論理式ではありません。
例３：
　ｍ＝３＾４１
　ｍ＝２＾２４
はいずれもゲーデル数でなく、対応する記号列は存在しません。

この回答へのお礼

ありがとうございます。

＞作れる論理式はＴでの論理式全体ということであって、論理式の生成規則に従って作られるものであれば何でも良く特別のものではありません。

おっしゃっていることの意味がよくわかりません。

「作れる論理式は」は「Tでの論理式全体」にかかっているのですか？
それとも、「何でも良く特別のものではありません。」にかかっているのですか？

前者だとして解釈すると、論理式(記号列)がTでの論理式全体　となってしまい意味がわかりません。後者だとして解釈すると、

＞実際に作るとどんな論理式になるのか興味があります

の答えになっているとは思えません。

もう少しわかりやすく説明してもらえると助かります。

私の「実際に作るとどんな論理式になるのか興味があります」の意味は、

論理式Pを実際に作ったときの記号列に興味がある。ただしPを解釈すると「mがTのある論理式のゲーデル数である」という意味となるものとする。

ということです。


＞自然数ｍが与えられたとき、
ｍがゲーデル数であるか否かは素因数分解により簡単に(アルゴリズムとして簡単に)チェックできます。
ｍがゲーデル数ならそれに対応する記号列が決まります(その記号列は先の素因数分解によりそのまま記号列に置き換えられます)。
記号列をチェックする事によりその記号列が論理式であるか否かが決定されます。

この作業が(コンピュータにも行えるという意味)でルーチンであるから、上の論理式Pが作れると思ったわけです。

つまり、∃p_1∃p_2…∃p_n　各p_iは素数で　m=2^(p_1)*3^(p_2)…
さらにp_1,p_2,…,p_nはある規則にしたがっている。

みたいな論理式(ただし「素数」とか「ある規則」とか言う言葉は「素数を意味する論理式」「その規則を意味する論理式」を使うことで、"きちんと"書けば記号列で表記できる。その意味でここでは論理式と言っている)でPが表わされると思います。

お礼日時：2008/03/19 03:18