I am reading Enderton's A mathematical Introduction to Logic and have reached Gödel's Completeness Theorem for first order languages.

After introducing the new set of constant symbols, and proving consistency in the new language, then expanding $\Gamma$ to a new set $\Delta$ and introducing a new structure $\mathfrak{A}$, whose universe or carrier is the set of all terms in the expanded but with equality replaced by a new predicate $\mathrm{E}$, with interpretation $\mathrm{E}^\mathfrak{A}$ , we state the following claim:

$\mathfrak{A} \vDash \phi^{*} [s] \iff \phi \in \Delta$, where $s$ is the identity function on the set of variables and $\phi^{*}$ is $\phi$ but with the equality symbol replaced with the new predicate symbol.

I managed to follow through the proof of this claim. Now it is stated that if our original language did not include equality (then clearly $\phi^{*}$ is just $\phi$ ,at least when $\phi \in \Delta$), then we can just restrict the structure $\mathfrak{A}$ to the original language to complete the proof that $\Gamma$ is satisfied with that structure. This is not proved and I can not see why it is true.

I realize that right now I am not really following through this proof - I would be really glad if you can explain what is happening here.

Perhaps, even more so if you could shed some intuitive insight into the proof - what is the purpose of the new constants, why were the new formulas added to $\Gamma$ (formulas of the sort of $\lnot\forall x \phi \to \lnot \phi^{c}_{x})$ ?

The proof of the completeness theorem begins on page 135 in the book.

  • $\begingroup$ Regarding the last point: This construction gets rid of non-constructive proofs. That is, whenever you have a $\phi$ and can somehow prove $\exists x \neg\phi$, then you can also prove $\neg\phi^c_x$, in other words, $c$ is an explicit example. $\endgroup$ – Hagen von Eitzen Apr 18 '17 at 19:37
  • 2
    $\begingroup$ @HagenvonEitzen That's not really correct - it's not just about non-constructivity, it's that otherwise the structure wouldn't necessarily satisfy the desired theory! $\endgroup$ – Noah Schweber Apr 18 '17 at 19:39

This isn't quite an answer, but is way too long for a comment:

This proof is a bit oddly organized - let me outline a proof of completeness which in my opinion is simpler, and has the same basic idea (in particular, you'll see the role of adding to the language and the theory).

We start with a theory $T$. Now, associated to $T$ is a structure $M_T$ consisting of all equivalence classes of terms (with no free variables), where the equivalence relation is $T$-provability. E.g. if $T$ is the theory of arithmetic, then the terms $$S(1), \quad1+1, \quad(1+0)+1$$ each denote the same thing - that is, $T$ proves $S(1)=1+1$, etc. So these terms would all be equivalent, and their equivalence class would be a single element of $M_T$.

That describes the underlying set of $M_T$ - to turn this into a structure in the language of $T$, we interpret the nonlogical symbols according to $T$-provability. E.g. if $U$ is a unary relation symbol, then in $M_T$, we'll have $U([t])$ iff $T$ proves $U(t)$. (It's a good exercise to check that this is well-defined.) It should be clear how this idea extends to all possible symbols in the language.

Now it's natural to hope that $M_T$ is a model of $T$. However, in general this won't be the case. First of all, maybe the language of $T$ only has relation symbols - then there are no closed terms at all! More importantly, even if we have lots of terms, there will be no reason for $T$ to prove enough facts about the individual terms for $M_T$ to be a model of $T$.

For example, take the theory $T$ in the language $\{<, c, d\}$, which asserts that $<$ is a linear ordering and $c\not=d$. Then:

  • $c$ and $d$ are nonequivalent terms, so represent different elements in $M_T$.

  • $T$ doesn't prove $c<d$ or $d<c$ - so neither $[c]<[d]$ nor $[d]<[c]$ holds in $M_T$.

  • But then $M_T$ isn't a linear ordering!

The point is that $T$ isn't making enough decisions: it has these two terms $c$ and $d$, but it doesn't have enough axioms to tell how they relate to each other. So we'll want to pass from $T$ to a complete theory.

That explains why we might want to make the theory bigger - why might we want to increase the language? Well, this goes back to the idea of having too few terms. Let's look at the theory $T$ in the language $\{c\}$, where $T$ just says "$\exists x(x\not=c)$". Now $T$ only has one term, $c$; so the term model $M_T$ has a single element. But this element is equal to ($M_T$'s interpretation of) $c$! So $M_T$ doesn't satisfy "$\exists x(x\not=c)$." The problem is that $T$ proves that some object with a certain property should exist, but doesn't have a name for any such object.

To fix this, we'll add a new constant symbol $d$ to the language, and a new axiom "$c\not=d$" to the theory. The term model of this theory consists of two elements, $[c]$ and $[d]$, which are different - and this is a model of the new theory, and hence of $T$ itself!

So that's what's going on there. We need to expand the language so that we have "enough terms" to name all the things we want to name, and then add axioms so that we decide all the things we need to - in particular, each time we prove "there is a thing with [property]," we'd better have a specific term in our language and an axiom in our theory that says that that term has [property].

I think this is more understandable than the proof you've outlined - and I suspect that once you understand this motivation, you'll be able to see what your proof is doing.

| cite | improve this answer | |
  • $\begingroup$ Thanks, your comment sure made some things clearer , but perhaps I need to reread it a couple of times. In the text, the author doesn't mention nowhere that the new structure will contain only closed terms (without free variables), but instead its the set of all terms. Does that make the argument different or is it analagous? $\endgroup$ – Georgi Stefanov Apr 18 '17 at 20:10
  • $\begingroup$ @GeorgiStefanov It doesn't make it substantially different, but I find that including non-closed formulas in sets of axioms is often confusing because there's an urge to universalize them. And there's no need to include them, and we have to add terms anyways, so I leave them out. $\endgroup$ – Noah Schweber Apr 22 '17 at 19:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.