1階述語論理の決定不能性
証明.1
最もシンプルに証明する．Robinson算術の本質的決定不能性は証明済みとする．
Robinson算術の公理を全て$ \landで繋ぐ（Robinson算術は有限個の公理しかもたないからこの論理式も有限長しかない）．これを演繹定理で右に送れば良い．すなわち
$ \mathsf{Q} \vdash \varphi \iff \bigwedge \mathsf{Q} \to \varphi
$ \sf Qは本質的に決定不能だから右側も決定不能になる．（右側が決定可能だとすると話がおかしくなる）
発見者
いろんな人が独立に発見している
Alan Turing
Stephen C. Kleene