1
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Correct : "an assignment $s$ of objects to the free variables in $φ$", as for FOL. The only difference is that, in SOL, we may have also predicate variables and function variables. $\endgroup$ May 30, 2018 at 18:15
  • $\begingroup$ See Enderton, page 283 : "We must extend the definition of satisfaction in the natural way. Let $V$ now be the set of all variables, individual, predicate, or function. Let $s$ be a function on $V$ that assigns to each variable the suitable type of object. Thus $s(v_1)$ is a member of the universe, $s(X^n)$ is an $n$-ary relation on the universe, and $s(F^n)$ is an $n$-ary operation." $\endgroup$ May 30, 2018 at 18:18
  • $\begingroup$ Yes, I read the answer of Makholm and I realize that the formula to which s applies is $\forall P\, \phi$. This is what I missed, as far as what $s$ means is concerned. $\endgroup$
    – Dominic108
    May 30, 2018 at 20:02

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ @Dominic108: After you do your substitution, does your substituted $\phi$ not contain symbols such as "$\to$" or "$\neg$"? $\endgroup$ May 30, 2018 at 20:20
  • $\begingroup$ After some extra thoughts, I realize that it's just a question of notation. What I had in mind, was basically the same as in the Enderton definition. I wrote $\forall Q$ and Enderton wrote "for every $k$-ary relation $Q$ on $A$". Next, I wrote $\phi^M[s]$, where $P$ is replaced by $Q$, but this is equivalent to $M \models \phi[s']$ where $s'$ ... . So, what I wrote was also recursive. I just did not realize it. $\endgroup$
    – Dominic108
    May 31, 2018 at 0:29
  • $\begingroup$ And thankyou for your answer. It helped me to see that a recursive definition was a very natural thing, because the language is defined recursively and, in fact, my approach was not different. $\endgroup$
    – Dominic108
    May 31, 2018 at 0:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.