Re:Gödel, Escher, Bach: an in-depth explainer
by bmacho on Wednesday September 14, 2022 @04:54AM
(#32834719)
Why not?
E.g.: if ZFC is consistent, then ZFC+~Con(ZFC) is consistent as well, where ~Con(ZFC) is the statement that there is a contradiction in ZFC.
Now, ZFC+~Con(ZFC), which is a perfectly good axiom system, consistent and can talk about anything, can prove that the Turing machine that searches for a contradiction in ZFC halts (just apply the axiom ~Con(ZFC)), but it doesn't make it true.
E.g.: if ZFC is consistent, then ZFC+~Con(ZFC) is consistent as well, where ~Con(ZFC) is the statement that there is a contradiction in ZFC.
Now, ZFC+~Con(ZFC), which is a perfectly good axiom system, consistent and can talk about anything, can prove that the Turing machine that searches for a contradiction in ZFC halts (just apply the axiom ~Con(ZFC)), but it doesn't make it true.