7

Skolem Constants and Functions Can Handle "exists" 2

• Quantifier scoping dependencies are shown using new functions called Skolem functions.

• For example, the formula ∀ y ∃ x . loves(x,y) would be encoded as a formula such as loves(sk2(Y), Y), where sk2 is a new function that produces a potentially new object for each value of Y.

• ∀ y ∃ x . loves(x,y) means "for everybody (y), there is somebody (x) that loves them." So sk2(Y) is the somebody that loves Y.