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:
- Hold for all objects in all models ("Valid?")
- Hold for some objects in all models (??)
- Hold for all objects in some models (??)
- 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?