Relations between Gödel's theorems

I think, this is connected to this question, but I am not sure.

I am reading books on mathematical logic, and I face various difficulties in understanding details related to Gödel's theorems. I would appreciate if somebody could help me with the following.

Joseph Shoenfield in his book gives the following formulation of the Gödel completeness theorem:

A theory T is consistent iff it has a model.

I think I don't understand something, but for me this looks like a statement that, in particular, the Peano arithmetic must be consistent, since it has a model as well. On the other hand, the second Gödel incompleteness theorem states the following:

Assume T is a consistent formalized system which contains elementary arithmetic. Then the statement that T is consistent is not deducible inside T.

I would think that this means impossibility to prove the consistency of Peano's arithmetic (within the predicate logic), since

Suppose we "proved the consistency of PA in some theory $T$". Then a question immediately arises if $T$ itself is consistent, because if $T$ is inconsistent, then each statement (i.e. each formula) $A$ in $T$ is deducible in $T$ together with its negation $\neg A$. In particular, the statement "PA is consistent" is deducible together with the statement "PA is inconsistent". So we come to a situation where for proving what we want we have to continue our work, and prove that the theory $T$ is consistent as well. But by the second Gödel theorem, this is impossible inside $T$, and we have to find another theory $T_1$, and so on. And the question remains open at each step.

And for me, as an outlooker (I am a specialist in analysis, not in logic), this contradicts to the previous statement that PA is consistent.

What do I miss here? How is this "contradiction" settled? If in the Gödel completeness theorem people mean the relative consistency, why isn't this stated explicitly?

EDIT. To people who vote to close this question: could you, please, explain your motives?

• "this means that it is impossible to prove the consistency of Peano's arithmetic." NO: this means that the formal system of first-order PA cannot prove its own consitency. – Mauro ALLEGRANZA Jun 7 '17 at 11:58
• "Peano arithmetic must be consistent, since it has a model ". Intuitively, YES: the "usual" natural numbers are a model of PA. But a formal proof of it requires the "maufacturing" of a structure and a formal proof that this structure satisfies Peano's axioms. This can be done in some formal tehoery: e.g. ZF set theory. – Mauro ALLEGRANZA Jun 7 '17 at 12:00
• In the second Gödel theorem the theory T not necessarily coincides with PA, it just contains PA. Wouldn't it be correct to say that this implies the impossibility to prove the consistency of PA? – Sergei Akbarov Jun 7 '17 at 12:03
• Your first comment: NO; see Gentzen's consistency proof: a theory T "containing" PA can prove PA's consistency. Nevetheless, by G's 2nd Th, T cannot prove T's consistency. – Mauro ALLEGRANZA Jun 7 '17 at 12:35
• @SergeiAkbarov It's not about relative consistency, the point is that the theory in which your argument is carried out isn't PA itself, so there's no paradox; see my answer for further details. – Noah Schweber Jun 7 '17 at 15:08

1 Answer

EDIT:

Based on the comment thread, I think the underlying question here is: how is mathematical logic, as a field, "done"? And this is a special case of asking how mathematics is done. While focusing on logic may predispose one towards one method or another, ultimately those same methods make sense for all of mathematics.

In what follows I'm going to ignore the issue of the consistency of the formal theories we consider; I'll come back to this at the end. Also, the usual caveat: everything I say below is my own opinion and need not reflect the opinions of other mathematicians.

There are to my mind three basic ways of viewing the activity of mathematics. Many mathematicians, myself included, don't adhere to one particular way all the time, so this is somewhat artificial, but I think it's very useful in understanding mathematics as practiced and will also help address your concerns:

Mathematics as informal-but-precise

At one pole we have mathematics as usually practiced: perhaps surprisingly, it is extremely (from a logical standpoint) informal. If you look at an advanced textbook, or a research article, you'll quickly see what I mean: there is almost never any talk of a specific axiom system being used. There are exceptions - sometimes one axiom or another is singled out as being not "intuitively obvious," usually the axiom of choice, and then it is either not used or its use is explicitly remarked - but usually all arguments are via "intuitively obvious" principles, including principles about sets. Incidentally, ZFC and the other set theories emerged mostly as an attempt to articulate those principles precisely.

In this context, here's how one mathematician would tell another mathematician about the completeness theorem: $$\mbox{"If T is a consistent first-order theory, then T has a model. Here's the proof: ..."}$$ Note that the completeness theorem is not qualified by reference to any external axiom system, and the "proof" is an argument in natural language.

This is how mathematics is practiced almost always. But one might reasonably find this unsatisfying; and logicians are, in my experience, somewhat more likely to be uncomfortable with the above picture than mathematicians in general. This takes us to the middle of the road:

Mathematics as formalizable arguments

There is a natural fix for the above approach, which doesn't require us to change our practices too much: we can add a layer of interpretation to the above idea, which fortuitously tends to match working mathematicians' attitudes towards axiom systems in general.

This layer of interpretation is that it is left to the reader to isolate an appropriate axiom system in which the given informal proof can be formalized and is valid. The reader is free to choose the system in question, so long as it fits those criteria.

How does this work? Let's say I read Wiles' paper proving Fermat's last theorem (FLT). Now, this paper never mentions a specific axiom system; indeed, I believe (the pdf is not searchable unfortunately) that the word "axiom" is never even mentioned. But the paper concludes "FLT is true."

Reading the paper, I want to convince myself that there is a formal theory $T$ such that $T$ proves FLT, by essentially the argument in the paper. Depending on how much I care about parsimoniousness, I might try to make $T$ as weak as possible (and this is an active area of research - Colin McLarty is working on proving FLT from the smallest set of axioms possible), but maybe I just want some theory that does the job.

It's here that the value of ZFC reveals itself. On the one hand its axioms are extremely well justified from an intuitive standpoint (this is of course opinion, but I believe it is almost universal amongst those interested in formal set theories), especially if we drop the axiom of choice, so a proof from ZFC (or better, ZF) would be taken as a proof, full stop, by the vast majority of the mathematical community. On the other hand it is so powerful that with a bit of experience it's usually easy to convince oneself that a given argument can be translated into it. In particular, even if one doubts ZFC's "acceptability" (whether because one is doubtful that it is consistent, or some other reason), it is easy to convince oneself that the argument given can be converted to a ZFC proof.

Note that there's a separate issue of usability: ZFC is notoriously bad to actually work with - but we're not actually trying to produce a proof here, just convince ourselves that one exists, and for that ZFC is extremely satisfactory. I've said more about this in my answer to another question.

In this context, here's how one mathematician would tell another mathematician about the completeness theorem: $$\mbox{"Suppose T is a theory that can prove some basic facts about infinite sets like ....}$$ $$\mbox{Then T proves "Every consistent theory has a model."}$$ Often when we're extremely confident about the naturalness of the axioms used, we'll say "Any reasonable theory of sets $T$ can prove "every consistent theory has a model," even though this is substantially closer to the previous approach to mathematics.

Of course, given all this there is a serious question of what constitutes a proof, even though we have more rigor here than in the previous version. Part of this is the problem of convincing-but-wrong proofs, or proofs which are formalizable in a reasonable axiom system, but need a bit more than ZFC even though that's not apparent. his is a serious and long-running debate within mathematics which I will not attempt to summarize here.

Whatever its flaws, the other pole of mathematics-as-activity certainly avoids this dilemma. Speaking of which, that other pole is:

Mathematics as the construction of formal proofs

Here the only statements we are comfortable with are those of the form

$$(*)\quad\mbox{\mathfrak{S} is a proof of \varphi in T,}$$ where $T$ is a first-order theory, $\varphi$ is a sentence in the language of $T$, and $\mathfrak{S}$ is a formal proof of $\varphi$ from the axioms of $T$. $(*)$ is a purely finite statement, and is checkable by a computer, so the philosophical issues around mathematical truth, existence, etc. don't even crop up.

These mathematicians might not be interested in looking at informal proofs except as recipes for producing formal proofs. For such a mathematician, we never assert what the other two types of mathematician might call "mathematical facts" - we assert claims of provability from specific systems, and back those claims up with actual, ideally computer-checkable formal proofs.

In this context, here's how one mathematician would tell another mathematician about the completeness theorem: $$\mbox{Here's a proof of "every consistent theory T has a model" in ZFC.}$$ Another thing they might say is $$\mbox{Here's a proof of "every consistent theory T has a model" in WKL_0.}$$ And so on. I believe statements like this are the ones you'll be most comfortable with, at least at first.

The only step I've left out is the work of expressing a sentence like "every consistent theory $T$ has a model" in the given formal language, and in fact the totally formal mathematician would view this as ultimately unperformable: at best, the sentence $\varphi$ is a formal sentence which corresponds in some way to the natural language sentence "every consistent theory $T$ has a model."

Note that this constitutes a meaningful step away from the idea of proof as illuminating - a formal proof, even after being computer-checked, need not give the reader any understanding of why the result is true in the given axiom system. For this reason formal proofs (think the four-color theorem, Kepler's conjecture, etc.) are often viewed as unsatisfactory by the mathematical community, even though they are far more rigorous.



Okay, now let's talk about the elephant in the room:

Consistency

Let's go bottom-to-top.

The lovely thing about formal proofs is that consistency plays no role in the facts we assert! When I exhibit a formal proof of $\varphi$ in $T$, I don't need to qualify it with "if $T$ is consistent;" regardless of $T$'s consistency, I know now that $T$ proves $\varphi$. If $T$ is inconsistent this fact is trivial, but it doesn't make it false. So while I'm more interested in statements of the form "$\mathfrak{S}$ is a proof of $\varphi$ from $T$" for consistent $T$, nothing breaks down if a theory I thought was consistent turns out to be inconsistent.

For the second approach things are more nuanced. Let's say we find out that ZFC is inconsistent. Then we now know that every time we accepted a proof by saying, "It goes through in ZFC" (or stronger), we made a terrible mistake; and now we need to go back to those results and reexamine them to see if we can convince ourselves that they can be proved in a theory $T$ which we still think is consistent. It is generally agreed that the answer would almost always be yes.

For the first approach the game fundamentally changes. The consistency of formal theories is a non-issue, since we're not working inside one in the first place; so the relevant consistency issue is whether we can prove a contradiction from "intuitively obvious" first principles.

Now there's an extremely interesting story here: how this issue cropped up in the past, and how it was handled. I can think of a few instances that might or might not count. Note that I'm not a historian, so I'm woefully unqualified to comment here, but that's never stopped me before!

• The earlies candidate is irrational numbers. There's a famous story, whose veracity I'm not prepared to argue for of the reaction to the discovery of irrational numbers - according to the story (whose veracity I'm not prepared to argue for), they contradicted an existing philosophy/theology of numbers. However, this tended to not be a major problem for those outside this philosophy, as far as I know.

• A wonderfully explicit example is provided by Non-Euclidean geometries. This is because it became a huge philosophical focus point: Kant argued, and many mathematicians and philosophers agreed, that non-Euclidean geometries would contradict our fundamental intuitions about reality to the point of arguably being epistemologically impossible. (OK, what Kant said was more nuanced, I'm not a philosopher, sue me.) Out of fairness I should say that some people have argued that the discovery of non-Euclidean geometries is actually not damaging to Kant's philosophy; I disagree, but it should be mentioned.

• Yet another instance of this is the gradual acceptance of complex numbers, starting with their appearance in intermediate steps of the solution to a cubic equation and continuing on through their acceptance as consistent objects to the general belief in their existence on par with other mathematical entities (not universally accepted of course).

• The definition of "function" evolved to allow such beasts as the Dirichlet function, which were originally not considered functions in the first place. This isn't really a contradiction of axioms, but should count partly on this list since it represents a clashing of fundamental intuitions (about what a function should be), and also because historically it helped setthe stage for ...

• ... The axiom of choice, which provides maybe the most on-point example, Kant notwithstanding. You may have heard the joke "The axiom of choice is obviously true, the well-ordering principle is obviously false, and who can tell about Zorn's lemma."

What's fascinating about this is that in each case, mathematical practice stabilized (quickly or eventually). In particular, in the case of the axiom of choice, the axiom was eventually largely accepted by the mathematical community, the intuitions for it trumping the intuitions against it (and this battle between intuitions being affected by the axiom's implicit role in existing mathematics). This was the closest to a genuine "rift," I think - there are many more mathematicians seriously skeptical of the axiom of choice than of (as far as I know) complex numbers, nowhere-continuous functions, etc. - but even here a stable state emerged: unless otherwise mentioned, the axiom of choice is taken as accepted (or is irrelevant) in mathematical proofs. At the same time, it is perfectly respectable to study mathematics without choice, or assuming an actual denial of choice, so long as it is explicitly done. So even though no intuition in particular "won out" totally, our understanding of those fundamental intuitions emerged to the point that they no longer pose a problem to each other, and the practice that emerged ultimately makes perfect sense once we view mathematics as a social activity.

So what's the completeness theorem?

• Every consistent theory has a model.

• Any "reasonable" set theory proves that every consistent theory has a model.

• Check it out, here's a computer-verified proof of the sentence "every consistent theory has a model" in ZFC: [exercise for the reader]. And here's a computer-verified proof of the sentence "every consistent theory has a model" in WKL$_0$: [another exercise for the reader]. Neat, huh?

Regardless of which one you pick, the argument you've outlined in your question breaks down immediately, and so there's no problem.









Original answer:

As almost always is the case with such questions, the issue is: where are you proving the assertions you make?

Let's work with ZFC instead of PA, for simplicty (I'll explain why below). Then your argument looks like:

• If ZFC has a model, then ZFC is consistent. (You only need this direction, the soundness theorem, rather than the whole completeness theorem.)

• ZFC has a model. (This is less intuitively obvious than "PA has a model," but bear with me for now.)

• Therefore ZFC is consistent.

• But now we've proved the consistency of ZFC, contradicting Incompleteness.

Now, ZFC certainly proves the soundness theorem. The issue here is the second bullet point: ZFC cannot prove that ZFC has a model! So the theory in which we've proved "ZFC is consistent" is a theory stronger than ZFC itself, and so there's no problem here.

So the issue is: the crucial step in your argument is arguing that the theory in question has a model in the first place, and this - no matter how obvious to you - cannot be done in that theory itself.

Now why did I work in ZFC rather than PA?

Well, it turns out that PA is absolutely terrible at talking about models! A model is a set together with some relations and functions. Well, by the Ackermann interpretation (see Section 5 of this article), PA can talk about finite sets; but not infinite sets! This means, among other things:

• PA proves that PA has no model, since PA proves that any model of PA would have to be infinite.

• In fact, PA disproves the completeness theorem - PA proves that Robinson's theory $Q$ is consistent, but also proves that any model of $Q$ must be infinite, hence proves that $Q$ has no models.

So PA is a terrible theory to work in if we're doing model theory.

Instead, we need to work in a theory capable of handling infinite sets. This actually isn't much of a requirement: above I worked with the ultra-strong theory ZFC, since it's well-known, but there are satisfactory theories which are consistent relative to PA - for example, the theory WKL$_0$ proves the completeness theorem, and PA proves that WKL$_0$ is consistent! So externally we can say, "Obviously WKL$_0$ has a model," but that assertion can't be made in WKL$_0$ itself.

Incidentally, there are ways to do model theory inside PA - see e.g. the "arithmetized completeness theorem" - but they're much more involved, and I'm ignoring them here for simplicity.

• The problem will disappear as soon as you realize that no (reasonable) theory proves that it has a model. That's it - that resolves the entire issue. Even if such a theory proves the completeness theorem, it won't be able to apply it in the way that you've indicated. – Noah Schweber Jun 7 '17 at 17:53
• @SergeiAkbarov What does "has a model in $T$" mean? The only thing that can mean is "$T$-provably has a model" - a theory isn't a structure in which models actually exist, it's a set of sentences saying certain things. And no, you need the adjective "reasonable" - firstly, there are very strange weak theories, and a too-weak theory might not be able to conclude that a theory is consistent by virtue of it having a model (as strange as that sounds); and secondly, in order for "$T$ has a model" to even be expressible $T$ needs to be appropriately definable. – Noah Schweber Jun 7 '17 at 18:02
• (Similar "reasonability" assumptions, by the way, are needed in Goedel's incompleteness theorem: e.g. Dan Willard has studied consistent theories which prove their own consistency, and do so by virtue of not being strong enough for the Goedel analysis to apply.) So, to sum up: I mean exactly what I wrote. – Noah Schweber Jun 7 '17 at 18:03
• @SergeiAkbarov "If the enveloping theory is inconsistent then one can prove that the inner theory is inconsistent as well." No, if the enveloping theory is inconsistent then that theory proves that the inner theory is also inconsistent; but that need not mean that the inner theory is, actually, inconsistent! Inconsistent theories prove false things - e.g. if $T$ is inconsistent, then $T$ proves "$PA$ is inconsistent," but you don't believe $PA$ is inconsistent do you? – Noah Schweber Jun 7 '17 at 19:16
• @SergeiAkbarov Asaf has been perfectly clear. If you don't understand what he's saying, state a specific confusion; what point don't you get? – Noah Schweber Jun 11 '17 at 19:34