#### Supplement to Independence Friendly Logic

## Existential second-order logic (a.k.a. \(\Sigma^{1}_1\) logic)

The set of *formulas* of existential second-order logic of
vocabulary \(\tau\) (formulas of \(\mathbf{ESO}[\tau]\)) is the
smallest set containing all formulas of \(\mathbf{FO}[\tau]\) and
which is closed under the following two rules:

- If \(\phi\) is an \(\mathbf{ESO}[\tau \cup \{f\}]\) formula, then \((\exists f)\phi\) is an \(\mathbf{ESO}[\tau]\) formula.
- If \(\phi\) is an \(\mathbf{ESO}[\tau \cup \{R\}]\) formula, then \((\exists R)\phi\) is an \(\mathbf{ESO}[\tau]\) formula.

*E.g.,* since \((\forall x)R(x, f(x))\) is an
\(\mathbf{FO}[\{R, f\}]\) formula, we have that \((\exists f)(\forall
x)R(x, f(x))\) is an \(\mathbf{ESO}[\{R\}]\) formula, and \((\exists
R)(\exists f)(\forall x)R(x, f(x))\) is an \(\mathbf{ESO}\) formula of
empty vocabulary. Observe that no second-order variables are involved
in the formulation of the syntax. For instance, what is bound by the
second-order quantifier \((\exists f)\) is a function symbol (not a
function variable). The notion of a free individual variable can be
defined exactly as in the case of \(\mathbf{FO}\). An
\(\mathbf{ESO}[\tau]\) formula is a
*sentence* if it contains no free variables. (For this syntax,
see *e.g.* Väänänen 2007. For an alternative formulation,
see *e.g.* Ebbinghaus & Flum 1999.)

The semantics of \(\mathbf{ESO}[\tau]\) is specified by defining
the *satisfaction relation* \(M, g \vDash \phi\) for all
\(\mathbf{ESO}[\tau]\) formulas \(\phi , \tau\) structures \(M\) and
variable assignments \(g\). The semantic clauses for atomic formulas
and for formulas of the forms \(\vee\), \(\wedge\), \(\exists x\),
\(\forall x\) and \({\sim}\) are as in \(\mathbf{FO}\). The remaining
semantic clauses make use of the notion of expansion of a \(\tau\)
structure. A \(\tau'\) structure \(M'\) is an *expansion* of a
\(\tau\) structure \(M\) (to the vocabulary \(\tau')\), if \(\tau
\subseteq \tau'\), \(\rM = \rM'\), and the structures \(M\) and \(M'\)
agree on the interpretations of all symbols of vocabulary \(\tau\). So
any difference between the structures is due to the interpretations of
symbols that belong to \(\tau'\) but not to \(\tau\).

- \(M, g \vDash(\exists f)\phi\) iff there is an expansion \(M'\) of the structure \(M\) to the vocabulary \(\tau \cup \{f\}\) such that \(M', g \vDash \phi\).
- \(M, g \vDash(\exists R)\phi\) iff there is an expansion \(M'\) of the structure \(M\) to the vocabulary \(\tau \cup \{R\}\) such that \(M', g \vDash \phi\).

For example, let \(N_1\) be the \(\{R\}\) structure whose domain is
the set of natural numbers and which interprets ‘\(R\)’ as
the relation *smaller than*. Consider evaluating the
\(\mathbf{ESO}[\{R\}]\) sentence \((\exists f)(\forall x)R(x, f(x))\)
relative to \(N_1\). We have

for any assignment \(g\), because by interpreting the function symbol ‘\(f\)’ by the function \(n \mapsto n+1,\) an expansion \(N_2\) of \(N_1\) to the vocabulary \(\{R, f\}\) is obtained, with \(N_2, g \vDash (\forall x)R(x, f(x))\). The reason why \(N_2, g \vDash (\forall x)R(x, f(x))\) holds is that indeed any natural number \(n\) is smaller than the natural number \(n+1\). And if \(N_0\) is a model of empty vocabulary with the set of natural numbers as its domain, we have \(N_0, g \vDash (\exists R)(\exists f)(\forall x)R(x, f(x))\), for any assignment \(g\), since \(N_0\) can be expanded to \(N_1\), which is a structure of vocabulary \(\{R\}\), and then we have \(N_1, g \vDash (\exists f)(\forall x)R(x, f(x))\), as just noted.

## Skolemizations and Skolem normal forms

Let us restrict our attention to \(\mathbf{IFL}\) formulas in negation
normal form. A skolemization of an \(\mathbf{IFL}\) formula will be a
*first-order* formula of a larger vocabulary.

In \(\mathbf{FO}\), it is customary to effect skolemization only with respect to existential quantifiers; discussing \(\mathbf{IFL}\), Hintikka (1991, 1996, 1997) extends skolemization to disjunctions as well. For example, a skolemization of the sentence

\[ (\forall x)(\forall y)(R(x, y) \; (\vee /\forall x) \; S(x, y)) \]of vocabulary \(\{R, S\}\) is the \(\mathbf{FO}\) formula

\[ (\forall x)(\forall y)([R(x, y) \wedge d(y) = 0] \vee [S(x, y) \wedge d(y) \ne 0]). \]of vocabulary \(\{R, S, d, 0\}\). Here the function term \(d(y)\) is used to explicate the dependence of the choice of a disjunct on the value interpreting the universal quantifier \((\forall y)\). ‘0’ is a fresh constant symbol, standing for some fixed element of the domain. This constant is used for forming the conjuncts \(d(y) = 0\) and \(d(y) \ne 0\); for those values \(a\) of \(y\) for which \(d(a) = 0\) holds, the left disjunct is chosen, while for those values of \(a\) of \(y\) for which \(d(a) \ne 0\) holds, it is the right disjunct that is chosen.

Let \(\tau\) be a fixed vocabulary, and 0 a constant symbol not in
\(\tau\). If \(\phi\) is an \(\mathbf{IFL}[\tau]\) formula, its
*skolemization* \(\mathrm{sk}[\phi]\) is the formula
\(\mathrm{sk}_{\phi}[\phi]\) that can be computed by the following
rules:

- If \(\psi\) is any of the formulas \(R(t_1 ,\ldots ,t_n)\) or \(t_1 = t_2\) or \({\sim}R(t_1 ,\ldots ,t_n)\) or \({\sim}t_1 = t_2\), then \(\mathrm{sk}_{\phi}[\psi] = \psi\).
- \(\mathrm{sk}_{\phi}[(\psi \; (\vee /\forall y_1 ,\ldots ,\forall y_n) \; \chi)] = (\mathrm{sk}_{\phi}[\psi] \wedge d(z_1 ,\ldots ,z_m) = 0)\) \(\vee\) \((\mathrm{sk}_{\phi}[\chi] \wedge d(z_1 ,\ldots ,z_m) \ne 0)\), where \(d\) is a fresh function symbol, and \((\forall z_1),\ldots ,(\forall z_m)\) are those universal quantifiers that precede the token of the disjunction sign in \(\phi\), but are not among \((\forall y_1),\ldots ,(\forall y_n)\).
- \(\mathrm{sk}_{\phi}[(\psi \; (\wedge /\exists y_1 ,\ldots ,\exists y_n) \; \chi)] = (\mathrm{sk}_{\phi}[\psi] \wedge \mathrm{sk}_{\phi}[\chi]\)).
- \(\mathrm{sk}_{\phi}[(\exists x/\forall y_1 ,\ldots ,\forall y_n)\psi] =\) \(\mathrm{sk}_{\phi}[\psi][x/f(z_1 ,\ldots ,z_m)]\), where \(f\) is a fresh function symbol, and \((\forall z_1),\ldots ,(\forall z_m)\) are those universal quantifiers that precede the token of the existential quantifier in \(\phi\), but are not among \((\forall y_1),\ldots ,(\forall y_n)\).
- \(\mathrm{sk}_{\phi}[(\forall x/\exists y_1 ,\ldots ,\exists y_n)\psi] = (\forall x) \mathrm{sk}_{\phi}[\psi]\).

If \(\phi\) is a formula, \(x\) is a variable, and \(t\) is a term, by stipulation \(\phi[x/t]\) stands for the formula obtained from \(\phi\) by replacing all free occurrences of \(x\) in \(\phi\) by \(t\). This use of the slash sign must not be confused with its use to mark quantifier independence as in IF logic.

Observe that
the skolemization \(\mathrm{sk}[\phi]\) of an \(\mathbf{IFL}\) formula (in negation
normal form) is itself an \(\mathbf{FO}\) formula in negation
normal form, written in a larger vocabulary including as many function
symbols as there are tokens of the disjunction sign and tokens of the
existential quantifier in \(\phi\) – and possibly including also the
constant symbol 0. The arities of these function symbols are uniquely
determined by the position of the token in the syntactic tree of the
formula \(\phi\). Note that the interpretations of those function symbols
in \(\mathrm{sk}[\phi]\) that are triggered by existential quantifiers are nothing
other than Skolem functions for those existential quantifiers in the
sense specified in *Section* 1.

With the help of the notion of skolemization, the notion of the Skolem
normal form of an \(\mathbf{IFL}\) formula can be defined. If \(\phi\)
is a formula of \(\mathbf{IFL}[\tau]\), and \(\mathrm{sk}[\phi]\) is its
skolemization of vocabulary \(\tau'\), with \(\tau \subseteq \tau'\),
the *Skolem normal form* \(\mathrm{SK}[\phi]\) of \(\phi\) is the
\(\mathbf{ESO}[\tau]\) formula \(\exists f_1 \ldots \exists
f_n \mathrm{sk}[\phi]\), where \(\{f_1 ,\ldots ,f_n\} = \tau'\) \
\(\tau\). Here the set \(\{f_1 ,\ldots ,f_n\}\) consists of the
function symbols introduced for tokens of the disjunction sign and
tokens of the existential quantifier in \(\phi\), together with the
constant 0 if \(\phi\) contains any disjunction tokens.