Understanding an interpretation of Godel's first incompleteness theorem.

Question

I'm having some trouble interpreting this statement from wikipedia:

Gödel's first incompleteness theorem shows that for languages sufficient for doing a certain amount of arithmetic, there can be no effective deductive system that is complete with respect to the intended interpretation of the symbolism of that language. Thus, not all sound deductive systems are complete in this special sense of completeness, in which the class of models (up to isomorphism) is restricted to the intended one

From what I understand, there is no such thing as "the intended interpretation" for an arbitrary formal system. For PA, it is just convention that the "intended interpretation" is the "usual natural numbers", presumably as formalized in something like ZFC. Thus, I am having trouble understanding what "there can be no effective deductive system that is complete with respect to the intended interpretation of the symbolism of that language" means -- i.e. exactly what is meant by the "intended interpretation" here. I don't think it can mean "any possible intended interpretation", for exampe, consider the following:

Suppose that we have some semantic consequence relation $\vDash$ between models $\mathscr{U}$ and propositions $\phi$ in the language of $\mathscr{U}$. Presumably, the implied metatheory in which we define this is ZFC. So really when we say $\mathscr{U} \vDash \phi$ we mean $\vdash_{ZFC} (\mathscr{U} \vDash \phi)$.

From this, I think we can define a new syntactically defined consequence relation by setting $\Gamma \vdash_{\mathscr{U}} \phi$ if and only if $\vdash_{ZFC} (\mathscr{U} \vDash \wedge(\Gamma) \to \phi )$, and from this deduce that $\vdash_{\mathscr{U}}$ is sound and complete (with respect to this one model $\mathscr{U}$). Note that, by $\wedge(\Gamma)$ I mean the pairwise conjunction of all formulas in $\Gamma$.

Thus, if my reasoning is correct here, it seems that the deductive system given by the consequence relation $\vdash_\mathscr{U}$ is sound and complete with respect to what we by fiat make the "intended interpretation" $\mathscr{U}$. Perhaps it is not effective?

Is my argument flawed in some way, or is the wikipedia article I linked badly-worded, inaccurate, and/or using some more specific notion of "the intended interpretation" of general deductive systems that I am not aware of?

Answer 1

Here's the answer I think you'll find most satisfying, first up: we don't need the soundness condition at all! Goedel's original argument did require a soundness condition, but Rosser improved it: we can prove (in PA) that if $T$ is any consistent r.e. theory in the language of arithmetic extending Robinson's $Q$, then $T$ is incomplete. This is a completely formalist fact, and doesn't need to invoke models at all.

Rosser's trick, by the way, was to replace the Goedel sentence $G_T=$"I am unprovable in $T$" with the modified sentence $R_T=$"For any $T$-proof of me, there is a shorter $T$-disproof of me." Reasoning inside PA, if $T\vdash R_T$ then let $\pi$ be the shortest $T$-proof of $R_T$. There are only finitely many $T$-proofs shorter than $\pi$, so $T$ can "check them all" - if one of them is a proof of $R_T$ then $T$ is inconsistent, and if none of them $R$ then in this way $T$ disproves $R_T$, so either way $T$ is inconsistent. Meanwhile if $T\vdash \neg R_T$, then there is a shortest proof $\pi$ of $\neg R_T$. If $T$ is consistent, then there is no $T$-proof of $R_T$, in particular no $T$-proof of $R_T$ shorter than $\pi$. Again by checking all the finitely many $T$-proofs shorter than $\pi$, $T$ verifies that if there is a $T$-proof of $R_T$ then it is longer than $\pi$; and this is a $T$-proof of $R_T$! So $T$ is inconsistent.

So for $T$ to be consistent, $R_T$ must be undecidable in $T$.

---

You've also made a serious mistake regarding your "$\vdash_\mathcal{U}$".

First of all, if we're doing everything formalistically (that is, not working in a background model of ZFC), then we can't really have a model $\mathcal{U}$ (we can't really talk about "actual models" without fixing a background universe of set theory). So instead, $\mathcal{U}$ should really be a definable model. E.g. any model of ZFC has an object it thinks is the natural numbers; there is a single formula which picks out the relevant object in each model of ZFC. This isn't a huge issue, but it's worth pointing out.

Now to the main point: the relation "$\varphi\vdash_\mathcal{U}\psi$" is not effective (well, its deduction rules are effective, but its set of tautologies isn't; what I really mean is not decidable - but note that for complete systems, effective = decidable) or complete, even for reasonably nice $\varphi,\psi,$ and $\mathcal{U}$. For instance, take $\mathcal{U}$ to be "the natural numbers" and $\varphi$ to be $\top$; then $\varphi\vdash_\mathcal{U}\psi$ iff $ZFC$ proves "The natural numbers satisfy $\psi$." But the set of arithmetic consequences of ZFC is not decidable or complete!

We can go more Platonistic: working within a universe of sets $V$, it is certainly the case that for each structure $\mathcal{U}\in V$ and each $\varphi$, either $V\models(\mathcal{U}\models\varphi)$ or $V\models(\mathcal{U}\models\neg\varphi)$, so the system is complete; however, now it is not effective since truth in $V$ cannot be effectively determined.

---

Now on to the "intended interpretation" issue.

Not all theories have intended interpretations in any sense. However, if $T$ is any theory including some theory of arithmetc $S$ (e.g. $T$ might have other symbols - a model of $T$ might look like a model of $S$ together with some other junk), then we can say that a "standard model" of $T$ is one where the $S$-part is the actual natural numbers. This definition is phrased in ZFC, so different models of ZFC may have different things they think are the actual natural numbers. ZFC now proves "If $S$ is sufficiently strong and $T$ has standard models (this is a soundness condition), then the set of arithmetic consequences of $T$ is not r.e. and complete."

Now I'm mostly a formalist, but I'd argue that we have to begin math with a thing we consider the "true natural numbers" to a certain extent, so I'm comfortable referring to the intended interpretation of a theory in the language of arithmetic; but even if one isn't, Goedel's theorem can be formulated and proved in ZFC as I've described above.

Answer 2

Your reasoning isn't quite correct. An absolutely essential feature of Incompleteness is the requirement that the set of axioms be "recursively enumerable" and that the proof system comprise a "recursively enumerable" set of rules - intuitively, a computer should be able to check whether or not a proof is valid. In the example you give, the set of axioms is every statement which is true in $\mathscr{U}$ - which, if $\mathscr{U}$ contains arithmetic in any sense, is far from recursively enumerable.

An even more trivial pseudo-counterexample to Incompleteness is $TA$ or "true arithmetic": this is the set of all sentences that are really true about the natural numbers. We could syntactically define a consequence relation based on this, and this consequence relation would have to be complete - but the definition is absurdly complicated, because $TA$ is itself extremely difficult to define.

To address the question of "the intended interpretation": it's easiest to think about it in terms of arithmetic. The requirement is that the language is powerful enough to express arithmetic; the "intended interpretation" is then any interpretation in which the "arithmetic" expressed is actually arithmetic.

Answer 3

The description you quote from Wikipedia is not very good. In particular, the theorem -- at least in the well-polished form that is usually given in contemporary texts -- does not speak about "intended models" at all.

Instead it speaks about systems that

1. are at least semi-decidable (that is, we can recognize algorithmically what are valid proofs when we see them),
2. are consistent,
3. can represent statements in the first-order language of arithmetic in a uniform way, such that
4. certain true statements of arithmetic (for example, all true statements with no free variables and only bounded quantification) are provable, and
5. respects the usual first-order proof rules for the representation of arithmetical statements.

For each such system, it produces an arithmetical statement whose representation in the system is neither provable or disprovable by the system.

This does not speak about any "intended interpretation" of the object system at all.

There is an intended interpretation at play in condition 4 above, namely for defining what we mean by "true" statements -- but then what we need are only arithmetical statements that are true in the intended interpretation of the language of arithmetic. Some Wikipedia editors must have confused that with intended interpretations of the system instead.

Answer 4

As Henning said, the "interpretation" involved in the incompleteness theorem refers to a different thing from "interpretation" in model theory. See this post for a general definition of "interpreting arithmetic" and both constructive and non-constructive proofs of the generalized incompleteness theorems for formal systems that interpret arithmetic. This applies to any conceivable practical formal system that has existed or will ever exist, not just those based on classical logic.

In particular, this addresses your query:

From what I understand, there is no such thing as "the intended interpretation" for an arbitrary formal system. For PA, it is just convention that the "intended interpretation" is the "usual natural numbers", presumably as formalized in something like ZFC. Thus, I am having trouble understanding what "there can be no effective deductive system that is complete with respect to the intended interpretation of the symbolism of that language" means -- i.e. exactly what is meant by the "intended interpretation" here.

The point of the general notion of "interpreting arithmetic" in my linked post is so that you can deal with formal systems that are not simply extensions of PA. In many textbooks you will find a much weaker notion of interpretation where you only deal with first-order theories and a limited form of translation of arithmetical sentences. However, the incompleteness theorems go far beyond that. Even a thoroughly non-classical formal system will fall to incompleteness so long as it can prove the same arithmetical sentences that PA can under a sufficiently nice translation, and that is the point of rigorously defining the generalized notion of interpretation.

For example, you could have an intuitionistic type theory that supports LEM (the law of excluded middle) for arithmetical sentences but not for general sentences, which would then be incomplete.

Another helpful viewpoint is that you could treat any practical formal system as a program that generates sentences (which you hope are meaningful and true). And the incompleteness theorems are merely saying that there is no program that generates all and only arithmetical sentences that are true, where "true" here means "satisfied by $\mathbb{N}$", where "$\mathbb{N}$" is from the meta-system's viewpoint simply a model of PA. If we go outside the meta-system, it may seem surprising that it does not matter which model of PA the meta-system uses! If so, remember that that same model is also the model based on which the meta-system constructed programs, so to make clear the actual crux of Godel's version of the incompleteness theorems we could state it this way:

Godel's Incompleteness theorem crux: No program represented by a standard natural number can enumerate all and only the first-order arithmetical sentences that are satisfied by the standard natural numbers.