Robinson算術の本質的決定不能性を用いたZF集合論の第1不完全性定理の証明
#ZF集合論の不完全性定理について
説明
Gödelの第1不完全性定理は一般に算術，すなわちPeano算術やRobinson算術などについての言明であり，素朴に集合論について適用できない．
方法
1. 理論の解釈可能性という概念を用いてZF集合論$ \sf ZFがRobinson算術$ \sf Qによって解釈可能，ということを示す
すなわち$ \sf ZF \rhd Q
ZF公理系のRobinson算術での解釈可能性
2. ZF集合論が再帰的公理化可能であるということを示す．
3. $ \sf Qは本質的に決定不能である．
Robinson算術の本質的決定不能性
4. 次の定理を用いる．
本質的に決定不能な理論へ解釈可能な再帰的公理可能理論は，無矛盾なら不完全
以上の議論より，$ \sf ZFが無矛盾なら不完全という結論が得られる．