| |
 |
|
|
Science Forum Index » Logic Forum » Proving a formula can't be simplified...
Page 1 of 1
|
| Author |
Message |
| Snis Pilbor... |
 Posted: Mon May 12, 2008 10:28 am |
|
|
|
Guest
|
How does one usually go about proving that a formula of the form
forall x exists y phi(x,y)
or
exists x forall y phi(x,y)
isn't equivalent to one of the form
forall x phi(x)
or
exists x phi(x)
where phi(x) doesn't have unbounded quantifiers?
For example, if our language includes a function symbol f. How would
one prove that "forall x exists y f(y)=x" isn't equivalent to some
formula "forall x phi(x)" or "exists x phi(x)" with phi quantifier-
free? |
|
|
| Back to top |
|
| Snis Pilbor... |
| Posted: Mon May 12, 2008 2:34 pm |
|
|
|
Guest
|
On May 12, 7:56 pm, Jan Burse <janbu... at (no spam) fastmail.fm> wrote:
Quote: Snis Pilbor schrieb:
How does one usually go about proving that a formula of the form
forall x exists y phi(x,y)
or
exists x forall y phi(x,y)
isn't equivalent to one of the form
forall x phi(x)
or
exists x phi(x)
where phi(x) doesn't have unbounded quantifiers?
For example, if our language includes a function symbol f. How would
one prove that "forall x exists y f(y)=x" isn't equivalent to some
formula "forall x phi(x)" or "exists x phi(x)" with phi quantifier-
free?
forall x exists y A(x,y) is only not equivalent to
forall x B(x), if the theory doesnt admit quantifier
elimination.
Example that works: Theory of inequalities of linear
combinations over rationals, here every inequality:
p(x1,..,xn) < q(x1,..,xn) can be braught into
either into one of the following forms:
x1 < r(x2,..,xn)
x1 > r(x2,..,xn)
0 < r(x2,..,xn)
0 > r(x2,..,xn)
eliminations follows from the following observations:
exists x1 (x1 < r(x2,..,xn)) <=> true
exists x1 (x1 > r(x2,..,xn)) <=> true
exists x1 (x1 < r1(x2,..,xn) & x1>r2(x2,..,xn))
=> r2(x2,..,xn) < r1(x2,..,xn)
Example that doesnt work: Arithmetic, something like
ackerman function shows by majorization that unbounded
quantifer can not be braught into bounded quantifier.
You can read primitive recursive for bounded quantifier,
and partial recursive for unbounded quantifier.
Thanks, that helps a little. A theory can fail to have quantifier
elimination, but still SOME formulas can have quantifiers eliminated.
For example, "forall x 1=1", can obviously have a quantifier
eliminated, in any reasonable theory/structure/whatever. So just
because the theory itself doesn't have quantifier elimination, doesn't
mean a given formula can't have its quantifiers eliminated.
For example, I'm pretty sure the statement "forall x exists y f(y)=x",
considered as a statement about functions from the naturals to the
naturals, can't have a quantifier removed. That is, if I have defined
a set as S={f:N->N : forall x in N exists y in N f(y)=x}, then I can't
define S using fewer quantifiers using the same language. HOWEVER...
I have no idea how you'd prove this.
Thanks a lot
S.P. |
|
|
| Back to top |
|
| Jan Burse... |
| Posted: Mon May 12, 2008 6:56 pm |
|
|
|
Guest
|
Snis Pilbor schrieb:
Quote: How does one usually go about proving that a formula of the form
forall x exists y phi(x,y)
or
exists x forall y phi(x,y)
isn't equivalent to one of the form
forall x phi(x)
or
exists x phi(x)
where phi(x) doesn't have unbounded quantifiers?
For example, if our language includes a function symbol f. How would
one prove that "forall x exists y f(y)=x" isn't equivalent to some
formula "forall x phi(x)" or "exists x phi(x)" with phi quantifier-
free?
forall x exists y A(x,y) is only not equivalent to
forall x B(x), if the theory doesnt admit quantifier
elimination.
Example that works: Theory of inequalities of linear
combinations over rationals, here every inequality:
p(x1,..,xn) < q(x1,..,xn) can be braught into
either into one of the following forms:
x1 < r(x2,..,xn)
x1 > r(x2,..,xn)
0 < r(x2,..,xn)
0 > r(x2,..,xn)
eliminations follows from the following observations:
exists x1 (x1 < r(x2,..,xn)) <=> true
exists x1 (x1 > r(x2,..,xn)) <=> true
exists x1 (x1 < r1(x2,..,xn) & x1>r2(x2,..,xn))
<=> r2(x2,..,xn) < r1(x2,..,xn)
Example that doesnt work: Arithmetic, something like
ackerman function shows by majorization that unbounded
quantifer can not be braught into bounded quantifier.
You can read primitive recursive for bounded quantifier,
and partial recursive for unbounded quantifier.
Hope this helps
Best Regards |
|
|
| Back to top |
|
| William Elliot... |
| Posted: Mon May 12, 2008 11:47 pm |
|
|
|
Guest
|
On Mon, 12 May 2008, Snis Pilbor wrote:
Quote: How does one usually go about proving that a formula of the form
forall x exists y phi(x,y)
or
exists x forall y phi(x,y)
isn't equivalent to one of the form
forall x phi(x)
or
exists x phi(x)
where phi(x) doesn't have unbounded quantifiers?
Let Q(x) be "some y with P(x,y)".
for all x, some y with P(x,y) <-> for all x, Q(x)
Q(x) has no unbounded variables except x
provided P(x,y) has no unbounded bariable except x,y.
Let Q(x) be "for all y, P(x,y)".
some x with for all y, P(x,y) <-> some x with Q(x)
Q(x) has no unbounded variables except x
provided P(x,y) has no unbounded bariable except x,y.
for all x, some y with P(x,y) <-> for all x, P(x,f(x))
where f is the appropiate Skolem function
some x with for all y, P(x,y) <-> for all y, P(c,x)
where c is the appropiate 0-ary Skolem function, ie a constant.
has no non-trivial equivalent form
some x with Q(x)
Quote: For example, if our language includes a function symbol f. How would
one prove that "forall x exists y f(y)=x" isn't equivalent to some
formula "forall x phi(x)" or "exists x phi(x)" with phi quantifier-
free?
|
|
|
| Back to top |
|
| |
|
Page 1 of 1
All times are GMT - 5 Hours
The time now is Sat Jul 26, 2008 5:13 pm
|
|
