Can we prove set theory is consistent?

Question

Disclaimer

Of course not, I'm aware of Gödel's second incompleteness theorem. Still there is something which does not persuade me, maybe it's just that I've taken my logic class too long ago. On the other hand, it may turn out I'm just confused. :-)

Background

I will be talking about models of set theory; these are sets on their own, so a confusion can arise, since the symbol $\in$, viewed as "set belonging" in the usual sense, may have a different meaning from the symbol $\in$ of the theory. So, to avoid confusion, I will speak about levels.

On the first level is the set theory mathematicians use all day. This has axioms, but is not a theory in the usual sense of logic. Indeed, to speak about logic we already need sets (to define alphabets and so on). In this naif set theory we develop logic, in particular the notions of theory and model. We call this theory Set1.

On the second level is the formalized set theory; this is a theory in the sense of logic. We just copy the axioms of the naif set theory and take the (formal) theory which has these strings of symbols as axioms. We call this theory Set2.

Now Gödel's result tells us that if Set2 is consistent, it cannot prove its own consistence. Well, here we need to be a bit more precise. The claim as stated is obvious, since Set2 cannot prove anything about the sets in the first level. It does not even know that they exist.

So we repeat the process that carried from Set1 to Set2: we define in Set2 the usual notions of logic (alphabets, theories, models...) and use these to define another theory Set3.

A correct statement of Gödel's result is, I think, that

if Set2 is consistent, then it cannot prove the consistence of Set3.

The problem

Ok, so we have a clear statement which seems to be completely provable in Set1, and indeed it is. This doesn't tell us, however that

if Set1 is consistent, then it cannot prove the consistence of Set2.

So I'm left with the doubt that what one can do "from the outside" may be a bit more than what one can do in the formalized theory. Compare this with Gödel's first incompleteness theorem, where one has a statement which is true for natural numbers (and we can prove it from the outside) but which is not provable in PA.

So the question is:

is there any reason to believe that Set1 cannot prove the consistence of Set2? Or I'm just confused and what I said does not make sense?

Of course one could just argue that Set1, not being formalized, is not amenable to mathematical investigation; the best model we have is Set2, so we should trust that we can always "shift our theorems one level". But this argument does not convince me: indeed Gödel's first incompleteness theorem shows that we have situations where the theorem in the formalized theory are strictly less then what we can see from the outside.

Final comment

In a certain sense, it is far from intuitive that set theory should have a model. Because models are required to be sets, and sets are so small...

Of course I know about universes, and how one can use them to "embed" the theory of classes inside set theory, so sets may be bigger than I think. But then again, existence of universes is not provable from the usual axioms of set theory.

Answer 1

Would you accept it if Set1 just proved the existence of a model for Set2 (in the same way that Set1 proves the consistency of formalized Peano arithmetic by providing a model of it)?

If so, and if you accept in Set1 that there is an inaccessible cardinal κ, then the set V_κ is a model of ZFC, provably in Set1. Most set theorists today seem to believe that there are inaccessible cardinals and much bigger "large cardinals" in the universe of sets. So they count this as a proof of the consistency of ZFC, just as they count the existence of the standard natural numbers as a proof of Peano arithmetic.

You do not even need to assume Set1 has an inaccessible cardinal. For example, you could assume Set1 contains all of Morse-Kelley set theory and Set2 consists of ZFC, and then Set1 would prove the consistency of Set2.

What you cannot do is prove the consistency of Set2 within Set1 using only techniques that can be formalized within Set2. This is no different than with Peano arithmetic: we can formally prove that Peano arithmetic is consistent, but not using methods that can themselves be formalized in Peano arithmetic. The fact that you are interested in set theory only makes the problem seem more complicated; the underlying phenomenon is not much different.

Answer 2

Your question certainly makes sense and it is a point that I feel is too often glossed over in textbooks.

Let me rephrase your question. Goedel's second theorem says that, assuming that a certain formal system (ZFC, say) has a certain property that we call "consistency," then there is no formal proof in ZFC of a certain string, commonly denoted by "Con(ZFC)." Fine. But why on earth should this theorem say anything about whether the consistency of ZFC can be proved mathematically? The theorem is just a theorem about abstract strings of symbols, not about what human beings can and cannot do. The string denoted "Con(ZFC)" is commonly taken to "say" that "ZFC is consistent," but what is the justification for doing so? A string is just a string, and doesn't "say" anything. If we choose to think of the string as "meaning" something then that's our business, but surely that kind of human social activity is not something we can prove mathematical theorems about?

The answer is that, underlying the usual discussions of Goedel's second theorem, there is the following Key Assumption: If someone were to come up with a mathematical proof of the consistency of ZFC, then by mimicking that proof, we could produce a formal proof of Con(ZFC) from the axioms of ZFC. The Key Assumption is crucial. Without it, we cannot make the leap from Goedel's second theorem to a meta-mathematical statement about the (im)possibility of proving the consistency of mathematics. And note that the Key Assumption is not a purely mathematical one; it cannot be, because it is a statement linking something that is not purely mathematical (namely, mathematical proof, which is a product of human activity) and something that is purely mathematical (namely, ZFC and theorems of ZFC). Therefore the Key Assumption is not susceptible to mathematical proof, and the reasons we have for accepting it must be in part philosophical.

So what reasons do we have for accepting the Key Assumption? The chief reason is that long experience has taught us that all mathematical proofs that mathematicians come up with can indeed be mimicked by formal proofs in ZFC. This may seem obvious to us today, but it is not at all a trivial statement. Prior to the set-theoretic revolution, it was by no means obvious that all the diverse areas of mathematics could be formulated in a single common language (i.e., set theory) and deduced from a short list of axioms. It is only through the hard work of those working in the foundations of mathematics that we now take for granted that for any precise mathematical statement we want to make, there exists a formal sentence $S$ in the first-order language of set theory with the property that any mathematically acceptable proof of the original mathematical statement can be mimicked to produce a formal proof of $S$ from the axioms of ZFC. And if you had any lingering doubts about whether this formal mimicry existed only in theory and not in practice, then in recent years, the advent of formal theorem-proving software such as Mizar, HOL Light, Coq, Isabelle, etc., should have swept away such doubts by demonstrating concretely that large areas of mathematics can be mimicked formally in practice, and not just in theory.

Finally, let me mention that although I believe it is very reasonable to accept the Key Assumption, it is possible to reject it. Perhaps most notably, the philosopher Michael Detlefsen has challenged the standard claim that the string Con(ZFC) properly mimics the statement "ZFC is consistent" in the sense of the Key Assumption, and has suggested that Hilbert's program to prove the consistency of mathematics is not yet dead. I believe that Detlefsen is simply mistaken and that there is nothing unsatisfactory about the standard string Con(ZFC), but he is at least correct that there is something to be checked here, and it is not a purely mathematical point but a partially philosophical one.

Answer 3

Is there any reason to believe that Set1 cannot prove the consistence of Set2? Or I'm just confused and what I said does not make sense?

What you're asking does make sense, but there are good informal-but-rigorous reasons to believe that Set1 (informal mathematics) cannot prove the consistency of Set2 (a formalization of "everything we want" from informal mathematics).

The reason is that we can recast Godel's incompleteness result in terms of the Halting Problem, so that being able to give such an informal consistency proof amounts to giving some physical method for deciding whether arbitrary Turing machine programs halt. The existence of such a method would imply that the Church-Turing hypothesis is false, which is a claim about the physical world that presently seems very unlikely to be true.

Answer 4

Your question raises two interesting issues: one of formalisation, one of externalisation/reflection. The former contains a real problem, but more philosophical than mathematical; the latter is I think where the mathematical content of your question lies, and it has a positive answer.

---

You hit the first one on the head when you point out: "of course one could just argue that Set1, not being formalized, is not amenable to mathematical investigation," and I don't think your next point quite answers that question: you discuss the externalisation issues of Gödel's theorem, but that's separate from the formalisation question. You ask for a reason to believe Set1 doesn't prove something — how could one hope to give that without discussing Set1 as a precise object in some meta-theory?

Fortunately, though, we don't need to posit a Set0 for this and end up with the same problem one turtle lower down. To formalise the fundamentals of proof theory, we just need to be able to talk about manipulating strings of symbols, so a theory of the natural numbers (eg PA or even HA) is more than enough. On the other hand, we do have to presume some given meta-theory (as most traditional logicians would call it) or logical framework (as many computer scientists would) to get off the ground, and for that we really do have the problem that we can't talk about it as an object itself without passing to a meta-meta-theory. This is a real problem, but more a philosophical than a mathematical one: we just have to either accept a potential infinite regress, or make a leap of faith that facts proven within our meta-theory, about some internal version of it, will apply to the meta-theory itself (whether this is a platonic object, a physical computer system, or whatever else).

---

The second issue is one of reflection, and has a more satisfying resolution. (I'll keep the meta-theory informal, but HA would be more than enough to formalise this, I think.) Say we have some axioms for Set1, strong enough that it contains an "internal copy" of the natural numbers and hence can talk about basic proof theory; then define Set2 as the "internal version" of the same theory in Set1, and so on. Now we can prove:

Lemma. (An instance of a reflection principle for provability.) If Set1 proves "Set2 is consistent", then it also proves "Set2 proves 'Set3 is consistent' ".

(This is a good exercise in internalisation; it essentially comes from the fact that "being a proof" is a very straightforward property, and hence robust under internalisation.)

Now, if Set1 is able to prove Gödel's theorem for Set2 (in the form you state it, i.e. "if Set2 proves consistency of Set3, then Set2 is inconsistent"), we can deduce Gödel's theorem for Set1 as follows:

Suppose Set1 proves Con(Set2). By the above proposition, Set1 also proves "Set2 proves Con(Set3)". Now, by Gödel's theorem for Set2, we can deduce (still in Set1) the theorem "Set2 is inconsistent". But now we have proofs in Set1 of both Con(Set2) and its negation; so Set1 is inconsistent. QED

So your question has a positive answer: if we're allowed to reason mathematically about Set1 at all, then yes, we have reason to believe it doesn't prove the consistency of Set2.

Answer 5

I think you are describing a process that is a fairly accurate description of how set theorists typically think about issues of consistency, where Set1 is the informal account of the cumulative hierarchy, as it is illuminated by our other formal investigations, Set2 is ZFC, and Set3 is not one, but a family of stronger set theories obtained by something like your process of reflection back into Set1, which I shall call Set3*.

The major divergence is that logicians won't talk about Set1 proving anything, because it doesn't have any kind of proof theory, which is as others have indicated your answer. Instead Set1 will "justify" the axioms of Set2, and will "ground" or "suggest" proposed axioms for Set3*.

So what I take from your discussion about applying incompleteness is (i) further indication that Set1 has no proof theory, since it is an abundant, fallible source of new proof-theoretic strength, (ii) that the Gödelian hierarchy of proof-theoretic strength must be a guide when we investigate the theories in Set3*, and (iii) not really any sign of a model, besides those we get from axiomatisations courtesy of the completeness theorem.

I think it is illuminating to contrast the status of the consistency for set theory with that for arithmetic, where Gentzen gave a proof-theoretic proof of consistency directly grounded in combinatorial intuition. There, Arith1, our arithmetic intuition, plays a more direct role in shoring up Arith2, Peano Arithmetic, and where analysis of the Gödelian hierarchy shows that consistency of the theory is equivalent in strength to the truth of the elementary combinatorial principle. Unfortunately, we don't know how to construct such combinatorial principles strong enough to prove ZFC consistent.

Answer 6

To Formalize theory means You have certain and countable number of axioms and rules of inference which can be recognized. When You formalize theory Set2 You have to chose only finite part of such possible and used rules. So It is possible that Your Set1 theory prove that certain subset of possible rules is correct and consistent. But is has hidden cost. Suppose You have such proof based on Set1 informal theory. Suppose it is finite and has length N signs. Then only finite number of rules of inference and axioms was used! So we may formalize it by adding it into Set2 and then we obtain formal theory which may prove its own consistency. This is in contradiction with Gödel Theorems.

Then You may construct such proof, but it have to have infinite amount rules of inference and axioms which are different each other, and this has to be uncountable infinity ( because Gödel theorems are valid for countable ones)

So You probably cannot prove that this informal proof, based on open system Set1 is correct, because it has to use certain rules of inference which are not clear, maybe not consistent in every situation and probably not applicable in certain situation, and which is the most important, impossible to count, so it cannot be grouped into countable amount of axiom schemas.