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

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.