Can we prove set theory is consistent? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-22T19:56:49Z http://mathoverflow.net/feeds/question/22635 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent Can we prove set theory is consistent? Andrea Ferretti 2010-04-26T18:54:01Z 2012-10-05T17:13:13Z <p><strong>Disclaimer</strong></p> <p>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. :-)</p> <p><strong>Background</strong></p> <p>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.</p> <p>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 <em>naif</em> set theory we develop logic, in particular the notions of theory and model. We call this theory <strong>Set1</strong>.</p> <p>On the second level is the <em>formalized</em> set theory; this is a theory in the sense of logic. We just copy the axioms of the <em>naif</em> set theory and take the (formal) theory which has these strings of symbols as axioms. We call this theory <strong>Set2</strong>.</p> <p>Now Gödel's result tells us that if <strong>Set2</strong> 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 <strong>Set2</strong> cannot prove anything about the sets in the first level. It does not even know that they exist.</p> <p>So we repeat the process that carried from <strong>Set1</strong> to <strong>Set2</strong>: we define in <strong>Set2</strong> the usual notions of logic (alphabets, theories, models...) and use these to define another theory <strong>Set3</strong>.</p> <p>A correct statement of Gödel's result is, <strong>I think</strong>, that</p> <blockquote> <p>if <strong>Set2</strong> is consistent, then it cannot prove the consistence of <strong>Set3</strong>.</p> </blockquote> <p><strong>The problem</strong></p> <p>Ok, so we have a clear statement which seems to be completely provable in <strong>Set1</strong>, and indeed it is. This doesn't tell us, however that</p> <blockquote> <p>if <strong>Set1</strong> is consistent, then it cannot prove the consistence of <strong>Set2</strong>.</p> </blockquote> <p>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 <strong>PA</strong>.</p> <p>So the question is:</p> <blockquote> <p>is there any reason to believe that <strong>Set1</strong> cannot prove the consistence of <strong>Set2</strong>? Or I'm just confused and what I said does not make sense?</p> </blockquote> <p>Of course one could just argue that <strong>Set1</strong>, not being formalized, is not amenable to mathematical investigation; the best model we have is <strong>Set2</strong>, 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.</p> <p><strong>Final comment</strong></p> <p>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...</p> <p>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.</p> http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent/22650#22650 Answer by Neel Krishnaswami for Can we prove set theory is consistent? Neel Krishnaswami 2010-04-26T21:40:46Z 2010-04-26T21:40:46Z <blockquote> <p>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?</p> </blockquote> <p>What you're asking <em>does</em> 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). </p> <p>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.</p> http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent/22656#22656 Answer by Carl Mummert for Can we prove set theory is consistent? Carl Mummert 2010-04-27T00:11:57Z 2010-04-27T00:11:57Z <p>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)?</p> <p>If so, and if you accept in Set1 that there is an inaccessible cardinal &kappa;, then the set V<sub>&kappa;</sub> 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. </p> <p>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. </p> <p>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.</p> http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent/22711#22711 Answer by Charles Stewart for Can we prove set theory is consistent? Charles Stewart 2010-04-27T11:32:17Z 2010-04-27T11:32:17Z <p>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*.</p> <p>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*.</p> <p>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.</p> <p>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. </p> http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent/22766#22766 Answer by kakaz for Can we prove set theory is consistent? kakaz 2010-04-27T19:33:07Z 2010-04-28T11:06:33Z <p>To Formalize theory means You have certain and countable number of <strong>axioms and rules of inference</strong> 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. </p> <p>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)</p> <p>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. </p> http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent/23012#23012 Answer by Peter LeFanu Lumsdaine for Can we prove set theory is consistent? Peter LeFanu Lumsdaine 2010-04-29T17:27:49Z 2010-04-29T17:36:36Z <p>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.</p> <hr> <p>You hit the first one on the head when you point out: "of course one could just argue that <strong>Set1</strong>, 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&ouml;del's theorem, but that's separate from the formalisation question. You ask for a reason to believe <strong>Set1</strong> doesn't prove something &mdash; how could one hope to give that without discussing <strong>Set1</strong> as a precise object in some meta-theory?</p> <p>Fortunately, though, we don't need to posit a <strong>Set0</strong> 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 <strong>PA</strong> or even <strong>HA</strong>) is more than enough. On the other hand, we do have to presume <em>some</em> 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).</p> <hr> <p>The second issue is one of reflection, and has a more satisfying resolution. (I'll keep the meta-theory informal, but <strong>HA</strong> would be more than enough to formalise this, I think.) Say we have some axioms for <strong>Set1</strong>, strong enough that it contains an "internal copy" of the natural numbers and hence can talk about basic proof theory; then define <strong>Set2</strong> as the "internal version" of the same theory in <strong>Set1</strong>, and so on. Now we can prove:</p> <p><strong>Lemma.</strong> (An instance of a reflection principle for provability.) If <strong>Set1</strong> proves "<strong>Set2</strong> is consistent", then it also proves "<strong>Set2</strong> proves '<strong>Set3</strong> is consistent' ".</p> <p>(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.)</p> <p>Now, if <strong>Set1</strong> is able to prove G&ouml;del's theorem for <strong>Set2</strong> (in the form you state it, i.e. "if <strong>Set2</strong> proves consistency of <strong>Set3</strong>, then <strong>Set2</strong> is inconsistent"), we can deduce G&ouml;del's theorem for <strong>Set1</strong> as follows:</p> <p>Suppose <strong>Set1</strong> proves <strong>Con(Set2)</strong>. By the above proposition, <strong>Set1</strong> also proves "<strong>Set2</strong> proves <strong>Con(Set3)</strong>". Now, by G&ouml;del's theorem for <strong>Set2</strong>, we can deduce (still in <strong>Set1</strong>) the theorem "<strong>Set2</strong> is inconsistent". But now we have proofs in <strong>Set1</strong> of both <strong>Con(Set2)</strong> and its negation; so <strong>Set1</strong> is inconsistent. <strong>QED</strong></p> <p>So your question has a positive answer: if we're allowed to reason mathematically about <strong>Set1</strong> at all, then yes, we have reason to believe it doesn't prove the consistency of <strong>Set2</strong>.</p> http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent/24919#24919 Answer by Timothy Chow for Can we prove set theory is consistent? Timothy Chow 2010-05-16T19:34:14Z 2010-05-16T19:34:14Z <p>Your question certainly makes sense and it is a point that I feel is too often glossed over in textbooks.</p> <p>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?</p> <p>The answer is that, underlying the usual discussions of Goedel's second theorem, there is the following Key Assumption: <i>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.</i> 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 <i>is</i> 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.</p> <p>So what reasons <i>do</i> 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.</p> <p>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.</p> http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent/108935#108935 Answer by Lukasz for Can we prove set theory is consistent? Lukasz 2012-10-05T17:13:13Z 2012-10-05T17:13:13Z <p>0 down vote</p> <p>I would like to inform that I (commonly with Dr Teodor Stepien) delivered a talk at the Conference "2009 European Summer Meeting of Association for Symbolic Logic, Logic Colloquium'09" (July 31 - August 5, 2009, Sofia, Bulgaria). In this talk, entitled "On consistency of Peano's Arithmetic System", we presented a sketch of the proof of the consistency of Peano's Arithmetic System (of course, the full proof was constructed by us before the mentioned Conference "Logic Colloquium 2009"). This proof is ABSOLUTELY ELEMENTARY, i.e. there are used ONLY the axioms of first-order logic and the axioms of Peano's Arithmetic System. Hence, from the construction of this proof, it follows that Gödel's Second Incompleteness Theorem is INVALID. The asbtract of this talk was published in "The Bulletin of Symbolic Logic": T. J. Stepien and L. T. Stepien, Bull. Symb. Logic 16, 132 (2010). This abstract is accessible under the following link <a href="http://www.math.ucla.edu/~asl/bsl/1601-toc.htm" rel="nofollow">http://www.math.ucla.edu/~asl/bsl/1601-toc.htm</a> and after clicking on: "2009 European Summer Meeting of the Association for Symbolic Logic, Logic Colloquium '09, Sofia, Bulgaria, July 31â€”August 5, 2009" (page 132).</p>