Understanding interpretation of quantified set variables in Herbert Enderton "Second-order and Higher-order logic"

Question

In Stanford Encyclopedia, concerning the semantics of second order logic, Herbert B. Enderton wrote

... an assignment $s$ of objects to the free variables in $\phi$. ... For a $k$-place predicate variable $P$,

$M \models \forall P\; \phi[s]\;$ iff$\;$ for every $k$-ary relation $Q$ on $A$, we have $M \models \phi[s']$

where $s'$ differs from $s$ only in assigning the relation $Q$ to the predicate variable $P$.

I think I understand informally what this means, but I am stuck when I try to understand how it works formally. Does the original assignment $s$ also assigns a value to the predicate variable $P$? Naively, I would say no, because otherwise $\forall P$ is uninteresting (or else I misunderstand how assignments work), but the context seems to say the opposite.

Also, why do we need a second use of $\models$. Couldn't we say

$$M \models \forall P\; \phi[s]\; \iff \forall Q\; \phi^M[s]$$

where $\phi^M$ is the result of substituting the symbols in $\phi$ by their interpretation fixed in $M$, $P$ by $Q$, and the range of $Q$ is also fixed in $M$ (the possible ranges depend on the semantic) and $s$ assigns a value to all free variables in $\phi$, except $Q$, which is taken care by $\forall Q$.

I use the assumption that the formal language is very close to the language that is used to define the models, both have quantifiers, etc. So, I am trying to leverage on this. May be it is too naive. What am I missing?

I am trying to understand how the formalism works. Also, again, why we need a second use of $\models$. If it was third order logic, would we need to use it three times? These two questions are most likely related. As usual, I must be missing some thing basic.

Answer 1

The trouble you're having is not really specific to second-order logic; you would run into exactly the same design issues when defining the semantics of quantifiers in ordinary first-order logic. If you already know some first-order logic, I think your problem is simply that the author of the article uses a different style than you're used to from the text you learned first-order logic from, but that difference would also exist for the plain first-order case.

Your basic problem, I think, is that you have not understood how the brackets and the $\vDash$ sign interact. Perhaps the spacing makes it unclear -- but the point here is that the author is explaining the semantics by defining a single three-place relation symbol $$ {\rm something}_1 \vDash {\rm something}_2 \;[{\rm something}_3] $$ You can't in this context have a $\vDash$ without the $[\;]$, or $[\;]$ without the $\vDash$. (Well, actually these things probably have defined meanings by themselves, but that will be a different definition than the one you're looking at here).

In this three-place symbol,

• ${\rm something}_1$ is a structure, that is, an appropriate arranged collection of semantic objects
• ${\rm something}_2$ is always a well-formed formula consisting entirely of symbols, and with no trace of anything from $M$ appearing within it.
• ${\rm something}_3$ is a mapping from symbolic names to semantic objects that those names are imagined to stand for.

It differs between developments whether the map ${\rm something}_3$ is always assumed to map every variable symbol (of every sort) to an appropriate semantic object, or if it can be partial as long as it does define a meaning for everything that appears free in ${\rm something}_2$. Your quote would work under both of these conventions. Both give the same result in the case where ${\rm something}_2$ is a sentence, but there are minor technical advantages and disadvantages of each choice when it may have free variables in it. (It's like straightening out the kink in a carpet that's just a few centimeters too wide for the room: the slack has to go somewhere). When the work is done properly, the end result ends up being equivalent in either case.

The definition of the $\vDash\;[\;]$ relation is now by recursion in the structure of the formula ${\rm something}_2$. Thus, the definition of $\cdots\vDash\;\forall P.\varphi \;[\cdots]$ will naturally depend on an application of $\vDash\;[\;]$ to its subformula $\varphi$.

---

Your proposal

$$M \models \forall P\; \phi[s]\; \iff \forall Q\; \phi^M[s]$$

seems to depend on building a $\phi^M$ which is something that contains a mixture of symbols and semantic objects. This can be made to work if you insist enough, but it is often considered inelegant and error-prone to mix syntax and semantics in that way.

Even worse, it seems like you're depending on $\forall Q$ to do its work on the metalevel, so if your proposal is to work we need to say that the quantifier in $\forall Q$ is not just a symbol.

In fact it looks like getting your proposal to work would require doing all of the interesting semantic work inside a definition of what $\varphi^M[s]$ actually means, in detail. And then $\vDash$ would just be a renaming of the thing that definition defines. All you would have achieved is to do the same work with different notation.