第１不完全性定理 公理系ＰＡ

　不完全性定理を始めて勉強するなら、「数学ガール」第３巻がおすすめです。ミルカさんがやさしく指導してくれて、テトラちゃんが一緒に悩んでくれて、ユーリちゃんが鋭い直観的指摘をしてくれます。

数学ガール/ゲーデルの不完全性定理 (数学ガールシリーズ 3)

さて新井先生の「数学基礎論」は第３章、不完全性定理です。

不完全性定理は算術を含む公理系についての定理です。
本で紹介されているのは、

第１不完全性定理
公理系ＰＡが無矛盾であるならば、ＰＡは不完全：
φのＰＡでの証明も、¬φのＰＡでの証明も存在しないような閉論理式φがつくれる。

ＰＡは自然数の算術を含む公理系なのですが、このＰＡとは何なのかをまとめてみます。

公理系とは、関数記号や関係記号の集合である言語Ｌがまず定義されたときに、Ｌ-閉論理式の集合のことでした。簡単に言うと「文」の集合なのですけど、「文」とは何かについて形式的に定義したのでした。

公理系ＰＡは、
・証明体系Ｈ
・原始再帰的関数の関数記号たち
・数学的帰納法の公理
からなります。

公理系ＰＡを決めるための言語は、
・証明体系Ｈで出てきた→,⊥,∃,＝,あと無限個の変数記号
・原始再帰的関数全体と１対１で対応している関数記号の皆さん
ですが、関数記号の皆さんを決めるためには、原始再帰的関数たちをコード化していかなくてはなりません。
どういう方法でもいいのですが、要点は原始再帰的関数がコード（つまり自然数）eによって[e]と書かれ、異なる関数には異なるコードが割り当てられていればとりあえずオッケー。
原始再帰的関数全体の集合をＰＲとすると、関数記号の皆さんは

と書けます。
言語に定数記号を特別に入れる必要はありません。自然数０、１、２、…は、ゼロ関数0と後者関数Scによって、0、Sc(0)、Sc(Sc(0))、…と表せるので、それらに対応するコードによって、自然数の関数記号が与えられます。

公理系ＰＡの公理は、
・証明体系Ｈの公理（命題論理の公理、等号公理、量化公理）
・関数記号の公理。各原始再帰的関数[e]の定義式を１階論理で表したモノ。
・数学的帰納法の公理
になります。

そうすると、
　　
自然数の集合Ｎが、公理系ＰＡの標準モデルとなります。つまりＰＡは算術を形式化したものなんですね。

ＰＡを使って何ができるか。

１．自然数に関する原始再帰的関数や述語をＰＡの論理式に写し取ることができる
２．ＰＡの論理式をコード化して、自然数に写し取ることができる

１と２から、ＰＡは自己言及する命題を扱えるようになります。
第１不完全性定理は、自己言及する命題
Ｐ「Ｐは証明不能である」
を作ることで証明されますが、ＰＡはそれを表現するのに十分な記述力をもっているということなんですね。