第１不完全性定理の回避寺戸良三ラッセルは自身のパラドックスを回避するために、PM で型理論を公理化しました。しかし、ゲーデルの不完全性定理は自己言及のパラドックスになっていて、ゲーデルの論文でも、”嘘つきのパラドックス”とも密接な関係がある。と書いてある通り、それを使って証明したといえばそれまでだが、また、訳注に一般に、任意の認識論的二律背反を、決定不能性の証明に利用することができる。と書いてあるように、自己言及のパラドックスを証明の利用可能にしているとも取られるが、ゲーデルの不完全性定理は PM の体系から不完全性定理を証明したのですから、ラッセルの型理論はその後、紆余曲折あったが、自己言及のパラドックスを回避してしているので、ゲーデルの不完全性定理は証明になっていないことになります。以下、ゲーデルの論文で厳密に証明しよう。ここで、ゲーデルの証明にならない証明に使う型理論の説明を先に述べる。命題 n 階として (Pn ) とする。（∃P)(Pn を主張し、かつ Pn は偽である）この命題は n+1 階である（Pn+1 ) 主張しているのは n 階であるから、Pn の可能な値とならない。これで、パラドックスは排除された。これより、上記の型理論をゲーデルの論文に適用してみる。 n∈K≡Bew[R(n);n] (1) 命題 [R(q);q] を (1) の論理式を PM の定義可能とするため、論文中では丁寧に説明しているが、結局は命題 [R(q);q] を (1) より、決定不能であることを示そうとしているが、 Bew により、(1) の右辺は類の類となり、型理論により一つ上の階になり (1) は成り立たない。よって、ゲーデルの第１不完全性定理は証明にならない。文献ゲーデル不完全性定理、林晋・八杉満利子訳・解説、岩波文庫パラドックスとラッセルのタイプ理論、土屋盛茂、香川大学学術情報リポジトリ 1