# Consistency and Gödel's Incompleteness theorem.

In Mathematical Logic, Kleene states a string of implications that are a result of Gödel's completeness theorem of predicate logic;

$$\{E_1,...,E_k \vdash P\&\neg{P}\} \rightarrow \{E_1,...,E_k \vDash P\&\neg{P}\} \rightarrow \\\{E_1,...,E_k\,\text{are not simultaneously satisfiable}\}.$$

He says that the contraposition shows that $$E_1,...,E_k$$ cannot derive a contradiction. In other words finding a model that simultaneously satisfies $$E_1,...,E_k$$ is sufficient enough to show its consistency.

I'm wondering why, if this is computationally possible, do we care about Gödel's incompleteness part two, where a strong theory can't prove its own consistency? This process is in the observer's language but so is incompleteness. Is this process sufficient enough to verify consistency to ourselves?

• Completeness theorem says the existence of a model implies a theory is consistent. Incompleteness theorem says certain theories cannot prove their own consistency. For example, ZFC cannot prove its own consistency. All the completeness theorem implies on top of that is that ZFC cannot prove the existence of a model of ZFC, which seems like pertinent consequence of the incompleteness theorem that we should care about. – spaceisdarkgreen Feb 11 at 21:19
• Completeness theorem does give us a powerful new way to prove consistency (finding a model), but... we do actually need to prove the existence of a model, it doesn’t just happen by magic. – spaceisdarkgreen Feb 11 at 21:25

First of all, note that a consistent set of sentences - even a finite consistent set of sentences - may have no finite model. An easy example of this can be given by considering a language consisting of a single function symbol $$f$$, and looking at the sentence $$[\forall x,y(x=y\iff f(x)=f(y))]\quad\wedge\quad[\exists x\forall y(f(y)\not=x)].$$ This sentence is only true in infinite structures, since in any model of it the function named by $$f$$ is a non-surjective injection from the structure to itself.