Stanford Encyclopedia of Philosophy

Supplement to Independence Friendly Logic

Semantic Games for IF First-order Logic

In addition to two players, there are two roles: ‘verifier’ and ‘falsifier.’ Initially, player 1 is ‘falsifier’ and player 2 is ‘verifier.’ For every IF first-order formula φ, model M, and variable assignment g, a two-player zero-sum game G(φ, M, g) between player 1 and player 2 is associated.

  1. If φ = R(t1,…, tn) and M, g ⊨ R(t1,…, tn), the ‘verifier’ wins (and the ‘falsifier’ loses); otherwise the ‘falsifier’ wins (and the ‘verifier’ loses).
  2. If φ = ~ψ, the rest of the game is as in G(ψ, M, g), where player 1 has the role that player 2 had in G(φ, M, g), and vice versa.
  3. If φ = (ψ(∧/∃y1,…,∃yn) χ), the ‘falsifier’ chooses θ ∈ {ψ,χ} and the rest of the game is as in G(θ, M, g).
  4. If φ = (ψ (∨/∀y1,…,∀yn) χ), the ‘verifier’ chooses θ ∈ {ψ,χ} and the rest of the game is as in G(θ, M, g).
  5. If φ = (∀x/∃y1,…,∃yn)ψ, the ‘falsifier’ chooses an element a from M, and the rest of the game is as in G(ψ, M, g[x/a]).
  6. If φ = (∃x/∀y1,…,∀yn)ψ, the ‘verifier’ chooses an element a from M, and the rest of the game is as in G(ψ, M, g[x/a]).

The role switch interpretation of negation, originally proposed by Hintikka (1968), is incorporated in clause (2). The players' strategy functions are subject to the same restrictions as with formulas in negation normal form.

Existential second-order logic (a.k.a. Σ11 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:

E.g., since (∀x)R(x, f(x)) is a first-order formula of vocabulary {R, f}, 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 first-order logic. An ESO[τ] formula is an ESO[τ] 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 first-order logic. 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 τ.

For example, consider evaluating the ESO[{R}] sentence (∃f)(∀x)R(x, f(x)) relative to the {R} structure M, interpreting ‘R’ as the relation ‘smaller than’ on the domain M of natural numbers. Now M, g ⊨ (∃f)(∀x)R(x, f(x)), for any assignment g, because by interpreting the function symbol ‘f’ by the function n maps-to n+1, an expansion M′ of M to the vocabulary {R, f} is obtained, with M′, g ⊨ (∀x)R(x, f(x)). The reason why M′, 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, then N, g ⊨ (∃R)(∃f)(∀x)R(x, f(x)), for any assignment g, since N can be expanded to M, which is a structure of vocabulary {R}, and then we have M, g ⊨ (∃f)(∀x)R(x, f(x)), as just noted.

Skolemizations and Skolem normal forms

Let us restrict our attention to IF first-order formulas in negation normal form. A skolemization of an IF first-order formula will be a first-order formula of a larger vocabulary. Consider some examples. A skolemization of the formula (∀x)(∃y)R(x, y, z) of vocabulary {R} will be the formula (∀x)R(x, f(x), z) of vocabulary {R, f}, and a skolemization of the sentence (∀x)(∃y)(∀z)(∃v/∀x)R(x, y, z, v) of vocabulary {R} will be the sentence (∀x)(∀z)R(x, f(x), z, h(z)) of vocabulary {R, f, h}. Observe the introduction of fresh function symbols, erasing existential quantifiers, and replacing variables bound by existential quantifiers by function terms, where precisely those variables bound by preceding universal quantifiers appear as arguments that are not listed in the independence indication of the corresponding existential quantifier. A further example: a skolemization of the formula (∀x)(P(x) ∨ Q(x)) of vocabulary {P, Q} will be the sentence

(∀x)([P(x) ∧ d(x) = 0] ∨ [Q(x) ∧ d(x) ≠ 0])

of vocabulary {P, Q, d,0}. Here the function term d(x) is used to explicate the dependence of the choice of a disjunct on the value interpreting the universal quantifier (∀x). ‘0’ is a fresh constant symbol, standing for some fixed element of the domain. This constant is used for forming the conjuncts d(x) = 0 and d(x) ≠ 0; for those values a of x for which d(a) = 0 holds, the left disjunct is chosen, while for those values of a of x for which d(a) ≠ 0 holds, it is the right disjunct that is chosen. Similarly, a skolemization of the formula

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

of vocabulary {R, S} will be the formula

(∀x)(∀y)([R(x, y, z) ∧ d(y) = 0] ∨ [S(x, y, z) ∧ d(y) ≠ 0])

of vocabulary {R, S, d,0}. The function term d(y) only has y in its argument position; the choice of a disjunct depends on the value interpreting the universal quantifier (∀y), but not on the value interpreting the universal quantifier (∀x). In FO, it is customary to effect skolemization only with respect to existential quantifiers; discussing IF first-order logic, Hintikka (1991, 1996, 1997) extended skolemization to disjunctions as well.

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

(For the notation θ[x/t] with θ a formula, x a variable and t a term, see footnote 44.) Observe that the skolemization sk[φ] of an IF first-order 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 IF first-order formula can be defined. If φ is a formula of IF first-order logic of vocabulary τ, and sk[φ] is its skolemization of vocabulary τ′, with τ ⊆ τ′, the Skolem normal form SK[φ] of φ is the ESO[τ] formula ∃f1…∃fnsk[φ], where {f1,…, fn} = τ′ \ τ. (Recall that hence the set {f1,…, fn} 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.) The second-order formula SK[φ] (referred to when using capital letters) must not be confused with the FO formula sk[φ] (referred to when using lower case letters).