ゲーデルの不完全性定理を直観的に理解しようと思ったら、少なくとも2つのことが必要だと「まといのば」では考えます。
1つは「全ての論理式の集合が可算集合であることを示す」。
もう1つはカントールの対角線論法です。
逆に言えば、これほどまでに直観的でシンプルな方法があることを知ると、「嘘つきのパラドックス」の先へ行きたくなります（なりますよね？ｗ）。
「嘘つきのパラドックス」がいかにゲーデルの不完全性定理かについては、御本人が原論文で書いています（それもおそらく幾度も紹介しています）。
形式化っぽく書くと、
（嘘つきのパラドックス）＝（ゲーデルの不完全性定理）
です。
引用しましょう！！
どんな認識論的パラドックスも、決定不能命題の存在論の同様な証明に使える（クルト・ゲーデル）
たとえば、最近、盛り上がっている「嘘つきのパラドックス」という自己言及命題についても同様です。
これはゲーデルの不完全性定理の論文の中で、ゲーデル先生自身が「関わる」と言っているものです。
いやいや、もっとはっきりとは、こう書いています。
どんな認識論的パラドックスも、決定不能命題の存在論の同様な証明に使える（クルト・ゲーデル）
これについては原論文を参照せずに又聞きの又聞きにも関わらず、ドヤって批判してくる方が絶えないので、一応反論しておきます。
ゲーデルの不完全性定理の論文を猛烈に圧縮すると以下の通りとなります。冒頭と巻末の付記からの引用です（寺子屋「ゲーデルの不完全性定理」のレジュメにも載せています）。
どんな形式体系も、論理式は外見上、原子記号（変項、論理記号、括弧、句読点）の有限列であり、どの記号列が意味ある論理式であるか否かを正確に記述することは容易である。同様に、証明は、形式上（ある特定の性質をもつ）論理式の有限列に他ならない。もちろん、メタ数学的な考察においては、原始記号そのものがどんなものかは重要ではなく、われわれはこの用途に自然数を割り当てることにする。
すると、論理式は自然数の有限列、証明は自然数の有限列の有限列となる。こうしてメタ数学的概念（や命題）は、自然数や自然数の列についての概念（や命題）になる。（略）さて、以下では、体系PMで決定不能な命題、つまりAもnot-Aも証明できない命題Aを構成する。（略）以上の議論がリーシャルのパラドックスと類似していることが注目される。「うそつきのパラドックス」とも密接に関わっている。（脚注１４どんな認識論的パラドックスも、決定不能命題の存在論の同様な証明に使える）（略）
附記
（略）その後の発展の結果、とくにA.M.チューリングの仕事のお陰で、いまや形式体系の一般概念について厳密で、疑いなく妥当な定義が得られるようになり、それにより定理ⅥとⅪの完全に一般的な表現が可能になった。すなわち、つぎのことが厳密に証明される。ある程度の有限的算術を含むどんな無矛盾な形式体系にも決定不能な算術命題が存在し、さらにそのような体系の無矛盾性はその体系において証明できない。
『プリンキピア・マテマティカ』およびその関連体系における形式的に決定不能な命題について』
c.f.ゲーデルは不完全性を、チューリングは計算不可能性を、チャイティンはランダム性を発見した。 2018年04月21日
だからこそ、T理論では不完全性定理のワークとして「嘘つきのパラドックス」のワークをさせるのです。
そしてこれが内面化されないと、不完全性定理を実装できません（少なくともヒーラーは実装する必要があります）。
「ああ、それ、知っている」というふんわりとした感想だけでは不十分なのです。
「その踊りを知っています、見たことがあります」、というのと、「踊ったことがあります」というのでは大きく違いますよね。
踊ったことがある人々は、次の発言の違和感に気付けるのです。
（これは典型的な間違いです。そもそも自己言及パラドックスについて語るのに、最初から断定していることにおかしいと気付かないのが面白い）
Aさんは「私は嘘つきだ」と言ったから、Aさんは嘘つきだ。
論理学の命題としてはではなく、自然言語の文脈では、これは問題ありません。
（嘘つきがカミングアウトのときだけ正直者になるというラッセル的な抜け道を用意するのです）
ただ、論理学としては、厄介なパラドックスを生じさせるのです。
やはり原典というのは非常にシャープですね。
シャープにいろいろなことを明晰判明に説明します。
シャノンもそうでしたし、いま思いつくところで言えばリーマンもそうですし、ニュートンもそうですが、天才たちはあまりに難解なことをあまりに器用な手際で料理し紹介してくれます。僕らは圧倒されるのみです。
論理式は自然数の有限列、証明は自然数の有限列の有限列となる
ゲーデル先生のお言葉を整理すると、
・どんな形式体系も、論理式は外見上、原子記号（変項、論理記号、括弧、句読点）の有限列
・どの記号列が意味ある論理式であるか否かを正確に記述することは容易
・証明は、形式上（ある特定の性質をもつ）論理式の有限列
なるほどと唸らされます。
記号論理学を学んだ人は論理計算というのを延々とやらされた記憶があると思うので、この「証明は、形式上（ある特定の性質をもつ）論理式の有限列」というのはピンと来るでしょう。
形式上、式の有限列なのです。
でも、これは四則演算を子供の頃にやらされた我々であれば、計算とは形式上、ある特定の性質を持つ式の有限列と言えることが分かりそうです。
１＋（２＋５）×３ー５４÷３
というような式（問題）があったときに、
おそらくは以下のように1行ずつ解いていくでしょう。それは式の有限列として認識されます。
１＋（２＋５）×３ー５４÷３
＝１＋７×３ー１８
＝１＋２１−１８
＝２２ー１８
＝４
という感じです。
これが、「証明は、形式上（ある特定の性質をもつ）論理式の有限列」の風景です。
証明とは（論理）計算のことです。
これらの前提を踏まえて、ゲーデル数化が始まります。
メタ数学的な考察においては、原始記号そのものがどんなものかは重要ではなく、われわれはこの用途に自然数を割り当てる
この原子記号に自然数を割り当てることで、そして素因数分解の一意性を利用することで、「すべての論理式からなる集合が高々可算集合であること」を示すのです。
戸田山先生の「論理学をつくる」を用いて、その方法を示します。
本当は引用したいのですが、あまりに次数の表示などがここではできないので、概要を。
まず、論理式をつくる語彙のそれぞれに奇数を順に当てます（その割当を関数gで表します）。
（・・・３
）・・・５
¬・・・７
∧・・・９
∨・・・１１
→・・・１３
↔・・・１５
そして、命題です。
P・・・１７
Q・・・１９
R・・・２１
と。
で、これをｇを用いて表すと、
ｇ（（）＝３、ｇ（））＝５，ｇ（¬）＝７，ｇ（∧）＝９、ｇ（∨）＝１１、、、、
となります。
で、これらの記号を並べた記号の有限列に自然数を割り当てます。
ｇ（a₁a₂....an)=2^g(a₁) ・３^g(a₂)・・・・Prn＾g(an)
ただしここでPrnはｎ番目の素数！
そうすると、¬Pはこうゲーデル数化されます。
¬Pは（関数ｇで表すと）g（¬P）なので
g（¬P）＝２＾g（¬）・３＾ｇ（P）＝２⁷・３＾17
となります。これを解く気にはなれませんが、何らかの大きな自然数が導き出されて、それがゲーデル数となります。
ちなみにGoogle先生によれば、16,569,286,704 （165億6928万6704）だそうです。
もう一つ！
ｇ（P→Q）＝２^ｇ（P)・３^g（→）・５^g（Q）＝2^17・３^13・5^19
となります。
これを解く気にはなれませんが、何らかの大きな自然数が導き出されて、それがゲーデル数となります。
ちなみにGoogle先生によれば、、、、、 この値は3,985,807,500,000,000,000,000,000 です。
事程さように、ともかくこのゲーデル数の問題は、
¬Pとか、P→Q程度のシンプルな式ですら、こんな大きな自然数が出てきてしまうのです。
ただ、実際にそれを計算することを想定していないので問題ありません。純粋な思考実験です。
そして、このゲーデル数の自然数を素因数分解するとかならず一意的に決まり、そしてもともとの論理式になるということです。
この自然数をそれぞれの論理式のゲーデル数と呼び、関数gをゲーデル数化（Godel numbering） と言う。異なる記号列には異なる自然数が対応することを理解するには、どのような自然数もただ一通りに素因数分解されるということに注目すればよい。例えば 108000という自然数は、2^5・3^3・5^3という仕方でしか素因数分解できない。したがって、この自然数は、「））（」という記号列のゲーデル数であって、他の記号列のゲーデル数にはなれない。
このようにして、それぞれの有限記号列にはそれぞれ異なるゲーデル数が対応していることがわかった。そこで，これらの記号列のうち，論理式になっているものだけをとりだし、それらの論理式を対応するゲーデル数の小さなものから順番に並べ，0,1,2.3，という具合に番号をつけ直すことができる。こうして、すべての論理式に自然数の番号をつけて一列に並べること（枚挙
enumeration と言う）ができる。（p.365「論理学をつくる」）
見事な手際です。
これがゲーデルは素数を、チューリングはチューリングマシンを私は（チャイティンは）Lispを使ったという話に繋がるわけです。
その点について、チャイティンはこう言います。
（引用開始）
手短に言うと、ゲーデルは不完全性を、チューリングは計算不可能性を、私はランダム性を発見しました。
（略）
私のアプローチは、ゲーデルやチューリングの方式同様に複雑ですが、その複雑さが異なります。ゲーデルの場合は、それは公理系の内部構造、原始帰納定義スキーマ、および、彼のゲーデル数の番号付けが複雑なのでした。チューリングの場合は、彼の1936年の論文で説明された、万能チューリングマシンのインタープリタープログラムが複雑でした。私の場合には、（チューリングの複雑な万能マシンに相当する）LISPインタープリターが複雑です。これはみなさんには見えません。
（引用終了）
「ゲーデルの場合は、それは公理系の内部構造、原始帰納定義スキーマ、および、彼のゲーデル数の番号付けが複雑」。
いまやったのは3つ目の「ゲーデル数の番号付け」ですね！
ちなみにこの記事には最終盤に、以下のように書いてあります。
論理学でも紹介した書籍（「論理学をつくる」）ですが、上記で引用したので、再度紹介します。
ゲーデル数化などについても、３６５ページに非常に簡潔に紹介されています。
素因数分解の一意性とすべての論理式が枚挙可能であることがどうしてもつながらない人はぜひ読んでみると良いかと思います。
いまくどくど説明していることを、2013年にはあっさり4行で終わらせています。面白い。
これで、ゲーデル数化に成功し、すべての論理式の集合が可算集合であることを示せたので、あとはカントールの対角線論法に放り込めば不完全性定理の出来上がりです！次回は対角線論法に入ります！（先の「丸書いて線」とこの不完全性定理周辺が次回のOMSのテーマです！）
で、対角線論法については、もう「無限論の教室」が一番だと僕は思います。
