Why is establishing the absolute consistency of ZFC impossible? What are the fundamental limitations that prohibit us with coming up with a proof?
EDIT: This post seems to make the most sense. In short: if we were to come up with a mathematical proof of the consistency of ZFC, we would be able to mimic that proof inside ZFC. Ergo, if ZFC is consistent, there can be no proof that it is.
This kind of question often includes several common points of confusion.
There is a mathematical, formally defined relation of provability between a formal system and a sentence, which defines what it means for the sentence to be "provable" from the formal system. This relation depends on both the statement and the formal system. On the other hand, there is no rigorous notion of "provable" without reference to a formal system.
So it does not really make any sense to talk about a statement being "unprovable" without reference to what system is doing the proving.
In particular, every statement is provable from a formal system that already includes that statement as an axiom. That is somewhat trivial - but even if the statement is not an axiom, it is still the case that the only way for a statement to be provable in a particular system is for the statement to already be a consequence of the axioms of the system. This is true for Con(ZFC) and for every other mathematical statement. Some statements are provable from no axioms at all - these are called logically valid. The incompleteness theorems show in a very strong way that Con(ZFC) is not logically valid.
There is a particular polynomial $P$, with integer coefficients, integer exponents, and many variables, so that the statement Con(ZFC) can be expressed as "there are no positive integer inputs which cause the value of $P$ to equal 0". This statement is not particularly different in form, for example, than the special case of Fermat's last theorem: "there are not any positive integer inputs $x,y,z$ such that $x^{7}+y^{7}-z^{7} = 0$."
Nobody seriously claims that the proof of that special case of Fermat's last theorem is merely a conditional claim that can never be "absolutely proved" without assuming the consistency of some theory. But Con(ZFC) is not significantly different in form - just longer - than that special case of Fermat's last theorem. Both of these are just statements that some multivariable integer polynomial is never equal to zero on positive integer inputs.
The real situation is that almost nothing can be proved "absolutely". Unless a statement is logically valid, additional axioms will be required to prove it. There is nothing special about Con(ZFC) in that respect. Any proof of a non-trivial theorem will always rely on extra "assumptions', and in a trivial sense those assumptions always have to be at least as strong as the theorem we are trying to prove.
There are many, many axioms systems for set theory. ZFC is of interest because its axioms are very natural to motivate and because it is strong enough for formalize the vast majority of mathematical theorems. But that does not mean that ZFC is somehow a stopping point. There are natural systems of set theory stronger than ZFC.
On particular example is Morse--Kelley set theory, MK, which was exposited in the appendix of Kelley's book General Topology. This is a perfectly reasonable system for set theory, which happens to prove Con(ZFC). We should pay attention to the formal meaning of this: there is a finite derivation that has no assumptions besides the axioms of MK, and which ends with Con(ZFC). And note that MK was designed by a mathematician and published in a mathematics textbook for mathematical purposes.
The argument given in this MathOverflow answer includes a particular premise: that all "mathematical" techniques are already included in ZFC. That is the "Key Assumption" in that argument, which was alluded to in the question above.
There is some merit in that heuristic argument: many of the standard techniques of mathematics can be formalized in ZFC. The situation is not as clear as we might suppose, though, because of examples like MK set theory, which must be defined as "nonmathematical" in order for the Key Assumption to hold. At the worst, we could find ourselves making a circular argument, where we define "mathematical" to be "formalizable in ZFC" and then argue that ZFC is able to formalize all mathematical arguments.
A deeper question, which cannot be answered because it is ahistorical, is whether MK would be considered a more "natural" system if it had been exposited before ZFC. Just like ZFC, MK is based on a natural intuition about the nature of sets and classes, which leads to the next point.
What if we don't look at formal theories, and we just look for a "mathematical" but informal proof of the consistency of ZFC? Actually, we have one: there is a well known argument that our intuitive picture of the cumulative hierarchy shows that ZFC is satisfied by the cumulative hierarchy, and thus ZFC is unable to prove a contradiction. Of course, this argument relies on a pre-existing, informal understanding of the cumulative hierarchy. So not all mathematicians will accept it - but it is of interest exactly because it is very compelling as an informal argument.
If we want to separate "mathematical proof" from "formal proof", then it is not at all clear why this kind of proof should be out of the question. Unlike formal proofs, mathematicians may differ on whether they accept this informal proof of Con(ZFC). But it is certainly some kind of informal "mathematical proof" of Con(ZFC), if we are willing to consider informal proofs as mathematical.
We should really ask why someone would be interested in an "absolute" consistency proof of ZFC. Presumably, it is because they doubt that ZFC is consistent, and they want to shore up their belief (Hilbert's program can be caricatured in this way).
In that case, as soon as we see from the incompleteness theorems that the consistency of ZFC is not a logical validity, we are naturally led to an alternate question: "Which theories are strong enough to prove the consistency of ZFC?" There has been a lot of work on that question, in mathematical logic and foundations.
The incompleteness theorems give part of the answer: no theory that can be interpreted in ZFC can prove Con(ZFC). Examples like MK give another part: there are natural theories strong enough to prove Con(ZFC). In the end, we can choose any formal system we like for each mathematical theorem we want to prove. Some of those theorems are provable in systems that are unable prove Con(ZFC), and some of those theorems require systems that do prove Con(ZFC). Separating those two groups of theorems leads to interesting research in set theory and logic.
To add to Carl Mummert's answer...
Yes you read that right. Perhaps you might say, how about the formal system consisting of just first-order logic and not a single axiom, namely the pure identity theory, or maybe even without equality? Sorry, but that doesn't work. How do you state the claim that this system is absolutely consistent? You would need to work in a meta-system that is powerful enough to reason about sentences that are provable over the formal system. To do so, your meta-system already needs string manipulation capability, which turns out to be more or less equivalent to first-order PA. Hence before you can even assert that any formal system is consistent, you need to believe the consistency of the meta-system, which is likely going to be essentially PA, which then means that you do not ever have absolute consistency.
Of course, if you assume that PA is consistent, then you have some other options, but even then it's not so simple. For example you may try defining "absolute consistent" as "provably consistent within PA as the meta-system". This flops on its face because then you cannot even claim that PA itself is absolutely consistent, otherwise it contradicts Godel's incompleteness theorem. So ok you try again, this time defining "T is absolutely consistent" to mean "PA proves that Con(PA) implies Con(T)". Alright this is better; at least we can now show that PA is absolutely consistent, though it is trivial!
However, note that even with the assumption of consistency of some formal system such as PA, as above, you are still working in some meta-system, and by doing so you are already accepting the consistency of that meta-system without being able to affirm it non-circularly. Therefore any attempt to define any truly absolute notion of consistency is doomed from the start.
There's a level on which the answer is simply "because it turns out the be probably impossible" on a certain level. I'm not sure how much of any of this can be thought of as intuitive. Godel's Second Incompleteness Theorem states explicitly that if ZFC can prove its own consistency, then it is in fact inconsistent. The proof is very technical and relies heavily on the proof of the first incompleteness theorem.
The basic idea goes like this: Assume $T$ is a consistent set of axioms that meets a certain criterion (which ZFC does). Assume $T$ is able to prove its own consistency, and let $P$ be the unprovable statement in $T$ that says "there exists a proof of $P'$ if and only if $P'$ is false" for some statement $P'$. The construction of such a statement is doable with minor modifications to the standard proof of the first incompleteness theorem (specifically introducing a way to encode "P is provable" in the language of $T$). $T$ can prove the statement "$P$ is not provable" since $T$ can prove its own consistency, and $T$ can prove that "$P$ is not provable" is equivalent to $P$ itself! Therefore $T$ can in fact prove $P$, contradiction.
If there were a more powerful set of axioms that mathematicians agreed upon, then those axioms might be able to prove that ZFC is consistent, but there are two problems. First, Godel's Second Theorem applies to every system strong enough to prove the consistency of ZFC, so there is no axiomatic system able to prove both its own consistency and that of ZFC. Second, there is no such agreed upon more powerful set of axioms anyways (though one could argue that "ZFC plus the consistency of ZFC" is something most mathematicians assume). If we agreed on some such axiomatic system we could prove that ZFC was consistent, but only within the framework of a larger system whose consistency we cannot prove, which calls into doubt our proof of the consistency of ZFC.
