Godel's completeness theorem and formula that states consistency of ZF

Godel's completeness theorem, in original formulation, says that every logically valid statement/formula has finite deduction of a formula. Now then there is Godel's incompleteness theorem. Would this mean formula that states consistency of ZF does not exist without invoking a stronger axiomatic system?

Edit:

OK. So formula that states consistency exists. Then, what about its compatibility with completeness theorem? Is Godel's original formulation wrong, or am I interpreting in a wrong way? Contrapositive of Godle's completeness theorem in original formulation seems that if a formula does not have finite deduction, formula is not logically valid...

• You have no "ö" on your keyboard ? – callculus Jul 30 '14 at 3:31
• @calculus: Some of us don't have umlauts easily available. Perhaps many of us. Myself included. – Asaf Karagila Jul 30 '14 at 3:32
• @AsafKaragila I thought as much. It was more or less a joke. Nice to see, that you know the word umlaut(e), it is almost equal to the german word. – callculus Jul 30 '14 at 3:40
• You seem to be confusing existence of a formula with deduciblity of that formula in a particular formal system. The formula that says that ZFC is consistent exists, as Asaf explained, in any system that includes enough elementary arithmetic; so ZFC is more than enough for that. But this formula is not deducible in ZF; for deducibility you need a stronger axiomatic system. – Andreas Blass Jul 30 '14 at 3:59
• But then that seems to suggest that a consistency formula is not logically valid by completeness theorem (because contrapositive is that "if there is not finite deduction of a formula then a formula is not logically valid." – LAM Jul 30 '14 at 4:25

No. Not at all.

If a language has Godel numbering (and certainly the language of set theory with only $\in$ has that), then asserting that a theory in that language is consistent is a number theoretic statement. Namely, it's a statement about integers.

Of course, we need to assume that the numbers encoding the axioms of the theory make a definable set of integers, but we can always assume that (or else we can add a predicate to the language of Peano arithmetic whose interpretation is this collection of codes).

Now the statement of $\operatorname{Con}(T)$ is really just saying that there is no proof that $\exists x(x\neq x)$ from the axioms of $T$, or rather there is no code for a proof of the Godel number of $\exists x(x\neq x)$ (or some other form of false statement) from the Godel numbers of the axioms in $T$.

All that we really need from our theory is to allow us to internalize first-order logic. This can be done with theories much much weaker than $\sf ZFC$. And if you look at some set theory books, you might find there that set theory can be developed within a theory as weak as $\sf PRA$ (which is a weak fragment of Peano arithmetic).

Of course in that sort of context we can't talk about models, we can't say that a theory is consistent if and only if it has a model. But consistency is in its essence syntactical and requires us to be able to talk about proofs, not about interpretations and satisfaction. So there's no harm there.

To the edit let me point out that while both "completeness" and "incompleteness" have similar names, they talk about different types of completeness, and they are not quite related.

The incompleteness theorems tells us that $\sf ZF$ cannot prove its own consistency. This is, essentially, a theorem about proofs and syntax. But as a consequence of this theorem we know that assuming that $\sf ZF$ is consistent at all, then the theory $\sf ZF+\lnot\operatorname{Con}(ZF)$ is consistent. The completeness theorem then tells us that this theory has a model $(M,E)$.

And this model $M$ is such that there is no $(N,E')\in M$ such that $M$ "thinks" that $N$ is a model of $\sf ZF$.

There are a lot of very delicate points here about internal and external properties of these models.

And of course, in order to talk about the existence of a model we need to be able to talk about models, which are sets, so we need some rudimentary set theory at our disposal.