Existential second-order logic (a.k.a. Σ¹₁ logic)

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

• If φ is an ESO[τ∪{f}] formula, then (∃f)φ is an ESO[τ] formula.
• If φ is an ESO[τ∪{R}] formula, then (∃R)φ is an ESO[τ] formula.

E.g., since (∀x)R(x, f(x)) is an FO[{R, f}] formula, we have that (∃f)(∀x)R(x, f(x)) is an ESO[{R}] formula, and (∃R)(∃f)(∀x)R(x, f(x)) is an 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 (∃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 FO. An ESO[τ] 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 ESO[τ] is specified by defining the satisfaction relation M, g ⊨ φ for all ESO[τ] formulas φ, τ structures M and variable assignments g. The semantic clauses for atomic formulas and for formulas of the forms ∨, ∧, ∃x, ∀x and ~ are as in FO. The remaining semantic clauses make use of the notion of expansion of a τ structure. A τ′ structure M′ is an expansion of a τ structure M (to the vocabulary τ′), if τ ⊆ τ′, M = M′, and the structures M and M′ agree on the interpretations of all symbols of vocabulary τ. So any difference between the structures is due to the interpretations of symbols that belong to τ′ but not to τ.

• M, g ⊨ (∃f)φ iff there is an expansion M′ of the structure M to the vocabulary τ∪{f} such that M′, g ⊨ φ.
• M, g ⊨ (∃R)φ iff there is an expansion M′ of the structure M to the vocabulary τ∪{R} such that M′, g ⊨ φ.

For example, let N₁ be the {R} structure whose domain is the set of natural numbers and which interprets ‘R’ as the relation smaller than. Consider evaluating the ESO[{R}] sentence (∃f)(∀x)R(x, f(x)) relative to N₁. We have N₁, g ⊨ (∃f)(∀x)R(x, f(x)), for any assignment g, because by interpreting the function symbol ‘f’ by the function n n+1, an expansion N₂ of N₁ to the vocabulary {R, f} is obtained, with N₂, g ⊨ (∀x)R(x, f(x)). The reason why N₂, g ⊨ (∀x)R(x, f(x)) holds is that indeed any natural number n is smaller than the natural number n+1. And if N₀ is a model of empty vocabulary with the set of natural numbers as its domain, we have N₀, g ⊨ (∃R)(∃f)(∀x)R(x, f(x)), for any assignment g, since N₀ can be expanded to N₁, which is a structure of vocabulary {R}, and then we have N₁, g ⊨ (∃f)(∀x)R(x, f(x)), as just noted.

Skolemizations and Skolem normal forms

Let us restrict our attention to IFL formulas in negation normal form. A skolemization of an IFL formula will be a first-order formula of a larger vocabulary.

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

(∀x)(∀y)(R(x, y) (∨/∀x) S(x, y))

of vocabulary {R, S} is the FO formula

(∀x)(∀y)([R(x, y) ∧ d(y) = 0] ∨ [S(x, y) ∧ d(y) ≠ 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 (∀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) ≠ 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) ≠ 0 holds, it is the right disjunct that is chosen.

Let τ be a fixed vocabulary, and 0 a constant symbol not in τ. If φ is an IFL[τ] formula, its skolemization sk[φ] is the formula sk_φ[φ] that can be computed by the following rules.

• sk_φ[R(t₁,…, t_n)] = R(t₁,…, t_n).
• sk_φ[~R(t₁,…, t_n)] = ~R(t₁,…, t_n).
• sk_φ[(ψ (∨/∀y₁,…,∀y_n) χ)] = (sk_φ[ψ] ∧ d(z₁,…, z_m) = 0) ∨ (sk_φ[χ] ∧ d(z₁,…, z_m) ≠ 0), where d is a fresh function symbol, and (∀z₁),…,(∀z_m) are those universal quantifiers that precede the token of the disjunction sign in φ, but are not among (∀y₁),…,(∀y_n).
• sk_φ[(ψ (∧/∃y₁,…,∃y_n) χ)] = (sk_φ[ψ] ∧ sk_φ[χ])
• sk_φ[(∃x/∀y₁,…,∀y_n)ψ] = sk_φ[ψ][x/f(z₁,…, z_m)], where f is a fresh function symbol, and (∀z₁),…,(∀z_m) are those universal quantifiers that precede the token of the existential quantifier in φ, but are not among (∀y₁),…,(∀y_n).
• sk_φ[(∀x/∃y₁,…,∃y_n)ψ] = (∀x)sk_φ[ψ].

If φ is a formula, x is a variable, and t is a term, by stipulation φ[x/t] stands for the formula obtained from φ by replacing all free occurrences of x in φ 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 sk[φ] of an IFL formula (in negation normal form) is itself an 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 φ – 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 φ. Note that the interpretations of those function symbols in sk[φ] 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 IFL formula can be defined. If φ is a formula of IFL[τ], and sk[φ] is its skolemization of vocabulary τ′, with τ ⊆ τ′, the Skolem normal form SK[φ] of φ is the ESO[τ] formula ∃f₁…∃f_nsk[φ], where {f₁,…, f_n} = τ′ \ τ. Here the set {f₁,…, f_n} consists of the function symbols introduced for tokens of the disjunction sign and tokens of the existential quantifier in φ, together with the constant 0 if φ contains any disjunction tokens.