elementary question about definability

Question

My understanding is that an object, m, from the domain of a model, M, is definable by a formula, F(x), just in case M |= (Vx)[F(x) <----> x = m]. However, this assumes that there is a name for the object defined in the language in question, which seems to undercut the point of defining m. If we do not suppose this, then how do we characterize the definability of m in M? Could we just say that M |= F(x) under the assignment of x to m, and ~(M |= F(x)) under any other assignment?

Answer 1

Free variables in a formula $φ$ can be interpreted as elements of the model. Some texts are very precise and write "$M[x=a] \vDash φ$" to mean that $M$ satisfies $φ$ with $x$ interpreted as $a$, where $a$ is an element in the model. Some others might write something like "$M \vDash φ[a/x]$", which is similar to the term substitution notation, but now used to denote interpretation instead. This can be a bit cumbersome so sometimes people just say that $φ$ has $1$ parameter and write "$M \vDash φ(a)$" instead. Similarly, we often write "$\mathbb{N} \vDash 0 < 2$" to mean "$\mathbb{N}[x=2] \vDash 0 < x$", if over a language that does not have the symbol for $2$.

In your case:

Given any model $M$ over a language $L$, an element $a$ in $M$ is said to be first-order definable over $L$ iff there is a $1$-parameter first-order formula $φ$ such that $( M \vDash φ(b) ) \Leftrightarrow ( a = b )$ for any element $b$ in $M$.

This turns out to be equivalent to:

Given any model $M$ over a language $L$, an element $a$ in $M$ is said to be first-order definable over $L$ iff there is a $1$-parameter first-order formula $φ$ such that $M \vDash \forall x\ ( φ(x) \leftrightarrow x=a )$.

But remember that in both variations, what is on the right of "$M \vDash$" is not strictly speaking the formula itself. In the first variation "$φ(b)$" is semantically evaluated, and in the second case the entire "$\forall x\ ( φ(x) \leftrightarrow x=a )$ is semantic because "$a$" is not in the language.

Answer 2

No, the $\leftrightarrow$ is not in the formula. $m$ is definable in $M$ if for some formula $\varphi(x)$, for all $n$ in $M$, $M\models\varphi(n) \iff n=m$.

The quantification is external.