Loading article…
「Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I」（「プリンキピア・マテマティカおよび関連体系の形式的に決定不可能な命題について I 」）は、クルト・ゲーデルによる数理論理学の論文である。1930年11月17日に提出され、元々はドイツ語で『Monatshefte für Mathematik und Physik』 1931年版に掲載された。 英語訳がいくつか出版されており、古典的な数理論理学論文集2冊にも収録されている。この論文には、現在では論理学における基礎的な結果であり、数学における無矛盾性証明に多くの示唆を与えるゲーデルの不完全性定理が含まれている。また、この論文は、ゲーデルが不完全性定理を証明するために考案した新しい手法を紹介したことでも知られている。
確立された主な成果は、ゲーデルの第一および第二不完全性定理であり、これらは数理論理学の分野に多大な影響を与えてきた。これらは、本論文ではそれぞれ定理VIおよび定理XIとして示されている。
これらの結果を証明するために、ゲーデルは現在ゲーデル数法として知られる方法を導入しました。この方法では、一階算術の各文と形式的証明に特定の自然数が割り当てられます。ゲーデルは、これらの証明の多くの性質が、原始再帰関数を定義するのに十分な強さを持つ任意の算術理論内で定義できることを示しました。（再帰関数と原始再帰関数の現代的な用語は、この論文が発表された時点ではまだ確立されていませんでした。ゲーデルは現在原始再帰関数として知られるものに対してrekursiv （「再帰的」）という言葉を使用しました。）ゲーデル数法はその後、数理論理学において一般的に用いられるようになりました。
ゲーデル数法は斬新な方法であり、曖昧さを避けるために、ゲーデルはゲーデル数を操作および検証するために使用される原始再帰関数と関係の明示的な形式定義を45個提示した。彼はこれらを用いて、式Bew( x )の明示的な定義を与えた。この式は、 xが文φのゲーデル数であり、かつφの証明のゲーデル数となる自然数が存在する場合に限り真となる。この式の名前は、ドイツ語で証明を意味するBeweisに由来する。
ゲーデルがこの論文で考案した2つ目の新しい手法は、自己参照文の使用である。ゲーデルは、 「この命題は偽である」といった古典的な自己参照のパラドックスが、自己参照的な形式的な算術文として書き換えられることを示した。非公式には、ゲーデルの第一不完全性定理を証明するために用いられた文は「この命題は証明できない」である。このような自己参照が算術の中で表現できるという事実は、ゲーデルの論文が発表されるまで知られていなかった。アルフレッド・タルスキによる不可定義性定理に関する独立した研究はほぼ同時期に行われたが、1936年まで発表されなかった。
脚注48aで、ゲーデルは論文の第二部で無矛盾性証明と型理論との関連性を確立する予定であると述べていた（論文タイトルの末尾にある「I」は第一部を示している）。しかし、ゲーデルは亡くなる前に第二部を発表することはなかった。とはいえ、1958年に『Dialectica』誌に掲載された彼の論文は、型理論を用いて算術の無矛盾性証明を与える方法を示した。
ゲーデルの論文の英語訳は、彼の生前に3つ出版されたが、その過程は困難を伴った。最初の英語訳はバーナード・メルツァーによるもので、1963年にベーシックブックスから単独の著作として出版され、その後ドーバー社とホーキング社から再版された（『神は整数を創造した』、ランニングプレス、2005年：1097頁以降）。レイモンド・スムリアンが「良い翻訳」と評したメルツァー版は、シュテファン・バウアー＝メンゲルベルク（1966年）から否定的な評価を受けた。ドーソンのゲーデルの伝記（ドーソン 1997：216）によると、
幸いなことに、メルツァー訳はすぐにエリオット・メンデルソンがマーティン・デイヴィスのアンソロジー『決定不能なもの』のために作成したより優れた訳に取って代わられた。しかし、この訳もほぼ土壇場までゲーデルの目に触れることはなく、新しい訳も彼の好みに完全に合致するものではなかった。別の訳を検討する時間がないと知らされたゲーデルは、メンデルソンの訳は「概して非常に良い」と述べ、出版に同意した。[後に彼はこの同意を後悔することになる。出版された書籍は、ずさんな活字と多数の誤植によって全体的に損なわれていたからである。]
エリオット・メンデルソンによる翻訳は、アンソロジー『The Undecidable』（デイビス 1965:5ff）に収録されている。この翻訳はバウアー＝メンゲルベルク（1966）からも厳しい批評を受けており、彼は詳細な誤植リストを提示しただけでなく、翻訳における重大な誤りと思われる点についても指摘している。
ジャン・ファン・ヘイエノールトによる翻訳は、『フレーゲからゲーデルへ：数理論理学の資料集』（ファン・ヘイエノールト、1967年）に収録されている。アロンゾ・チャーチ（1972年）による書評では、これを「これまでになされた中で最も綿密な翻訳」と評したが、同時にいくつかの具体的な批判も述べている。ドーソン（1997年：216）は次のように述べている。
ゲーデルが好んだ翻訳は、ジャン・ファン・ヘイエノールトによるものだった。ファン・ヘイエノールトは、その本の序文で、ゲーデルは自身の作品の翻訳を自ら読んで承認した4人の著者のうちの1人であると述べている。
この承認プロセスは骨の折れるものだった。ゲーデルは1931年の原稿に修正を加え、両者の交渉は「長引いた」。「ファン・ヘイエノールトは個人的に、ゲーデルは自分がこれまで知っている中で最も頑固で几帳面な人物だと述べている」。両者は「合計70通の手紙をやり取りし、ドイツ語と英語の単語の意味と用法の微妙な違いに関する問題を解決するために、ゲーデルのオフィスで2回会った」。（ドーソン 1997:216-217）。
原著論文の翻訳ではないものの、非常に有用な第4版が存在し、「ゲーデルの1931年の決定不能性に関する原著論文で扱われた内容と非常によく似た領域を扱っている」（Davis 1952:39）とともに、ゲーデル自身によるこのトピックの拡張と解説も含まれている。これは『形式数学体系の決定不能な命題について』（Davis 1965:39ff）として出版されており、1934年にニュージャージー州プリンストンの高等研究所でゲーデルが行った講義を、スティーブン・クリーネとJ・バークレー・ロッサーが書き起こしたものである。この版には、2ページの正誤表とゲーデルによる追加の訂正がデイビスによって加えられている。この版は、ゲーデルが再帰の（一般的な、すなわちヘルブランド＝ゲーデルの）形式を生み出したヘルブランドの提案を初めて記述している点でも注目に値する。