Definition of witness property in Marker's "Model theory - An introduction"

Question

In David Marker's "Model theory - An introduction" he defines the witness property in the context of Henkin constructions as:

In the Erratum he says that in this definition, it should have been $(\exists \phi(v)\to \phi(c))\in T$ instead of $T\models (\exists \phi(v)\to\phi(c))$.

However, I've googled "Witness property" online and found the definition in various texts as: $\ $

or for example:

So is Marker's correction wrong and the original definition correct?

Answer 1

A structure $M$ can have the witness property by having enough constants to witness the truth of satisfiable well-formed formulas, in which case it would be correct to say that: for all $\varphi$, $M \models [\exists v](\varphi(v)) \to \varphi(c)$.

I would argue that for a theory the notation $\models$ isn't totally wrong, since $\Gamma \models \varphi$ can be used to denote semantic consequence.

Anyway, a theory is a set of sentences, so the erratum $[\exists v](\varphi(v)) \to \varphi(c) \in T$ denotes that the well-formed formula is in $T$ directly $T$ and $T \vdash [\exists v](\varphi(v)) \to \varphi(c)$ denotes that $[\exists v](\varphi(v)) \to \varphi(c)$ is a syntactic consequence of $T$.

In any of these notations, $[\exists v](\varphi(v)) \to \varphi(c)$ is in the deductive closure of $T$, perhaps trivially, which is what we're after.

Answer 2

The problem is that we don't know that the relation $T\models\varphi$ works anywhere close to the way we'd like it to till after the compactness theorem is proven. If $T$ has no models, then we have $T\models \exists x\varphi(x)\to \varphi(c)$ always, regardless if the sentence is included in $T.$ And more generally, we have $T\models \varphi$ for every sentence, whereas at most one of $\varphi$ and $\lnot \varphi$ is contained in $T$ when $T$ is finitely satisfiable.

Contrast the case of the analogous proof of the completeness theorem, where we know at that outset that a maximal (deductively) consistent theory $T$ has $\varphi \in T$ if and only if $T\vdash \varphi,$ and so the distinction is moot for the purposes of proving the completeness theorem.

If $T\models \varphi$ were instead initially defined to mean that there is a finite subset of $T$ such that every model of that subset satisfies $\varphi$, then we could use $\varphi\in T$ and $T\models \varphi$ interchangibly when $T$ is a maximal finitely satisfiable theory. This "more manifestly $\vdash$-like" definition can be useful in adapting things from the syntax side to the semantic side without having to go through the completeness theorem, e.g. if you want to define a semantic version of the Lindenbaum algebra and prove compactness from the ultrafilter lemma.

(Thanks to Michael Weiss for pointing out my original answer completely missed the point.)