Skolemization and quantifier dependencies
- From: "Michael De" <mikejde@xxxxxxxxx>
- Date: 2 Mar 2006 22:27:23 -0800
When we Skolemize a sentence A, we replace all the existential
quantifiers Ex1,...,Exn and the variables x1,...,xn they bind with
Skolem functions f1,...,fn whose arguments consist of only the
variables y1,...,ym bound by all the universal quantifiers preceding
the Ex1,...,Exn. This is supposed to illustrate that the existential
quantifiers (and associated variables) rely only on the universal
quantifiers. But why don't they also rely on preceding existential
quantifiers?
For example, consider the sentence (Ax)(Ey)(Az)(Ew)B(x,y,z,w) and its
Skolemization (Ef)(Eg)(Ax)(Az)B(x,f(x),z,g(x,z)). Why doesn't the last
Skolem function g have a third argument consisting of the term f(x)
which is the function that replaced y?
I have a deep feeling that I missing something very fundamental, but I
can't quite figure out what.
.
- Follow-Ups:
- Re: Skolemization and quantifier dependencies
- From: Keith Ramsay
- Re: Skolemization and quantifier dependencies
- From: Aatu Koskensilta
- Re: Skolemization and quantifier dependencies
- Prev by Date: Re: Proving induction
- Next by Date: Re: truth/falsity of sentences in first-order logic
- Previous by thread: Re: Proving induction
- Next by thread: Re: Skolemization and quantifier dependencies
- Index(es):