Established conventions for distinguishing the consequence relations of FOL

Solution 1:

In my experience, the most common convention in first-order logic is that the consequence relation $\models$ is something that only applies to theories and sentences. That is, it just doesn't make sense to write $\Gamma\models \varphi$ when $\Gamma$ and $\varphi$ have free variables. And in the absence of free variables, there is no difference between your "local" and "global" consequence relations.

But I agree that sometimes it is useful to talk about the consequence relation between (sets of) formulas with free variables. For example, when proving soundness for certain proof systems (e.g. in a sequent calculus $\varphi\vdash \psi$ makes sense when $\varphi$ and $\psi$ have free variables, and we want it to imply $\varphi\models \psi$). Or in model theory, when thinking about notions like isolated types, it can be more convenient to write $T\cup \varphi(x)\models p(x)$ instead of $T\models \forall x\,(\varphi(x)\rightarrow \psi(x))$ for all $\psi(x)\in p(x)$.

In these situations, as you might already guess from the examples I used, I think there's only one reasonable meaning of $\models$: what you call the "local relation". I don't think I've ever encountered the "global relation".

More precisely, I would say that first-order logic has infinitely many consequence relations, one denoted $\models_x$ for each variable context $x = (x_1,\dots,x_n)$. For the expression $\varphi\models_{x} \psi$ to be well-formed, the free variables in $\varphi$ and $\psi$ must all come from the context $x$. And $\varphi\models_{x} \psi$ means that for all structures $M$ and all tuples $a = (a_1,\dots,a_n)\in M^x$, if $M\models \varphi(a)$, then $M\models \psi(a)$. Note that this is equivalent to saying that for all structures $M$, the definable set $\varphi(M) = \{a\in M^x\mid M\models \varphi(a)\}$ is a subset of $\psi(M) = \{a\in M^x\mid M\models \psi(a)\}$. The notation can be extended naturally to sets of formulas, so $p(x)\models q(x)$ expresses a containment of type-definable sets across all models.

Most of the time, people will suppress the variable context subscript, just writing $\varphi(x) \models \psi(x)$, and think of this as a single consequence relation. This is safe to do in the classical semantics with no empty structures. But if you allow empty structures or multi-sorted structures with empty sorts, then it's an important technicality to notice that the consequence relations in distinct variable contexts are distinct. For example, writing $()$ for the empty variable context, we have $\forall x\, \bot\not\models_{()} \exists x\,\top$, since an empty structure validates $\forall x\, \bot$ but not $\exists x\, \top$. But on the other hand, $\forall x\, \bot\models_y \exists x\, \top$, vacuously, since $\forall x\,\bot$ is only true in an empty structure, and an empty structure admits no interepretations of the variable $y$.