This may or may not be the first part of a project to abridge Douglas Hofstadter's "Gödel, Escher, Bach: An Eternal Golden Braid", which somehow takes hundreds of pages to cover the same material.

There is of course a system which can prove ZFC to be consistent. Just take ZFC plus the axiom that ZFC is consistent (note: not the theory that this new system is consistent, just that ZFC is). Call that ZFC+1. (not a standard notation, just picked arbitrarily right now) And ZFC+1 can be shown to be consistent in ZFC+1 plus "ZFC+1 is consistent" and so on. I'm pretty sure the things I just said are all true? Though, what system am I working under, if I can prove that ZFC+\alpha (where alpha is an ordinal) can be proven to be consistent under ZFC+(\alpha+1) ?

(Fixed your <br/>s.)

Is it actually possible to express "ZFC is consistent" in the form of an axiom?

Well, yes, anything can be proven consistent if you start with "X is consistent" as one of your axioms.

I'm not actually sure about what the difference between an axiom and an axiom schema is, so I'm not certain that it can be expressed as a single axiom that ZFC , being the other axioms in use, is consistent, but I'm fairly sure that at least with axiom schemas you can? I'm pretty sure I saw that said somewhere? I thought wikipedia said it but I'm not finding it there right away, so I am not totally sure. But I'm pretty sure that for any axiom system, there is another axiom system that has all of those axioms, plus (an) axiom(s) that states that the other axioms don't lead to a contradiction. It might be /false/, but it could be proven. I'm like, about 85-90% sure of this? (not 99% sure though)

An axiom schema is not itself an axiom but rather a rule for generating axioms. It's a way to define a system that has an infinite number of axioms, which is necessary when you need to constrain the form of those axioms to avoid something undesirable (usually self-reference). Consider the relationship between an axiom schema and an axiom to be like the relationship between proper classes and sets. Proper classes exist so you can express things like "the collection of all sets that do not contain themselves" without introducing a paradox. Axiom schemata exist for similar reasons.

Ok, found a wikipedia page that says that you can add a statment that a formal system. see https://en.wikipedia.org/wiki/Ω-consistent_theory#Examples The page talks about adding the consistency or inconsistency of peano arithmetic to the axioms of peano arithmetic, but I assume the same would apply for ZFC .

Here's the big problem: Sure, assume ZFC is consistent. You haven't axiomatized its completeness, so by Godel you're basically just formalizing its incompleteness. No violation. Okay, fine, so that just means you need to make the axiom instead say "ZFC is both consistent and complete." At that point, you can prove that ZFC+1 is inconsistent (by direct application of Godel's incompleteness theorem), and by extension any model that asserts ZFC+1 is consistent must therefore also be inconsistent. (It doesn't prove anything one way or the other about ZFC itself.)

@Coda : Thank you for the explanation about axiom schema. But, why would you want to take as axiom that ZFC is complete? from godel's , it seems like it isn't complete (if we assume it is consistent that is), so why would we want to take it as an axiom that it is complete? I wasn't trying to establish any sort of violation of anything, just giving an example of a system that (assuming ZFC is consistent) is stronger than ZFC, by being able to prove ZFC consistent.

There are many wrong things being said here. (If it was so trivial to abridge GEB, it would have been done long ago. :-P) There are also many things people are unsure of. I'll try to address them one by one. (I have a PhD in mathematical logic, and very rarely get to see someone being "wrong on the Internet"^{TM} in my area of expertize. Please forgive me.:) First, cases 1B and 2A are not "uncontroversial" at all. As the following shows, it's very wrong to conflate the notions of truth and provability in any sufficiently complex (r.e.) theory. In fact, it is _precisely_ the desire to proclaim 1B and 2A uncontroversial, that has got us into all this mess. ;-P Second, not every logic employs principle of explosion. There are paraconsistent logics. Third, "mathematics _as a whole_ is incomplete" is dishonest, considering your second asterisk. There is no "mathematics as a whole" in a shape that can be meaningfully said to be complete or incomplete. Fourth, not everyone would agree that Goldbach hypothesis (Gh) is "either true or false". That requires a standard model of arithmetic, which is not something trivial. (How about a standard model of religion?:) Fifth, if we handwave the standard model into existence, it is _impossible_ that Gh is false but unprovable (in PA, even). Hint: if Gh is false, then there is a concrete number 2N such that (1 is not prime or 2N-1 is not prime) and (2 is not prime or 2N-2 is not prime) and ... and (N is not prime or N is not prime). For every concrete number 2N, it is a matter of simple (but possibly incredibly boring:) arithmetic to check this. Sixth, "there is an even worse fourth possibility" - this is one of those truths that people usually completely misunderstand (you disclaimed yourself with the asterisk, I know, but again, it's dishonest). Yes, ZFC might be shown inconsistent. PA might be shown inconsistent. But mathematics as a whole cannot be inconsistent, because it's contrary to its definition. People have tried to base the whole of mathematics on naive set theory, which is inconsistent. Has something terrible happened to mathematics? Hardly. We have just invented a better foundation. Seventh, I have always been amused by the general misunderstanding of the effect of Gödel2 on our understanding of mathematics. Imagine for a moment a world where Gödel2 is not true (or at least not yet proven:), and we have found a proof in ZFC that ZFC is consistent. Would you believe it? Seriously? :-) Remember that if it is consistent, it is at least _possible_ to be unable to prove its consistency, but if it inconsistent, then it can prove anything. Now, what does the Bayes say? :-] Eighth: "theories which are complete and can prove themselves consistent" are not hard to conceive. Any inconsistent theory in some ordinary logic with explosion will serve the purpose. :-) (Now the comments.) Ninth: "what system am I working under, if I can prove that ZFC+\alpha (where alpha is an ordinal) can be proven to be consistent under ZFC+(\alpha+1) ?" For a concrete alpha, you're working in the most elementary propositional logic. "ZFC+\alpha is consistent" is one of _axioms_ of your theory. To prove an axiom, you usually don't need much complicated machinery. :-D For a general ordinal, well, you have to have some way of talking about general ordinals. But it's not that hard - second-order will do. Tenth: "Is it actually possible to express "ZFC is consistent" in the form of an axiom?" For a question to be meaningful, obviously you meant "axiom in ZFC's language" - otherwise you've just expressed it. :-) And yes, it's possible - but nontrivial. The simplest way is probably to take some elementary introduction to logic of proofs, and encode it into ZFC, together with ZFC's axioms. For example, symbols are specific finite ordinals, tuples are finite sets of Kuratowski's sets, formulas are tuples of symbols with special properties, proofs are tuples of formulas with special properties, and not(there exists(proof whose last element is formula \emptyset\in\emptyset)). You don't even need schemas for this, if you're careful. :-) Eleventh, drocta's "I'm pretty sure" (85-90%:) is trivially true unless you require that language stays the same (as above), and then it might be false. Not every theory has a language powerful enough to naturally express claims about itself, unless you cheat by just picking some irrelevant formula and saying it expresses consistency. :-P Twelfth: Coda, I must say I don't get your analogy with proper classes. Here, take schema of replacement (in ZFC). What undesirable property are we avoiding by not stating it as a single axiom? For me, "ZFC is not finitely axiomatizable" is a fact (consequence of Montague's reflection), not something that can be delegated to some sense of aestetics. Thirteenth: yes, the Wikipedia link about \Omega-consistent theories applies to ZFC just fine. Fourteenth: "(It doesn't prove anything one way or the other about ZFC itself.)" Surely it does. Since it is inconsistent, it proves _everything_ you wish (and even everything you don't wish;) about ZFC. If there are any further questions, and you are not bored to death already, feel free to ask. :-)

In the final paragraph, there is mentioned the possibility of a more advanced theory of mathematics capable of proving the consistency of ZFC, and of a yet more advanced theory of mathematics capable of proving the consistency of this, and so on. Is there any reason why we couldn't, continuing in this fashion, arrive at a theory of mathematics to which the requirements of Gödel's incompleteness theorems do not apply and which is capable of proving its own consistency? I.e. could there be a collection of theories of mathematics, T_1, ..., T_n, such that the following holds: * T_1 is capable of proving the consistency of ZFC * T_2 is capable of proving the consistency of T_1 * T_3 is capable of proving the consistency of T_2 ... * T_n is capable of proving the consistency of T_{n-1} * T_n is capable of proving the consistency of T_n

That's a lot of feedback. I'll see what I can do to fix those problems while keeping the essay accessible.

@benneh: To my admittedly inexpert understanding, the possibility of that T_n which is capable of proving the consistency of all other systems of logic which actually are consistent (and only those), can neither be proven nor disproven at this time, but the smart money is on "it's turtles all the way down."

benneh: As you can probably see, the problem is in the last row. T_n being capable of proving the consistency of T_n (itself) would then be inconsistent, so nothing it proves can be trusted. Specially, that applies to consistency of T_{n-1}.

john: I'm not assuming that T_n is capable of proving the consistency of anything other than T_{n-1}. It probably also follows that it's capable of proving the consistency of all the other T_i's, and of ZFC itself. But we're only talking about finitely many theories here. I don't see why it follows that it's capable of proving the consistency of "all other systems of logic which actually are consistent (and only those)", which certainly does seem unlikely. Unless I'm misunderstanding your comment? Veky: I'm assuming that T_n doesn't satisfy the requirements of Gödel's incompleteness theorems, so there's nothing immediately problematic about it being able to prove its own consistency. That was the point of the question.

drocta: The point is that you DON'T want to axiomatize completeness, but just axiomatizing consistency doesn't actually gain you anything -- all you've done is defined a system that is more powerful on paper, but it actually ISN'T. It doesn't give you any new tools to work with, and if somehow a proof of ZFC's inconsistency were to be found then your model would therefore be inconsistent because you would have a proof of a theorem that is the negation of an axiom of the model. (Case in point: Any theorem that is conditional on the consistency of ZFC would still be conditional on the consistency of ZFC+n, so you wouldn't gain the ability to prove anything new!) Veky: I wasn't intending my analogy of axiom schemata to be particularly formal or rigorous; I only meant to illustrate the relationship between axiom schemata and axioms. In the case of the axiom schema of replacement, expressing the assumption as a single axiom would require the use of second-order logic; this is undesirable because ZFC is formally a theory in first-order logic. (Again, this isn't intended to be rigorous, but nothing says you CAN'T discuss ZFC using second-order logic -- we'd just rather not.)

benneh: T1 is obviously more complicated than ZFC, since it can speak about ZFC's proofs. That means it surely qualifies for Gödel2. Also, T2 is even more complicated. And so on. Tn cannot suddenly become so simple that Gödel2 doesn't apply. Of course, you can try to exploit a loophole by having Tn have non-r.e. axioms. But then its proofs are pretty much arbitrary, and there is no particular reason we'd believe them when they say the Tn is consistent. [See "Seventh:" in my rant above.:] Coda: being second-order is not "an undesirable property of an axiom", but a property of the whole logical environment. I still think you have clumsily expressed yourself. But it's not so bad if it was just a surface analogy.

Veky: I totally agree I've clumsily expressed myself. :P

Veky: When you say "T1 is obviously more complicated than ZFC, since it can speak about ZFC's proofs. That means it surely qualifies for Gödel2.", is there some formal reason to expect that? I agree that, intuitively, it seems entirely reasonable. But is it actually true?

Is it actually true, depends on a lot of technical details. (I thought we were speaking informally.) The biggest elephant in the room is, what exactly is Con(T)? [The concrete sentence in theory T, whose unprovability we refer to when we say "T can't prove its consistency".] Unfortunately, there is no universal answer. We would like to say it is a sentence which is true (in T's standard model, another can of worms) if T is consistent, and false if T is inconsistent. But that sentence is obviously parametrized by T: different theories can have different _languages_, so surely there cannot be "one size fits all" Con sentence. But once we acknowledge that, the problem is trivial: any tautology can be used as Con(T) for consistent theories, and any antitautology can be used for inconsistent theories. That obviously is not what is meant. :-) Intuitively, Con(T) has to somehow "speak about" proving process of T: it has to have identifiable parts that we can recognize as formulas, axioms, rules of inference and so on. But that's not something we can uniformly rigorously define for all theories T. The usual copout is to say "well, it just has to be able to formalize Gödel's proof of Gödel1". And that is a bit more concrete, but it has the unfortunate consequence of requiring arithmetics, since that is what Gödel used. :-) It is a bit arbitrary, but it does standardize that part quite well. So, in that sense, T1 (and T2 and...) surely qualify. But it is entirely possible that someone one day finds another, fundamentally different, way of specifying what Con'(T) should be, and everyone agreeing that it accords with their intuitive meaning of "T is consistent", but Con'(T) not requiring arithmetic to express. It is not a mathematical statement, it is more a value judgement - just like Church-Turing's Thesis, for example.

I see. Thanks for the in-depth reply. So, basically, the answer to my question is that, while no example of the sort of situation I described is known, the question itself can't be formalised in such a way that it's possible to prove that no such example can exist. Is that a fair assessment of our discussion?

@Veky >>"The biggest elephant in the room is, what exactly is Con(T)? [The concrete sentence in theory T, whose unprovability we refer to when we say "T can't prove its consistency".].... I don't quite follow you here... As you indicate in your next paragraph, the answer seems to be fairly trivial? e.g. Con(T) could be '~A=A is not a theorem'. But you seem to anticipate that when you say "That obviously is not what is meant." But I wasn't really quite sure why that is not sufficient.

@Sabin: The point is that such a simple statement, in and of itself, doesn't actually tell us anything. It's just a restatement of an axiom or a logical consequence of the axioms. A trivial proof for a trivial statement wouldn't actually prove the consistency of the model. (The simplest proof, of course, would simply be "by definition.") Instead of demonstrating a proof for that statement, you would have to demonstrate that there does not exist a proof for the inverse of that statement -- that is, you have to prove a fact about proofs themselves. In plain English, the sentence COULD be "there does not exist a proof that ~A=A is a theorem." Unfortunately, there's no way to even EXPRESS that in most formal languages. It's certainly not possible in ZFC's standard language. You could potentially EXPRESS it in some semantic representation of second-order logic, but Godel's theorem implies that no proof exists -- and if you could actually FIND a proof, it asserts that this would imply that second-order logic (or at least your chosen model of second-order logic) is inconsistent. It IS possible to use such a statement to prove the consistency of ZFC using a more powerful model (e.g. something based on second-order logic) but that doesn't invalidate Godel's theorem.

@Coda I mean, I agree with the end result, which is that there's no getting around Godel's theorem. But I think you're losing me on some of the particulars. Specifically, I think where you lost me is "[Expressing 'there does not exist a proof that ~A=A is a theorem'] is certainly not possible in ZFC's standard language". Granted, it's been awhile since I read this portion but as long as we're talking GEB, I thought that type of self-introspection that the whole point of Hofstadter's "proof-pair" concept? The plain-English "there does not exist a proof that ~A=A is a theorem", works out roughly to something like ∃X[ProofPair{X,"~A=A"}] To clarify, I'm not suggesting that one can PROVE such an expression. I'm just a bit confused because the general tone of the discussion seems to suggest that it's not even possible to EXPRESS such a statement.

I think Coda is again clumsily expressing themself. ;-P "ZFC standard language" probably means "ZFC language interpreted in the standard model", which certainly means it talks about sets and their elements, not formulas and their inferences. But one of Gödel's big insights (which is in fact Hilbert's, but no idea in math is named by its first thinker anyway:) was that "standardness" of language has nothing to do with the theory itself. Logicians often use the phrase "intended interpretation", which means "whatever the human who first wrote the axioms had in mind while writing them". Zermelo and Fraenkel did have sets in mind, and Peano did have arithmetic - and it's usually obvious _to us, humans_, what the intended interpretation is. But it is a social-cultural thing, it cannot be deduced from the theory itself. Computers can deduce whatever consequences of ZFC axioms we can, but I assure you they don't have the slightest idea what the theorems they prove are talking _about_. (Maybe some day they will. I'm not saying strong AI is impossible - just that it's unnecessary for employing a logical theory.;) And it is in no way a handicap. Now I guess it is obvious what's the problem. Whenever someone writes the axioms for a theory T, it is very unlikely that their _intended interpretation_ of these axioms includes such things as proofs in theory T. When you design a computer program to print out some text, it's usual that the text it prints is a combination of fixed text ['axioms'] that's part of the program, and outputs calculated from the inputs ['assumptions'] of the program. It is not very usual that the text refers to program itself, or the process of printing itself. [But not impossible - see quines.;] And that is all that is meant by "Con(T) cannot be standardly expressed in most theories T". It usually requires some reinterpretation, and we are not sure whether that reinterpretation preserves what we want from the theory. Designing something that can be trusted to meaningfully speak about, for instance, points and lines, and also about its own proofs, as a coherent whole, is hard - and even then, not terribly useful, because of Gödel2.

I always found Gödel's completeness theorem to be much more exciting than his incompleteness theorems.

@Veky I see your point now. I do think it's worth reiterating point 10 of your original post: regardless of the intention of the author of theory T, you can still use its axioms to create a "proof formula", and you can still write a sentence of T which talks about aforementioned formula. I don't think these facts erode the usefulness or meaning of T as a whole.

Once again Veky corrects me on my verbiage, so thank you. :) I'm a software engineer by trade, and abstract math is just a hobby that I don't spend nearly enough time on. My ability to reason about things moves a lot faster than my ability to communicate that reasoning in English. (Heaven forbid you ask me to do it in something that ISN'T my native language! I'd fall flat on my face trying to figure out the appropriate jargon in Japanese.)

Sabin: _for some theories T_, yes. Usually, when theories want to "formalize the whole mathematics", they have to be able to formalize the logic itself, too. But there are many theories (e.g. Euclidean geometry) that do not aspire to be the whole mathematics formalizers, and where we don't have a clear idea of what would a "proof sentence" be. Even more to the point, there are concrete axiomatizations of the (first-order part of) Euclidean geometry [for example Tarski's one], where we _know_ there is no proof formula, since it is proved to be consistent and complete, and in fact decidable. So yes, there are theories where Gödel's incompleteness provably doesn't apply, and there are many more where the question doesn't make sense. The usual web-discussions don't notice that phenomenon since the amateurs tend to focus on "universal" theories like ZFC, where you do have enough expressiveness to go meta without big problems. But not all theories are like that.

There are already 500000(+/-500000) summaries of the Incompleteness Theorem online. Why another?

For the same reason the other 5e5 were written. Because people think that it's incredibly simple, _and_ that everybody else gets it wrong. Both of those ideas are the consequences of focusing on some, but different, technical details in the proof. :-)

I was actually just trying to explain it to myself. Apparently I failed. I'm not sure if the essay as it currently exists is salvageable so I may take it down.

It's better than at least 100000 of those 500000 the Gödstadter is talking about. :-) Don't worry, I could tear down many others too, it's just that your commenting system doesn't hassle people with registering. :-] And also, based on your other texts, I had a feeling you _would_ understand my comments, unlike many other "Gödevangelists" on the web. I think it should stay. It, together with the comments, presents a nice view of what often goes wrong in such explanations. Of course, if you're _embarassed_ by it, then it probably should be taken down. But honestly, there are texts on qntm.org you should be more embarassed by. :-D

I don't think that's really entirely accurate, Veky, at least the part about people thinking everyone else has it wrong. Rather, most people I know who have seriously studied Godel have had a "Eureka" moment at some point, where everything finally clicks; that one part of things that makes you say, "Ahhhh, if I had only read that 100 pages ago, I would have understood it immediately!" So of course the natural inclination is to try to use that knowledge to help others. In other words it's less an issue of hubris and more just someone trying to be sincerely helpful. The trouble, I've found, is that everyone's "Eureka Moment" tends to be different, and so everyone's summary of GIT tends to overly simplify that which isn't related to that key part of things.

Sabin: I'm not really sure you're saying something different than I am. "Everybody else got it wrong" meaning not "they don't understand", but "they put focus on some irrelevant detail". :-)

"This is highly undesirable because it renders mathematics totally useless." But we still will have been able to launch rocket ships to space. That's an interesting notion of useless you have there.

fhyve: qntm saved himself with an asterisk. See also my "Sixth:" remark above. ;-) Of course, even if basic logic is found to be incomplete some day, we will just base our mathematics on something else. Usefulness of mathematics does not require its base to be consistent internally, it just requires the conclusions to be consistent with the world. But in fact your objection is philosophically deeper. See Winger, The Unreasonable Effectiveness of Mathematics in Natural Sciences. Even if we assume consistency, it doesn't explain usefulness in any reasonable way. People have thought about that for a long time, and have some partial answers - but my hunch is that those are separate phenomena. Being able to derive X from Y is different thing than actually deriving it; and _that_ is again a different thing than expecting the real world to reflect X.

@qntm As an almost complete mathematical layman, I appreciate the essay. It mirrors and helps reinforce my previous readings on Gödel's theorems and it is very easily accessible. When divulging knowledge, there often must be a tradeoff between correctness and accessibility.

@qntm: > Is it actually possible to express "ZFC is consistent" in the form of an axiom? I'm not sure if this has been answered yet, but if not, the standard way is to encode ZFC-proofs (using, e.g., Gödel-encoding), and then make the axiom state "it is not the case that a contradiction is provable" (symbolically, "¬□⊥" or "¬□(1=0)"),

Great post.

I thought the issue with undecidable statements isn't that they're "really" true or false, but we can't determine which one; but rather that you can take an undecidable statement, *or its inverse*, and either way derive a consistent, if not necessarily intuitive, system. After all, if it were "really" one way or the other, then a proof by contradiction should be possible! For a concrete example of this kind of thing, the parallel postulate is undecidable in the context of the rest of Euclidean geometry; which is convenient, because hyperbolic geometry is "Euclidean geometry minus the parallel postulate plus an axiom that contradicts the parallel postulate". You can actually derive theorems that must apply to both geometries, simply by ignoring what triangles and parallel lines do. (In fact, many of the early theorems of hyperbolic geometry were attempts at proof by contradiction. If you derived a weird enough quadrilateral, then surely your axioms weren't "really" true!) This kind of thing is just less obvious in the context of number theory, because undecidable statements tend to produce numbers that don't intuitively resemble "normal" numbers.

Referring to the issue of provability of consistency of the Arithmetic System, I'd like to inform you about the paper: T. J. Stępień, Ł. T. Stępień, „On the Consistency of the Arithmetic System”, Journal of Mathematics and System Science, vol. 7, 43 (2017), arXiv:1803.11072 . In this paper a proof of the consistency of the Arithmetic System has been published, this proof has been done within this Arithmetic System. <br/> Previously, in 2009, Dr Teodor J. Stepien and me delivered a talk at "Logic Colloquium 2009" in Sofia (Bulgaria). During this talk, a sketch of the proof of the consistency of the Arithmetic System was presented. <br/> The abstract of this talk was published in The Bulletin of Symbolic Logic: T. J. Stepien and L. T. Stepien, "On the consistency of Peano's Arithmetic System" , Bull. Symb. Logic 16, No. 1, 132 (2010), http://www.math.ucla.edu/~asl/bsl/1601-toc.htm .

I've come to the conclusion that there are some S that are so bad that both S and ~S are not true. Stupid example: "This statement cannot be proved true." So far I haven't been able to make a non self-referential one after allowing for a Y combinator reduction. (That is, if you load a Y combinator I simplify by replacing the Y combinator with This statement...)