Skolemization how is it achieved

Skolemization and Satisfiability

A formula in prenex normal form can have both universal and existential quantifiers in its quantifier prefix. If one is only interested in the satisfiability of the formula, the latter can be replaced if the existence of corresponding witnesses is postulated by constants (symbols) or functions (function symbols). The process of converting a formula in PNF into a corresponding formula without existential quantifiers is called skolemization. - The ways of speaking go back to the Norwegian mathematician, logician and philosopher Albert Thoralf Skolem.

example 1

The convergence of a sequence \ (\ {a_i \} _ {i \ in \ mathbf N} \) is often described as follows: For every \ (\ epsilon> 0 \) there is a \ (n_0 \ in \ mathbf N \) ), so that for all \ (i, j \ geq n_0 \) the relation \ (| a_i - a_j | <\ epsilon \) holds.

Alternatively, one could postulate the existence of a function \ (f \ colon \ mathbf R _ {> 0} \ to \ mathbf N \) and demand that for each \ (\ epsilon> 0 \) and for all \ (i, j> f (\ epsilon) \) the relation \ (| a_i - a_j | <\ epsilon \) holds.

Task 1

Rephrase a definition of continuity accordingly: A function \ (f \ colon \ mathbf R \ to \ mathbf R \) is continuous if \ (\ dots \)

The above example shows that when removing an existential quantifier \ (\ exists x_i ^ s \)

  1. the occurrences of \ (x_i ^ s \) are replaced by a term \ (f (\ dots) \) and
  2. in the term \ (f (\ dots) \) includes the free variables (except \ (x_i ^ s \)).

Satisfiability reductions

Formally, the process of skolemization can be summarized by the following definition of satisfiability reducibility.

A predicate logic formula \ (\ phi \) is satisfiability-reducible to a predicate logic formula \ (\ psi \) if:

  1. \ (\ Fvars \ phi = \ Fvars \ psi \).
  2. There are \ (S \) signatures \ (\ Sigma \) and \ (\ Sigma '\) such that \ (\ phi \ in \ Fpl \ Sigma \), \ (\ psi \ in \ Fpl {\ Sigma '} \) and \ (\ Sigma \ subseteq \ Sigma' \) apply.
  3. For every \ (\ Sigma \) structure \ (\ mathcal S \) there is a \ (\ Sigma '\) expansion \ (\ mathcal S' \), so that for every \ (\ mathcal S \) - Occupancy \ (\ beta \) applies: If \ (\ mathcal S, \ beta \ models \ phi \), then \ (\ mathcal S ', \ beta \ models \ psi \).
  4. For every \ (\ Sigma '\) expansion \ (\ mathcal S' \) and the associated \ (\ Sigma \) reduction \ (\ mathcal S \) and every \ (\ mathcal S \) occupancy \ ( \ beta \) apply: If \ (\ mathcal S ', \ beta \ models \ psi \), then \ (\ mathcal S, \ beta \ models \ phi \).

One writes \ (\ phi \ sqsubseteq \ psi \).

There are a number of simple connections.

Lemma 1
  1. If \ (\ phi \ sqsubseteq \ psi \) holds, then \ (\ Erfb \ phi \) holds if and only if \ (\ Erfb \ psi \) holds.
  2. If \ (\ phi \ sqsubseteq \ psi \) applies and \ (Q \) is a quantifier and \ (x_i ^ s \) a variable, so is \ (Q x_i ^ s \ phi \ sqsubseteq Q x_i ^ s \ psi \ ).
  3. The relation \ (\ sqsubseteq \) is transitive.

Skolemization

Theorem for the skolemization of existential quantifiers

Let \ (\ psi \) be a predicate logic formula, \ (i \ in \ Naturals \), \ (s \ in S \) and \ (x_ {i_0} ^ {s_0}, \ dots, x_ {i_ {n -1}} ^ {s_ {n-1}} \) an enumeration of the free variables in \ (\ psi \) without \ (x_i ^ s \). Furthermore, let \ (f \) be a function symbol that does not appear in \ (\ psi \) and has the single signature \ (\ langle s_0, \ dots, s_ {n-1}, s \ rangle \). Then \ [\ exists x_i ^ s \ psi \ sqsubseteq \ psi \ {x_i ^ s \ mapsto f (x_ {i_0} ^ {s_0}, \ dots, x_ {i_ {n-1}} ^ {s_ {n -1}}) \} \] and the substitution is responsible for the formula.

In the special case that \ (\ psi \) has no free variables besides \ (x_i ^ s \), a corresponding constant symbol is added instead of a function symbol.

proof

So let \ (\ phi = \ exists x_i ^ s \ psi \) and \ (\ tilde \ psi = \ psi \ {x_i ^ s \ mapsto f (x_ {i_0} ^ {s_0}, \ dots, x_ {i_ {n-1}} ^ {s_ {n-1}}) \} \). Let \ (\ Sigma \) and \ (\ Sigma '\) be the corresponding signatures, i.e., \ (\ Sigma' = \ Sigma \ cup \ {f \} \).

Conditions 1 and 2 are obviously met.

In order to determine the \ (\ Sigma '\) expansion of \ (\ mathcal S \) searched for in 3., only \ (f ^ {\ mathcal S'} \) has to be defined. So let \ (a_i \ in s_i ^ {\ mathcal S} \) for each \ (i

  1. \ (\ mathcal S, \ gamma \ models \ phi \).

  2. \ (\ mathcal S, \ gamma \ not \ models \ phi \).

(The spellings are justified on the basis of the coincidence lemma.) In the first case, \ (f ^ {\ mathcal S '} (a_0, \ dots, a_ {n-1}) = a \) for a \ (a \), for which \ (\ mathcal S, \ gamma [x_i ^ s \ mapsto a] \ models \ psi \) applies. In the second case one sets \ (f ^ {\ mathcal S '} (a_0, \ dots, a_ {n-1}) = a \) for any \ (a \ in s ^ {\ mathcal S} \).

So apply \ (\ mathcal S, \ beta \ models \ phi \). Let \ (\ gamma \) be the restriction of \ (\ beta \) to \ (\ Fvars \ psi \ setminus \ {x_i ^ s \} \). Then \ (\ mathcal S, \ gamma \ models \ phi \) and thus \ (\ mathcal S, \ gamma [x_i ^ s \ mapsto f ^ {\ mathcal S '} (a_0, \ dots, a_ { n-1})] \ models \ psi \) with \ (a_i = \ gamma (x_ {i_j} ^ {s_j}) \) for each \ (i

Now, however, \ (f ^ {\ mathcal S '} (a_0, \ dots, a_ {n-1}) = \ PLSem {f (x_ {i_0} ^ {s_0}, \ dots, x_ {i_ {n- 1}} ^ {s_ {n-1}})} \ gamma {\ mathcal S '} \). The substitution lemma results in \ (S, \ gamma \ models \ psi \ {x_i ^ s \ mapsto f (x_ {i_0} ^ {s_0}, \ dots, x_ {i_ {n-1}} ^ {s_ { n-1}}) \} = \ tilde \ psi \). So (i) holds.

That 4. applies, follows from the sentence for

A skolemization algorithm

A given formula in PNF can easily be converted into a satisfiability-equivalent formula with the help of the theorem for scolemization.

Skolem \ ((\ phi) \)

Precondition: \ (\ phi \) is in prenex normal form
if \ (\ phi \) is quantifier-free
return \ (\ phi \)
elseif \ (\ phi = \ forall x_i ^ s \ psi \)
return \ (\ forall x_i ^ s \) Skolem \ ((\ psi) \)
else
write \ (\ phi = \ exists x_i ^ s \ psi \)
let \ (\ {x_ {i_0} ^ {s_0}, \ dots, x_ {i_ {n - 1}} ^ {s_ {n - 1}} \} = \ text {fvars} (\ phi) \)
let \ (\ tilde \ psi = \) Skolem \ ((\ psi) \)
choose \ (f \) not in the current signature
add \ (f \) with type \ (\ langle s_0 \ dots s_ {n-1}, s \ rangle \) to the current signature
return \ (\ tilde \ psi \ {x_i ^ s \ mapsto f (x_ {i_0} ^ {s_0}, \ dots, x_ {i_ {n - 1}} ^ {s_ {n - 1}}) \} \ )
Postcondition: \ (\ phi \ sqsubseteq \) return.

The application of the above algorithm (or corresponding variants) is called skolemization.

Example 2

The application of the algorithm in the singular case to \ (\ exists x_0 \ forall x_1 \ exists x_2 \, r (x_0, x_1, x_2, x_3) \) results in:

  1. \ (\ text {Skolem} (\ exists x_0 \ forall x_1 \ exists x_2 \, r (x_0, x_1, x_2, x_3)) = \ text {Skolem} (\ forall x_1 \ exists x_2 \, r (x_0, x_1 , x_2, x_3)) \ {x_0 \ mapsto f (x_3) \} \).

  2. \ (\ text {Skolem} (\ forall x_1 \ exists x_2 \, r (x_0, xx_1, x_2, x_3)) = \ forall x_1 \ text {Skolem} (\ exists x_2 \, r (x_0, x_1, x_2, x_3)) \).

  3. \ (\ text {Skolem} (\ exists x_2 \, r (x_0, x_1, x_2, x_3)) = \ text {Skolem} (r (x_0, x_1, x_2, x_3)) \ {x_2 \ mapsto g (x_0 , x_1, x_3) \} = r (x_0, x_1, g (x_0, x_1, x_3), x_3) \).

  4. The result is \ (\ forall x_ 1 \, r (x_0, x_1, g (x_0, x_1, x_3), x_3) \ {x_0 \ mapsto f (x_3) \} = \ forall x_1 r (f (x_3), x_1, g (f (x_3), x_1, x_3), x_3) \).

Task 4

Skolemize the formula \ (\ forall x_0 \ exists x_1 \ exists x_2 \ forall x_3 (r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3))) \) . Include the law you are using at each step.

solution

According to the law for the elimination of quantifiers, \ [\ forall x_0 \ exists x_1 \ exists x_2 \ forall x_3 (r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3) )) \ equiv \ forall x_0 \ exists x_1 \ forall x_3 (r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3)))) \ enspace. \] Application of the algorithm for skolemization gives:

  1. \ (\ text {Skolem} (\ forall x_0 \ exists x_1 \ forall x_3 (r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x_3)))) = \ forall x_0 \ text {Skolem} (\ exists x_1 \ forall x_3 (r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3))) \ enspace. \)

  2. \ (\ forall x_0 \ text {Skolem} (\ exists x_1 \ forall x_3 (r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3)))) = \ forall x_0 \ text {Skolem} (\ forall x_3 (r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3))) \ {x_1 \ mapsto h (x_0) \} \ enspace. \)

  3. \ (\ forall x_0 \ text {Skolem} (\ forall x_3 (r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3)))) \ {x_1 \ mapsto h (x_0) \} = \ forall x_0 \ forall x_3 \ text {Skolem} ((r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3))))) \ {x_1 \ mapsto h (x_0) \} \ enspace. \)

  4. \ (\ forall x_0 \ forall x_3 \ text {Skolem} ((r (x_0, f (x _1)) \ rightarrow r '(f (x_0), g (x_0, x _3)))) \ {x_1 \ mapsto h (x_0) \} = \ forall x_0 \ forall x_3 (r (x_0, f (h (x_0))) \ rightarrow r '(f (x_0), g (x_0, x _3))) \ enspace. \)

Task 5

Use the example above to check that the algorithm is correct. To do this, consider the structure whose support set are the integers and where \ (r \) is the relation that applies if the product of the first two arguments is equal to the product of the last two arguments.

Exercise 6

Modify the above algorithm so that quantifications that are unnecessary (a variable that does not occur freely is quantified) are not treated any further.

Exercise 7

Think about whether it is possible to perform scolemization on any formulas - including formulas that are not in PNF. How could this possibly look like?

Exercise 8
  1. Skolemize the following formula:
    \ (\ varphi = \ exists x_1 \ forall x_2 ((e (x_0, x_1) \ wedge e (x_1, x_2)) \ rightarrow e (x_0, x_2)) \)
  2. The following \ (\ Sigma_ {graph} \) structure \ (\ mathcal S \) is given: \ [\ begin {align} \ text {Vertex} ^ \ mathcal S & = \ {a, b, c, d \ } \ enspace, \ e ^ \ mathcal S & = \ {\ langle a, b \ rangle, \ langle a, c \ rangle, \ langle a, d \ rangle, \ langle c, b \ rangle, \ langle c , d \ rangle, \ langle d, b \ rangle \} \ enspace \ end {align} \]

Give expansions of \ (\ Sigma_ {graph} \) and \ (\ mathcal S \) which prove that \ (\ varphi \) is satisfiability-reducible to the skolemization of \ (\ varphi \).

Exercise 9
  1. Give a skolemization of the following formula \ (\ varphi \):

\ (\ varphi = \ forall x_0 \ exists x_2 \ exists x_3 (\ neg (x_2 \ doteq x_3) \ wedge (e (x_0, x_1) \ rightarrow (e (x_1, x_2) \ wedge e (x_1, x_3)) )) \)

  1. The result from a) is denoted by \ (\ psi \). A \ (\ Sigma _ {\ text {graph}} \ text {structure} \ \ mathcal S \) is given by: \ begin {align *} \ text {Vertex} ^ {\ mathcal S} & = \ {a , b, c, d, e, f, g, h, i \}, \ e ^ {\ mathcal S} & = \ {\ langle a, b \ rangle, \ langle a, c \ rangle, \ langle a, d \ rangle, \ langle b, e \ rangle, \ langle b, f \ rangle, \ langle c, g \ rangle, \ langle d, h \ rangle, \ langle d, i \ rangle \}. \ end {align *} Enter two pairs of expansions \ ((\ Sigma '_ {\ text {graph}}, \ mathcal S') \) and \ ((\ Sigma '_ {\ text {graph}}, \ mathcal S '') \) from \ ((\ Sigma _ {\ text {graph}}, \ mathcal S) \), which prove that \ (\ varphi \) is satisfiability-reducible to \ (\ psi \). The structures \ (\ mathcal S '\) and \ (\ mathcal S' '\) should differ.
solution
  1. \ (\ forall x_0 (\ neg (f (x_0, x_1) \ doteq g (x_0, x_1, f (x_0, x_1))) \ wedge (e (x_0, x_1) \ rightarrow (e (x_1, f (x_1 )) \ wedge e (x_1, g (x_0, x_1, f (x_0, x_1))))) \)

  2. The signature \ (\ Sigma _ {\ text {graph}} \) can be extended to \ (\ Sigma '_ {\ text {graph}} \) as follows: \ begin {align *} \ Sigma' _ {\ text {graph}} (e) & = \ Sigma _ {\ text {graph}} (e) \ \ Sigma '_ {\ text {graph}} (f) & = \ langle \ text {VertexVertex}, \ text { Vertex} \ rangle \ \ Sigma '_ {\ text {graph}} (g) & = \ langle \ text {VertexVertexVertex}, \ text {Vertex} \ rangle \ end {align *} The following structure \ (\ mathcal S '\) is a possible expansion of \ (\ mathcal S \) with the desired property. \ begin {align *} \ text {Vertex} ^ {\ mathcal S '} & = \ text {Vertex} ^ {\ mathcal S} \ \ text {e} ^ {\ mathcal S'} & = \ text { e} ^ {\ mathcal S} \ f ^ {\ mathcal S '} (x_0, x_1) & = \ begin {cases} e, & \ text {if $ x_1 = b $} \ h, & \ text {if $ x_1 = d $} \ a, & \ text {otherwise} \ end {cases} \ g ^ {\ mathcal S '} (x_0, x_1, x_2) & = \ begin {cases} f, & \ text {if $ x_1 = b $ and $ x_2 = e $} \ i, & \ text {if $ x_1 = d $ and $ x_2 = h $} \ a, & \ text {otherwise} \ end { cases} \ \ end {align *}

    In \ (\ mathcal S '' \) one could e.g. otherwise replace the element \ (a \) with \ (b \).

The decisive conclusion from the correctness of the above algorithm is:

Corollary 1

A formula \ (\ phi \) in PNF is satisfiable if and only if Skolem \ ((\ phi) \) is satisfiable.

Skolemizing sets of formulas

The process of skolemization can easily be extended to sets of formulas, i.e. one can also define Skolem \ ((\ Phi) \) in a meaningful way. It should be noted that the formulas in \ (\ Phi \) have to be skolemized one after the other, so that the new symbols to be selected do not appear in the other formulas.

The procedure does not terminate for infinite sets, but one can still meaningfully define Skolem \ ((\ Phi) \). Each formula is skolemized separately in such a way that different new symbols are used for different formulas. Here it can happen that an infinite number of new symbols are necessary, so that the resulting signature is infinite.

If \ (\ Phi \) is enumerable, then Skolem \ ((\ Phi) \) is also enumerable.

Corollary 2

A set of formulas \ (\ Phi \) in PNF is satisfiable if and only if Skolem \ ((\ Phi) \) is satisfiable.