Are there any established conventions for distinguishing the consequence relations of first-order logic? I'm thinking both in terms of what to call them (e.g. global vs local) and what notation to use.

What follows is background and motivation for the question and some links to answers on this site or external resources.

For example, is it at least somewhat conventional to use $\Gamma \models \varphi$ for the local consequence relation and $\Gamma \Rightarrow \varphi$ or $\varphi \mathop{=\!\!\!|} \Gamma$ or $\Gamma \models^g \varphi$ or something for the global one? For example, this answer by sequitur to a similar question I had about modal logic uses $\models^g$.

As for my motivation, I'm trying to (re)-learn first-order logic thoroughly so I can a) prove stuff about various proof calculi and b) understand my model theory textbooks better.

Also, is having a logic with multiple consequence relations so awkward/weird that it's better to talk about two distinct first-order logics rather than one with multiple consequence relations. For example, this answer (among others that I've seen before but can't find) defines a logic as a set of sentences and exactly one consequence relation. I know there's another answer out there that defines what a logic is in general more explicitly. I'll update the link when I find it.

Also, it is possible to define stranger consequence relations for FOL that permit, for example, adding new free variables (via $\forall x \mathop. \varphi \models \varphi(x)$) but not removing them or permit removing free variables but not adding them. I'm assuming that these consequence relations (and possibly others?) are not really worth talking about. Is this assumption correct?

This question, which cites this email, discusses which consequence relation for first-order logic is better to teach students. I'll call them $\models^g$ for the global consequence relation that ranges over variable assignments and $\models^l$ for the local one that doesn't.

First, let $M \models \varphi$ hold if and only if $M, v \models \varphi$ for all $M$-valuations on the free variables of $\varphi$ $v$.

Let $M, v \models \varphi$, where $v$ is a valuation that is constrained to only assign interpretations to the free variables of $\varphi$.

I'm being pedantic about the free variables of the valuation so that $\lnot (x = x)$ is a tautology when the structure is empty, but $\lnot \forall x \mathop. x = x$ and $\lnot \forall x \mathop. x \neq x$ are both non-tautologies because they don't have any free variables. Previously, I liked to define $v$ to assign an interpretation to every possible variable symbol, but this has the unfortunate consequence of making everything a tautology in empty structures (and I think it also makes $\forall$-elimination work in a weird symmetry-breaking way).

The local relation is defined as follows.

$ \Gamma \models \varphi$ if and only if for all models $M$ and $M$-valuations on $\text{FV}(\varphi)$ $v$, if $M, v \models \Gamma$ then $M, v \models \varphi$.

The global relation is defined as follows.

$ \Gamma \models \varphi$ if and only if for all models $M$, if $M \models \Gamma$ then $M \models \varphi$.


1 Answer 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$.

  • $\begingroup$ This question says that the global relation appears in Mendelson et al. I'm not sure how popular that book is or if it's the most popular one that uses the global relation. I like the family of relations per variable context $\models_{\vec{x}}$. Is it capable of assessing the truth of $\varphi \models_{\vec{x}} \psi$ when $\text{FV}(\varphi)$ and $\text{FV}(\psi)$ are not equal to $\vec{x}$? Do you know if there's a book or similar that uses the $\models_\vec{x}$ approach? Thank you. $\endgroup$ Jan 3, 2022 at 4:21
  • $\begingroup$ There's a lot of stuff in Mendelson that I disagree with. But I just had a look in my copy (6th edition), and it seems to me that he uses the local relation. On p. 62, he writes "$C$ is said to be a logical consequence of a set of wfs $\Gamma$ if and only if, in every interpretation, every sequence that satisfies every wf in $\Gamma$ also satisfies $C$". That's the local relation, right? @GregoryNisbet $\endgroup$ Jan 3, 2022 at 4:34
  • 1
    $\begingroup$ When you say $\mathrm{FV}(\varphi)$ is not equal to $\vec{x}$, do you just mean that not every variable in $\vec{x}$ appears in $\varphi$? If so, then yes: you can always view a formula as a formula in any larger variable context. $\endgroup$ Jan 3, 2022 at 4:39
  • 1
    $\begingroup$ @GregoryNisbet I think "interpretation" refers to $M$ and "sequence" refers to $v$. $\endgroup$ Jan 3, 2022 at 4:44
  • 1
    $\begingroup$ @GregoryNisbet For more on what's going on in Mendelson: math.stackexchange.com/q/576172/7062. Unfortunately I don't have a reference for you to a book that uses the $\models_x$ approach. I'm not aware of any introductory logic books that (in my view) get all their conventions right. Maybe I'll write one someday... $\endgroup$ Jan 3, 2022 at 4:57

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .