Satisfiability and validity in first-order logic

There seems to be a subtle point about the concepts of satisfiability vs validity in first-order logic that I could use some clarification on.

These terms are usually defined as follows. A first order sentence is:

• Valid iff it is true in every model
• Satisfiable iff it is true in some model

But since FOL admits quantifiers, there seem to be some strange and counterintuitive quirks to this when free variables get involved. It seems to me that we have four possibilities. A formula with free variables can:

1. Hold for all objects in all models ("Valid?")
2. Hold for some objects in all models (??)
3. Hold for all objects in some models (??)
4. Hold for some objects in some models ("Satisfiable?")

In other words, we can consider the universal or existential closure of the formula, and then separately ask whether it holds in all or just some models.

What terminology do we use for these four cases?

• By definition, a sentence has no free variables. Sentences that hold in all models are called valid and sentences that hold in some models are called satisfiable (that covers your 1 and 4 for sentences). For formulas with free variables, I don't believe there is any standard terminology. Why do you ask? – Rob Arthan Sep 22 '17 at 20:18
• Thanks - changed to formula. I'm asking because the answer to this question confused me: math.stackexchange.com/questions/617263/… – Mike Battaglia Sep 22 '17 at 21:00
• The answer to that question is not very good: a sentence like $\forall x\forall y(x = y)$ is satisfiable but not "true" (or better "valid") because it holds in some models but not in all models. There is no general agreement about whether to take the universal closure or the existential closure in this connection (although the universal closure is the more common convention). But it doesn't make any difference if you start with a sentence - and then you have to address the possibility that a given sentence may be true in some models but not in others. – Rob Arthan Sep 22 '17 at 22:58
• @NoahSchweber: thanks for pointing out a very significant typo. – Rob Arthan Sep 22 '17 at 22:59
• Thanks, that's helpful, I guess it's just a matter of convention then. If you want to write this up as an answer I'll accept it. – Mike Battaglia Sep 22 '17 at 23:37

If we define the semantics for formulas with free variables, like in Enderton's textbook, we have that a formula $\varphi$ is satisfied in a structure $\mathfrak A$ with a variable assignment $s$, in symbols:
$\mathfrak A,s \vDash \varphi$.
Thus, the formula $x=0$ is satisfiable because the structure $\mathbb N$ with the assignment $s(x)=0$ will do.
A formula $\varphi$ is true in a structure $\mathfrak A$ if it is satisfied with every variable assignment.
A formula is valid iff for every structure $\mathfrak A$ and every assignment $s$, $\mathfrak A$ satisfy $\varphi$ with $s$.