### 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`

.