今回、ある掲示板で話題になっていた、
ZFC から証明不可能な実数を構成したいと思います。
もちろん、ZFC の無矛盾性は仮定します。
N を可算無限基数, M を最小の非可算基数とします。
ZFC の論理式 A(x) を、以下のように定めます：
A(x) ⇔ (2^N = M ∧ x = 1)∨(2^N ≠ M ∧ x = √2)
そうすれば、等号述語論理の一般論より、
ZFC からは、論理式
(∃_1 x) A(x)
が証明可能です。
ここに、∃_1 は、「ただ一つ存在する」
という意味です。
そこで、A(x) を満たす唯一つの x を a と置きます。
ZFC から a が実数であることが証明可能なことは、明らかです。
（実際は、ZFC から、a = 1 ∨ a = √2 が証明可能。）
しかし、ZFC が無矛盾ならば、
ZFC からは証明不可能です。
実際、ZFC から a が有理数であることが証明可能とします。
そうすれば、A(a) と
A(a) ⇔ (2^N = M ∧ a = 1)∨(2^N ≠ M ∧ a = √2)
が ZFC から証明可能であることより、
2^N = M ∧ a = 1
が ZFC から証明可能です。
しかし、2^N = M は ZFC からは証明不可能ですから、
不合理です。
逆に、ZFC から a が無理数であることが証明可能とします。
このときも、
A(a) と
A(a) ⇔ (2^N = M ∧ a = 1)∨(2^N ≠ M ∧ a = √2)
が ZFC から証明可能であることより、
2^N ≠ M ∧ a = √2
が ZFC から証明可能です。
ここで、やはり、2^N ≠ M は ZFC から証明不可能ですから、
不合理です。
したがって、上記 a は、 ZFC の下で、
文責: Dr. Kazuyoshi Katogi
