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

Solution 1:

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.

Solution 2:

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.