Consistency of ZFC and the key assumption

Question

I recently read this answer to a MathOverflow question that got me thinking. Very roughly, here's what the author of that answer says:

Gödel's second incompleteness theorem implies that if there is a proof of 'Con (ZFC)' in ZFC, then ZFC is inconsistent. Also, most people have the following assumption (key assumption, or KA for short): any mathematical proof can be turned into the corresponding proof in ZFC. Therefore, if we were to mathematically prove the consistency of ZFC, this proof could be turned into its ZFC counterpart, which, in turn, will show that ZFC is, in fact, inconsistent.

Later the author of the answer goes on and stresses that KA cannot be justified mathematically, but only philosophically. Essentially, we believe KA is true because an enormous amount of mathematical proofs has already been turned into proofs in ZFC using various software. In other words, because we have seen this "translation" process take place many times, it can be carried out for any mathematical proof (this is an inductive argument, in the philosophical sense). My question is: if we were prove the consistency of ZFC mathematically, what can in principle prevent this proof from being turned into a proof in ZFC?

P.S. I thought this question is more appropriate for Math.SE, but feel free to move it to Philosophy.SE.

Answer 1

I'm sure people will weigh in who understand this much better than I do, but one idea comes immediately to mind. One can prove that Peano arithmetic (PA) is consistent. By Gödel's theorem, this can only be proved in PA if PA is inconsistent. But the proof is not carried out in PA, but rather in ZFC, which is strictly stronger than PA.

So one could at least in principle invent a system S that was stronger than ZFC, and use that to prove that ZFC was consistent. The problem is then that there is no way to know that S itself is consistent; if S is inconsistent its proof of ZFC's consistency is worthless. And S is even more complicated and powerful than ZFC, so our belief in ZFC's consistency is no support for the consistency of S, or at least of no more support than it was for the consistency of ZFC in the first place. And of course S is of no use in proving that S itself is consistent, by Gödel's theorem.

(A trivial but specific example of such a system S that can prove the consistency of ZFC is simply ZFC plus the axiom that ZFC is consistent. Clearly S is consistent if and only if ZFC is, and the proof (in S) that ZFC is consistent is trivial.)

Answer 2

If we were prove the consistency of ZFC mathematically, what can in principle prevent this proof from being turned into a proof in ZFC?

Well, we can prove the consistency of ZFC mathematically, e.g. by assuming that there is an inaccessible cardinal. But to stick with this example, this can't be turned into a proof inside ZFC itself because ZFC can't prove the premiss that there is an inaccessible cardinal.

Is that very puzzling, post-Gödel? We know that no recursively axiomatized set theory will fix the truth-values of every sentence expressible in the language of set theory. By making stronger and stronger assumptions (assumptions, you might hope, that seem to justified in turn by the intuitive conception of the cumulative hierarchy of sets), we can prove more and more. But there is no limit point to the process of adding assumptions where we can prove or disprove everything (unless we become inconsistent, or it stops being decidable what is an axiom of the theory).