十分強い帰納的公理化可能な理論を前提として、第一と第二がある。
第一で証明も反証もできない命題の存在を主張し、第二でその一つが自身の無矛盾性、つまり具体例を挙げることができるものであることを示している。
巨大数論への影響[]
結論から言えば、計算可能と不可能を分ける動機となる。
任意の関数fと任意の定義域内の引数xを受け取り妥当なyを返してくれる計算機が存在すればこの区分は意味を成さないことになる。第一不完全性定理からこのような計算機は、（ある程度強い関数を扱えるものとして）存在しないことが導かれる。
再帰的に定義可能なメタ理論MTから一階の形式言語Lを定義し
WIP
第一不完全性定理からじゃなくても統語論側から直接チューリングマシンの決定可能性問題を否定的に解決して、計算不可能な関数の存在を認めてもいいし、逆にこの統語上の問題を証明の存在に関する解釈をして第一第二不完全性定理を導いてもいいだろう。
不完全性定理を回避する理論[]
ラヨ数系の定義に必要になってくると思われる。