Teaching logic: Tarski vs Mates vs "logical constants"
I'm teaching an intermediate/advanced logic course this semester. So I had to ask myself how to introduce the semantics of quantifiers, with an eye on proving soundness and completeness. The standard approach, going back to Tarski, defines a satisfaction relation between a formula, a model, and an assignment function, and then defines truth by supervaluating over all assignments. The main alternative, often found in intro logic textbooks, is Mates' approach, where ∀xA(x) is defined as true in a model M iff A(c) is true in every c-variant of M, where c is a constant not occurring in A.
The Tarskian approach seems conceptually cleaner. It is nicely compositional, which Mates's approach is not. (In Mates's approach, the semantic value of ∀xA(x) is not determined by the semantic value of A(x).) On the flip side, Mates's approach cleverly conceals the complexity of interpreting quantifiers in the semantic clause for quantifiers: we don't need to keep track of assignments when interpreting negation or conjunction.
A somewhat analogous choice arises in the proof theory: when we argue from a universal premise ∀xA(x) to an "arbitrary" instance, should we use an individual constant or a variable? In Mates's approach to quantification, with its focus on truth (as opposed to satisfaction), it's natural to use a constant: A(x) is effectively understood as a predicate expression, and it's not clear what it means to reason from a universal statement to a predicate. In the Tarskian approach, both options are possible.
I went with Mates's approach. My main motivation was to avoid having to wrestle with fiddly issues about substitution. If we only substitute constants for variables, there's no need to mention the "free for" condition, and we don't need to establish tricky lemmas about substitution in the soundness and completeness proofs. (In (Bell and Machover 1977, 57–64), these lemmas take seven pages!)
Another reason for preferring Mates is that it seems overkill to have infinitary assignment functions in the semantics even though no sentence involves infinitely many variables. Intuitively, what we need to interpret Fx is information about the denotation of x: we don't need to know the denotations of all other variables in the language.
But there are also a few downsides to Mates's approach, apart from semantic non-compositionality. For example, soundness and completeness require a lemma about extensionality: if M assigns the same denotation to terms t1 and t2 then A(t1) and A(t2) have the same truth value in M. The proof is annoyingly fiddly; it takes about a page in my step-by-step presentation.
Another drawback is that Mates's approach requires having infinitely many constants in the language. This becomes awkward when we later want to discuss Peano Arithmetic or ZFC, whose signatures are supposed to include only one individual constant (PA), or even zero (ZFC). Relatedly, if we use constants for the Universal Instantiation rule, we can't simply say that in deductions from a premise set Γ, the rule mustn't introduce a constant occurring in Γ. For what if Γ already contains all constants? (I ran into this problem at the very first step of the Henkin completeness proof, where I wanted to show that if a set is consistent in the original language, then it is also consistent in an extended language.)
I'm now thinking that a cleaner approach would use neither variables nor ordinary constants, but a special class of "logical constants". Syntactically, these would behave like constants in that they can't be bound. But they would be classified as logical symbols. This means that they can be ignored when introducing the signature of a theory, and we can safely assume that they don't occur in a premise set Γ. The rule of Universal Instantiation would require replacing the bound variable by a logical constant. In the semantics, truth would be defined relative to "extended models". An extended model is simply a model, except that it may also interpret one or more logical constants. The interpretation of ∀xFx in a model M requires interpreting Fc in extended models Mc that extend M by interpreting the logical constant c. For ∀x∀yRxy, we need doubly extended models Mc,d, and so on.
I haven't worked out the details. I'm still going with Mates because I don't like using unorthodox approaches in my teaching. I vaguely remember having seen something like the approach I have sketched, but I wonder why it isn't more popular.