ゲーデルの不完全性定理
ゲーデルの不完全性定理の証明のアイデアが知りたいと思い、適当な入門書(基礎論の教科書ではないです。)を読んでいるのですが、
まず、定理の主張が「形式的体系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のある論理式のゲーデル数であるかどうか」をコンピュータに判定させること(とてつもなく時間がかかりそうですが)可能だと思うので上のような論理式は作れると思うのですが、実際に作るとどんな論理式になるのか興味があります。
補足
コメントをありがとうございます。ゲーデルが、「自己の無矛盾性を証明できない、自然数を包括する公理体系」というのは、有限finitary体系ではないのでしょうか？ 確かに、自然数を無限に包括することの無限性はありますが、その一方で、自然数である限りの有限的様態もつきまとっていますよね？