# 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.

-

The approach that proceeds via an extended language is sometimes more elegant. With the other "variable interpretation function" approach, it is no longer true that a formula is true or false in a structure; instead one has to speak of truth in a structure relative to a variable interpretation. One has to prove as a separate theorem that two variable interpretations that agree on the free variables of a formula will give it the same truth value, and thus the truth of a sentence in a structure is independent of the variable interpretation. However, to check the truth of a sentence, we must still begin with some arbitrary variable interpretation. That separate theorem, the need to choose an arbitrary assignment that will not affect anything, and the notational complications of variable interpretation functions are entirely eliminated with the augmented-language approach.

Also, the definition by variable interpretation functions fails for empty structures (i.e. empty domain of discourse), which do not have any variable interpretation functions. In light of the theorem mentioned before, we might define a sentence to be true in a structure when it is satisfied by every variable interpretation - but then every sentence is true in the empty model. If we say that a sentence is true when it is satisfied by some variable interpretation, then no sentence is true. Either way, the semantics via variable interpretation functions breaks down in empty structures. By contrast, the augmented-language version treats the quantifiers more disquotationally and has no problem with empty structures.

The main downside of the augmented-language version is that it abuses the naive meaning of "language". When a structure is uncountable, its augmented language is also uncountable. That doesn't cause any mathematical problems if we treat the language abstractly, but if we think that a key aspect of a formal language is that we can write down each sentence with a finite number of symbols from a finite alphabet, then uncountable languages are no good.

-
The empty structure does have a possible variable interpretation function, namely the one whose domain is empty. So a sentence with no free variables can still be either true or false, according to how it evaluates under the empty variable assignment. – Henning Makholm Sep 2 '13 at 11:46
@Henning: by definition, in the convention Enderton and others follow, the domain of each variable interpretation function is the infinite set of all the logical variables. – Carl Mummert Sep 2 '13 at 18:42
x @Carl: I tend to view that as a quick-and-dirty approximation to the finite variable assignments that I think of as "what is really going on". The use of infinite variable assignments is to me an approximation that avoids a bit of technical footwork at the cost of not working for empty structures. – Henning Makholm Sep 3 '13 at 10:05
It does have the advantage that every formula is true or false relative to a fixed structure and variable assignment function, which I see as the underlying point and main benefit of using assignment functions, because the expanded language method will only give truth values for sentences. If one is only going to define truth for sentences anyway, then the use of assignment functions compared to an expanded language is more of a bookkeeping device to track the variable substitutions than a real change in the definitions. – Carl Mummert Sep 3 '13 at 10:20