On page 73 of Marker's Model Theory, An Introduction the following theorem can be found:

Theorem 3.1.4 Suppose that $L$ contains a constant symbol $c$, $T$ is an $L$-theory, and $\varphi ( \bar v)$ is an $L$-formula. The following are equivalent:

i) There is a quantifier-free $L$-formula $\psi ( \bar v )$ such that $T \models \forall \bar v \, ( \varphi (\bar v) \leftrightarrow \psi (\bar v) )$.

ii) If $M$ and $N$ are models of $T$, $A$ is an $L$-structure, $A \subseteq M$, and $A \subseteq N$, then $M \models \varphi (\bar a)$ if and only if $N \models \varphi (\bar a)$ for all $\bar a \in A$.

The proof of i) $\Rightarrow$ ii) is easy.

To show ii) $\Rightarrow$ i), Marker makes a case distinction. He first supposes $T \models \forall \bar v \, \varphi ( \bar v )$: then $T \models \forall \bar v \, ( \varphi (v) \leftrightarrow c = c )$, so we're done. Similarly if $T \models \forall \bar v \, \neg \varphi ( \bar v )$, then we're done because $T \models \forall \bar v \, ( \varphi (v) \leftrightarrow c \neq c )$.

After that, he states: Thus, we may assume that both $T ∪ \{\varphi (\bar v)\}$ and $T ∪ \{\neg \varphi (\bar v)\}$ are satisfiable. Of course, I agree with this statement - this is not an issue.

My problem lies in the fact that in the subsequent proof that Marker gives it is not at all clear to me where this assumption is used. (Note that at no spot he explicitly mentions the usage of this assumption.)

So my concrete question is: where is this assumption used in Marker's proof?

I think it should be used somewhere, otherwise it seems that the assumption the language have at least one constant can be omitted from the statement.

(NB: Alas, the complete proof is a little lengthy to post here.)


See proof page 74; Marker wants to prove the Claim :

$T \cup \Gamma(\overline d) \vDash \phi(\overline d)$.

He proceeds by contradiction, assuming : $\mathcal M \vDash T \cup \Gamma(\overline d) \cup \{ \lnot \phi(\overline d) \}$.

This, I think, is the point ... If one of $T \cup \{ \phi(\overline v) \}$ or $T \cup \{ \lnot \phi(\overline v) \}$ were unsatisfiable, "adding" to $T$ the new premises $\Gamma$ will not change this situation.

  • $\begingroup$ Thanks for your answer. Still, I do not understand where it's used. As you justly state, he supposes $M$ is a model of this theory. In order this be possible, it has to be the case that $M \cup \{ \neg \varphi ( \bar d ) \}$ is satisfiable, right? (Otherwise there cannot even be such a structure $M$.) That is, it is certainly a necessary assumption. The weird thing is that, when I go through the proof, I still do not see in which step (inference) it is used. $\endgroup$ – Boda Poldi Mar 4 '15 at 9:29
  • $\begingroup$ @BodaPoldi - I think that the "step" is exactly that : if $T \cup \{ ¬ \phi(v) \}$ is not satisfiable, then also $T \cup \Gamma(d) \cup \{ ¬ \phi(d) \}$ is not, and thus he cannot assume the existence of $\mathcal M$. $\endgroup$ – Mauro ALLEGRANZA Mar 4 '15 at 10:32
  • $\begingroup$ Thank you. I also thought about that. However, we get this structure $M$ (because of the assumption) by contradiction, right? So we don't use anything there: if it doesn't exist, then what we wanted to show (namely $T \cup \Gamma ( \bar d ) \models \varphi ( \bar d )$) is trivial. Isn't it? $\endgroup$ – Boda Poldi Mar 4 '15 at 16:26

Marker is rather messy on this point. It is a minor point (that is why nobody cares) but it may confuse students.

When Marker defines formulas he forgets a connective: the 0-ary Boolean connective $\top$ (or $\bot$, if you prefer). The role of this connective is merely formal: it allows you to write a quantifier-free sentence also in languages without constants.

You need to have it otherwise relational theories (e.g. dense linear orders, random graphs) would never have elimination of quantifiers for a trivial reason: there is no quantifier-free sentence equivalent to $\forall x\ (x=x)$.

  • $\begingroup$ Thanks for your answer. I understand (and in fact already understood) this point about quantifier elimination and languages without constant symbol. It does not, however, seem to answer my question: where in the proof does Marker use the assumption (the one which I stated in my question)? $\endgroup$ – Boda Poldi Mar 4 '15 at 9:27
  • $\begingroup$ At some point he defines $A$ to be the structure generated by $\bar d$. If $\bar d$ is the empty tuple and the language has no constants, then $A=\varnothing$. Marker does not allow empty structures! (A choice that makes degenerated cases not seamless.) $\endgroup$ – Primo Petri Mar 4 '15 at 10:01
  • $\begingroup$ This is a very good point. I agree with you that if $\bar d$ is the empty tuple (corresponding to the fact that $\varphi$ is a sentence), and the language doesn't have any constant symbols, then $A$ would be the "empty" structure (so it wouldn't exist). Still, where does Marker use the hypotheses that $T ∪ \{\varphi (\bar v)\}$ and $T ∪ \{\neg \varphi (\bar v)\}$ are satisfiable? $\endgroup$ – Boda Poldi Mar 4 '15 at 16:32

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.