Syntax and Semantics

Editorial

Basic syntax and semantics for SOL covered so far. As a chapter it's too short. Substitution for second-order variables has to be covered to be able to talk about derivation systems for SOL, and there's some subtle issues there.

Explain

The non-logical symbols of a second-order language are specified the same way a first-order language is: by listing its constant symbols, function symbols, and predicate symbols.

In first-order logic, the identity predicate $\eq$source is usually included. In first-order logic, the non-logical symbols of a language $\Lang{L}$source are crucial to allow us to express anything interesting. There are of course sentences that use no non-logical symbols, but with only $\eq$source it is hard to say anything interesting. In second-order logic, since we have an unlimited supply of relation and function variables, we can say anything we can say in a first-order language even without a special supply of non-logical symbols.

Definition of second order terms

[Second-order Terms] The set of second-order terms of $\Lang L$source, $\TrmSOL[L]$source, is defined by adding to the definition of first order terms the clause

1. If $u$source is an $n$source-place function variable and $t_1$source, dots, $t_n$source are terms, then $\Atom{u}{t_1, \ldots, t_n}$source is a term.

Explain

So, a second-order term looks just like a first-order term, except that where a first-order term contains a function symbol $\Obj{f^n_i}$source, a second-order term may contain a function variable $\Obj{u^n_i}$source in its place.

Definition of second order formulas

[Second-order formula] The set of second-order formulas $\FrmSOL[L]$source of the language $\Lang L$source is defined by adding to the definition of first order formulas the clauses

1. If $X$source is an $n$source-place predicate variable and $t_1$source, dots, $t_n$source are second-order terms of $\Lang L$source, then $\Atom{X}{t_1,\ldots, t_n}$source is an atomic formula.

   tagitemprvAllIf $!A$source is a formula and $u$source is a function variable, then $\lforall[u][!A]$source is a formula.

   tagitemprvAllIf $!A$source is a formula and $X$source is a predicate variable, then $\lforall[X][!A]$source is a formula.

   tagitemprvExIf $!A$source is a formula and $u$source is a function variable, then $\lexists[u][!A]$source is a formula.

   tagitemprvExIf $!A$source is a formula and $X$source is a predicate variable, then $\lexists[X][!A]$source is a formula.

Explain

To define the satisfaction relation $\Sat{M}{!A}[s]$source for second-order formulas, we have to extend the definitions to cover second-order variables. The notion of a structure is the same for second-order logic as it is for first-order logic. There is only a difference for variable assignments $s$source: these now must not just provide values for the first-order variables, but also for the second-order variables.

Second order variable assignments

[Variable Assignment] A variable assignment $s$source for a structure $\Struct{M}$source is a function which maps each

1. object variable $\Obj{v_i}$source to an element of $\Domain M$source, i.e., $s(\Obj{v_i}) \in \Domain{M}$source

2. $n$source-place relation variable $\Obj{V_i^n}$source to an $n$source-place relation on $\Domain{M}$source, i.e., $s(\Obj{V_i^n}) \subseteq \Domain{M}^n$source;

3. $n$source-place function variable $\Obj{u_i^n}$source to an $n$source-place function from $\Domain{M}$source to $\Domain{M}$source, i.e., $s(\Obj{u_i^n})\colon \Domain{M}^n \to \Domain{M}$source;

Explain

A structure assigns a value to each constant symbol and function symbol, and a second-order variable assignment assigns objects and functions to each object and function variable. Together, they let us assign a value to every term.

Value of a function variable application

[value of a Term] If $t$source is a term of the language $\Lang L$source, $\Struct M$source is a structure for $\Lang L$source, and $s$source is a variable assignment for $\Struct M$source, the value $\Value{t}{M}[s]$source is defined as for first-order terms, plus the following clause:

Variants of variable assignments

[$x$source-Variant] If $s$source is a variable assignment for a structure $\Struct M$source, then any variable assignment $s'$source for $\Struct M$source which differs from $s$source at most in what it assigns to $x$source is called an $x$source-variant of $s$source. If $s'$source is an $x$source-variant of $s$source we write $\varAssign{s'}{s}{x}$source. (Similarly for second-order variables $X$source or $u$source.)

Changing the value of one variable in an assignment

If $s$source is a variable assignment for a structure $\Struct M$source and $m \in \Domain{M}$source, then the assignment $\Subst{s}{m}{x}$source is the variable assignment defined by

If $X$source is an $n$source-place relation variable and $M \subseteq \Domain{M}^n$source, then $\Subst{s}{M}{X}$source is the variable assignment defined by

If $u$source is an $n$source-place function variable and $f\colon \Domain{M}^n \to \Domain{M}$source, then $\Subst{s}{f}{u}$source is the variable assignment defined by

In each case, $y$source may be any first- or second-order variable.

Satisfaction clauses for second order logic

[Satisfaction] For second-order formulas $!A$source, the definition of satisfaction is like the definition of first order satisfaction with the addition of:

1. Case: $!A \ident \Atom{X^n}{t_1, \dots, t_n}$source

   $\Sat{M}{\indfrm}[s]$source iff $\langle \Value{t_1}{M}[s], \dots, \Value{t_n}{M}[s] \rangle \in s(X^n)$source. tagitemprvAll

   Case: $!A \ident \lforall[X][!B]$source

   $\Sat{M}{\indfrm}[s]$source iff for every $M \subseteq \Domain{M}^n$source, $\Sat{M}{!B}[\Subst{s}{M}{X}]$source.

   tagitemprvEx

   Case: $!A \ident \lexists[X][!B]$source

   $\Sat{M}{\indfrm}[s]$source iff for at least one $M \subseteq \Domain{M}^n$source so that $\Sat{M}{!B}[\Subst{s}{M}{X}]$source.

   tagitemprvAll

   Case: $!A \ident \lforall[u][!B]$source

   $\Sat{M}{\indfrm}[s]$source iff for every $f\colon \Domain{M}^n \to \Domain{M}$source, $\Sat{M}{!B}[\Subst{s}{f}{u}]$source.

   tagitemprvEx

   Case: $!A \ident \lexists[u][!B]$source

   $\Sat{M}{\indfrm}[s]$source iff for at least one $f\colon \Domain{M}^n \to \Domain{M}$source so that $\Sat{M}{!B}[\Subst{s}{f}{u}]$source.

Example of complementary unary relations

Consider the formula $\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]$source. It contains no second-order quantifiers, but does contain the second-order variables $X$source and $Y$source (here understood to be one-place). The corresponding first-order sentence $\lforall[z][(\Atom{P}{z} \liff \lnot \Atom{R}{z})]$source says that whatever falls under the interpretation of $P$source does not fall under the interpretation of $R$source and vice versa. In a structure, the interpretation of a predicate symbol $P$source is given by the interpretation $\Assign{P}{M}$source. But for second-order variables like $X$source and $Y$source, the interpretation is provided, not by the structure itself, but by a variable assignment. Since the second-order formula is not a sentence (it includes free variables $X$source and $Y$source), it is only satisfied relative to a structure $\Struct{M}$source together with a variable assignment $s$source.

$\Sat{M}{\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]}[s]$source whenever the elements of $s(X)$source are not elements of $s(Y)$source, and vice versa, i.e., iff $s(Y) = \Domain{M} \setminus s(X)$source. For instance, take $\Domain{M} = \{1, 2, 3\}$source. Since no predicate symbols, function symbols, or constant symbols are involved, the domain of $\Struct{M}$source is all that is relevant. Now for $s_1(X) = \{1, 2\}$source and $s_1(Y) = \{3\}$source, we have $\Sat{M}{\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]}[s_1]$source.

By contrast, if we have $s_2(X) = \{1, 2\}$source and $s_2(Y) = \{2, 3\}$source, $\Sat/{M}{\lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})]}[s_2]$source. That's because $\Sat{M}{\Atom{X}{z}}[\Subst{s_2}{2}{z}]$source (since $2 \in \Subst{s_2}{2}{z}(X)$source) but $\Sat/{M}{\lnot \Atom{Y}{z}}[\Subst{s_2}{2}{z}]$source (since also $2 \in \Subst{s_2}{2}{z}(Y)$source).

Existence of a nonempty complement

$\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]$source if there is an $N \subseteq \Domain{M}$source such that $\Sat{M}{(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])}[\Subst{s}{N}{Y}]$source. And that is the case for any $N \neq \emptyset$source (so that $\Sat{M}{\lexists[y][\Atom{Y}{y}]}[\Subst{s}{N}{Y}]$source) and, as in the previous example, $N = \Domain{M} \setminus s(X)$source. In other words, $\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]$source iff $\Domain{M} \setminus s(X)$source is non-empty, i.e., $s(X) \neq \Domain{M}$source. So, the formula is satisfied, e.g., if $\Domain{M} = \{1, 2, 3\}$source and $s(X) = \{1, 2\}$source, but not if $s(X) = \{1, 2, 3\} = \Domain{M}$source.

Since the formula is not satisfied whenever $s(X) = \Domain{M}$source, the sentence

is never satisfied: For any structure $\Struct{M}$source, the assignment $s(X) = \Domain{M}$source will make the sentence false. On the other hand, the sentence

is satisfied relative to any assignment $s$source, since we can always find $M \subseteq \Domain{M}$source but $M \neq \Domain{M}$source (e.g., $M = \emptyset$source).

Defining negation with a universally false second order sentence

The second-order sentence $\lforall[X][\lforall[y][X(y)]]$source says that every $1$source-place relation, i.e., every property, holds of every object. That is clearly never true, since in every $\Struct{M}$source, for a variable assignment $s$source with $s(X) = \emptyset$source, and $s(y) = a \in \Domain{M}$source we have $\Sat/{M}{X(y)}[s]$source. This means that $!A \lif \lforall[X][\lforall[y][X(y)]]$source is equivalent in second-order logic to $\lnot !A$source, that is: $\Sat{M}{!A \lif \lforall[X][\lforall[y][X(y)]]}$source iff $\Sat{M}{\lnot !A}$source. In other words, in second-order logic we can define $\lnot$source using $\lforall$source and $\lif$source.

Exercise defining conjunction and disjunction

Show that in second-order logic $\lforall$source and $\lif$source can define the other connectives:

1. Prove that in second-order logic $!A \land !B$source is equivalent to $\lforall[X][(!A \lif (!B \lif \lforall[x][X(x)])\lif \lforall[x][X(x)])]$source.

2. Find a second-order formula using only $\lforall$source and $\lif$source equivalent to $!A \lor !B$source.

Explain

The central logical notions of validity, entailment, and satisfiability are defined the same way for second-order logic as they are for first-order logic, except that the underlying satisfaction relation is now that for second-order formulas. A second-order sentence, of course, is a formula in which all variables, including predicate and function variables, are bound.

Second order validity

[Validity] A sentence $!A$source is valid, $\Entails !A$source, iff $\Sat{M}{!A}$source for every structure $\Struct M$source.

Second order entailment

[Entailment] A set of sentences $\Gamma$source entails a sentence $!A$source, $\Gamma \Entails !A$source, iff for every structure $\Struct M$source with $\Sat{M}{\Gamma}$source, $\Sat{M}{!A}$source.

Second order satisfiability

[Satisfiability] A set of sentences $\Gamma$source is satisfiable if $\Sat{M}{\Gamma}$source for some structure $\Struct M$source. If $\Gamma$source is not satisfiable it is called unsatisfiable.

Explain

Quantification over second-order variables is responsible for an immense increase in the expressive power of the language over that of first-order logic. Second-order existential quantification lets us say that functions or relations with certain properties exist. In first-order logic, the only way to do that is to specify a non-logical symbol (i.e., a function symbol or predicate symbol) for this purpose. Second-order universal quantification lets us say that all subsets of, relations on, or functions from the domain to the domain have a property. In first-order logic, we can only say that the subsets, relations, or functions assigned to one of the non-logical symbols of the language have a property. And when we say that subsets, relations, functions exist that have a property, or that all of them have it, we can use second-order quantification in specifying this property as well. This lets us define relations not definable in first-order logic, and express properties of the domain not expressible in first-order logic.

Definability of a binary relation

If $\Struct{M}$source is a structure for a language $\Lang{L}$source, a relation $R \subseteq \Domain{M}^2$source is definable in $\Lang{L}$source if there is some formula $!A_R(x, y)$source with only the variables $x$source and $y$source free, such that $R(a, b)$source holds (i.e., $\tuple{a,b} \in R$source) iff $\Sat{M}{!A_R(x, y)}[s]$source for $s(x) = a$source and $s(y) = b$source.

Defining identity without the equality symbol

In first-order logic we can define the identity relation $\Id{\Domain{M}}$source (i.e., $\Setabs{\tuple{a,a}}{a \in \Domain{M}}$source) by the formula $\eq[x][y]$source. In second-order logic, we can define this relation without $\eq$source. For if $a$source and $b$source are the same element of $\Domain{M}$source, then they are elements of the same subsets of $\Domain{M}$source (since sets are determined by their elements). Conversely, if $a$source and $b$source are different, then they are not elements of the same subsets: e.g., $a \in \{a\}$source but $b \notin \{a\}$source if $a \neq b$source. So “being elements of the same subsets of $\Domain{M}$source” is a relation that holds of $a$source and $b$source iff $a = b$source. It is a relation that can be expressed in second-order logic, since we can quantify over all subsets of $\Domain{M}$source. Hence, the following formula defines $\Id{\Domain{M}}$source:

Exercise defining identity with a one way conditional

Show that $\lforall[X][(X(x) \lif X(y))]$source (note: $\lif$source not $\liff$source!) defines $\Id{\Domain{M}}$source.

Second order definition of transitive closure

If $R$source is a two-place predicate symbol, $\Assign{R}{M}$source is a two-place relation on $\Domain{M}$source. Perhaps somewhat confusingly, we'll use $R$source as the predicate symbol for $R$source and for the relation $\Assign{R}{M}$source itself. The transitive closure $R^*$source of $R$source is the relation that holds between $a$source and $b$source iff for some $c_1$source, dots, $c_k$source, $R(a,c_1)$source, $R(c_1, c_2)$source, dots, $R(c_k,b)$source holds. This includes the case if $k = 0$source, i.e., if $R(a,b)$source holds, so does $R^*(a,b)$source. This means that $R \subseteq R^*$source. In fact, $R^*$source is the smallest relation that includes $R$source and that is transitive. We can say in second-order logic that $X$source is a transitive relation that includes $R$source:

The first conjunct says that $R \subseteq X$source and the second that $X$source is transitive.

To say that $X$source is the smallest such relation is to say that it is itself included in every relation that includes $R$source and is transitive. So we can define the transitive closure of $R$source by the formula

We have $\Sat{M}{R^*(X)}[s]$source iff $s(X) = R^*$source. The transitive closure of $R$source cannot be expressed in first-order logic.

Inf characterizes infinite domains

$\Sat{M}{\fn{Inf}}$source iff $\Domain{M}$source is infinite.

Proof

$\Sat{M}{\fn{Inf}}$source iff $\Sat{M}{\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]] \land \lexists[y][\lforall[x][\eq/[y][u(x)]]]}[s]$source for some $s$source. If it does, $s(u)$source is an injective function, and some $y \in \Domain{M}$source is not in the range of $s(u)$source. Conversely, if there is an injective $f\colon \Domain{M} \to \Domain{M}$source with $\ran{f} \neq \Domain{M}$source, then $s(u) = f$source is such a variable assignment.

Count characterizes enumerable domains

$\Sat{M}{\fn{Count}}$source iff $\Domain{M}$source is enumerable.

Proof

Suppose $\Domain{M}$source is enumerable, and let $m_0$source, $m_1$source, dots, be an enumeration. By removing repetitions we can guarantee that no $m_k$source appears twice. Define $f(m_k) = m_{k+1}$source and let $s(z) = m_0$source and $s(u) = f$source. We show that

Suppose $M \subseteq \Domain{M}$source is arbitrary. Suppose further that $\Sat{M}{(X(z) \land \lforall[x][(X(x) \lif X(u(x)))])}[\Subst{s}{M}{X}]$source. Then $\Subst{s}{M}{X}(z) \in M$source and whenever $x \in M$source, also $(\Subst{s}{M}{X}(u))(x) \in M$source. In other words, since $\varAssign{\Subst{s}{M}{X}}{s}{X}$source, $m_0 \in M$source and if $x \in M$source then $f(x) \in M$source, so $m_0 \in M$source, $m_1 = f(m_0) \in M$source, $m_2 = f(f(m_0)) \in M$source, etc. Thus, $M = \Domain{M}$source, and so $\Sat{M}{\lforall[x][X(x)]}[\Subst{s}{M}{X}]$source. Since $M \subseteq \Domain{M}$source was arbitrary, we are done: $\Sat{M}{\fn{Count}}$source.

Now assume that $\Sat{M}{\fn{Count}}$source, i.e.,

for some $s$source. Let $m = s(z)$source and $f = s(u)$source and consider $M = \{m, f(m), f(f(m)), \dots\}$source. $M$source so defined is clearly enumerable. Then

by assumption. Also, $\Sat{M}{X(z)}[\Subst{s}{M}{X}]$source since $M \ni m = \Subst{s}{M}{X}(z)$source, and also $\Sat{M}{\lforall[x][(X(x) \lif X(u(x)))]}[\Subst{s}{M}{X}]$source since whenever $x \in M$source also $f(x) \in M$source. So, since both antecedent and conditional are satisfied, the consequent must also be: $\Sat{M}{\lforall[x][X(x)]}[\Subst{s}{M}{X}]$source. But that means that $M = \Domain{M}$source, and so $\Domain{M}$source is enumerable since $M$source is, by definition.

Exercise directly describing denumerable domains

The sentence $\fn{Inf} \land \fn{Count}$source is true in all and only denumerable domains. Adjust the definition of $\fn{Count}$source so that it becomes a different sentence that directly expresses that the domain is denumerable, and prove that it does.