# Two styles of semantics for a first-order language: what's to choose?

The usual classical semantics for FOL gets presented in two styles. Suppressing details irrelevant for the headline question, suppose the $L$-wff $\varphi(x)$ has only $x$ free, and let $I$ be a fixed interpretation of the non-logical vocabulary of $L$. Then one story comes to this:

$\exists x\varphi x$ is true on interpretation $I$ if, for some assignment $s$ of an object in the domain as value to $x$, $\varphi x$ is true on $I + s$.

The other story comes to this:

$\exists x\varphi x$ is true on interpretation $I$, if for some name $c$ in $L^+$ -- $L$ augmented with a name for every object in the domain -- $\varphi c$ is true on $I^+$ (the interpretation $I$ augmented with interpretations of all the new names).

We either keep $L$ fixed, and spin the objects assigned to variables; or we augment $L$ with a fixed name for every object. On the face of it there is little (nothing?) to choose. Different standard texts go in different ways. But are there subtle techie or conceptual reasons to prefer one line to the other?

[There was some relevant discussion among some philosophers over 35 years ago about Tarskian vs Fregean styles of semantics: but I'm interested here in the views of mathematicians (and computer scientists!).]

-
The second story is closer to actual mathematical practice: after all, how does one verify $\phi c$ if not by writing a proof of $\phi c$ in $L^+$? –  Zhen Lin Sep 1 '13 at 20:00
The first strikes me as being closer to the way that I actually think about such propositions in everyday mathematics. –  Brian M. Scott Sep 1 '13 at 20:02
@Andres: I’d probably do the same. It really does seem to me rather like learning to deal with equivalence relations and partitions as two ways of thinking about the same thing, or with topologies and nbhd systems. –  Brian M. Scott Sep 1 '13 at 20:38
@RobArthan Dirk van Dalen's very well-known classic text, Logic and Structure, comes immediately to mind. And I happened to just be looking at Shawn Hedman's A First Course in Logic which takes the same approach. –  Peter Smith Sep 2 '13 at 6:54
@DougSpoonwood: Obviously the question is phrased in the context of a formalization where $\exists$ rather than $\forall$ is the primitive quantifier. But the substance of it is pretty much the same for all variable binders. It is not a question of how to construct semantics for quantifiers as much as a question about how to handle the semantics of variables. Quantifiers just happen to be the kind of variable introducer that's relevant in FOL. –  Henning Makholm Sep 2 '13 at 8:30

Some random observations from (sorry, not what you asked for) a computer science perspective:

The dichotomoy is closely parallel to a choice one needs to make when defining semantics for programming languages. One can either carry around an environment which maps variable names to the values they are currently bound to, or implement variable bindings by substituting some syntactic representation of the values into the expression at the scope of the binding operator.

Both styles are found in the computer science literature, but the first one (with environment) seems to be the more popular one for several reasons. Or perhaps I'm biased; I much prefer environment-based semantics.

The main allure of the substitution-based semantics is that it seems technically simpler because it depends on machinery (for substitution etc) that one usually has to develop anyway in order to support syntactical reasoning about programs and program fragments. It's also closer to the classical conception of the lambda calculus as a purely syntactical rewrite system.

On the other hand it depends on having a syntactic representation for each possible value. This blurs the distinction between syntax and semantics (in your logic setting it feels inelegant to have to let even the language you work with vary according to the domain of the interpretation; that makes it strange if in the same breath you need to compare different interpretations of the same language). Moreover, in a programming-language context one often want to reason about properties that depend critically on the fact that some possible values cannot be written as closed terms, which directly conflicts with what one needs for a substitution-based semantics. That problem can be worked around with enough technical fiddlework, of course, but it doesn't really look nice.

The environment-based semantics doesn't have these problems, and provides a clear break between the syntax of formulae and their semantics.

The environment-based semantics also has the benefit of being strictly compositional in that the meaning of an expression depends only on the meaning of its parts rather than on their syntax -- the meaning here being a mapping from environments to (values, actions, truth values, whatever) that can be reified as a reasonably natural semantic object at the metalevel.

For someone who comes to formalism from a programming background, the environment-based semantics feels closer to what "really happens" with an expression that contains variables (see also Brian's comment). On the other hand, substitution seems to be how variables are usually explained in elementary mathematics education.

In each case, the fact that it can also be done the other way with equivalent results is of course a relevant and interesting property that deserves proof and discussion.

-