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?
Best Answer
It's not, in any sense.
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.
So even in principle, searching through the finite structures isn't going to be enough. But it gets worse:
There are also consistent finite sets of sentences which don't even have computable models! (Tennenbaum's theorem is usually stated for PA, which is infinite, but it also applies to related finitely axiomatizable theories.)
And even worse, it's extremely non-computable to check whether a computable structure satisfies a given first-order sentence - in general, checking satisfaction of an $n$-quantifier sentence requires the $n$th iterate of the halting problem. This is neat because by contrast every consistent computable set of sentences does have a $0'$-computable (even low) model, so building models is somehow easier than checking models! (This is rightfully counterintuitive, see this previous math.stackexchange question.)