Email Gateway (Aug 18 2022 at 14:01): Email Gateway (Aug 18 2022 at 14:01):From: jd@cococo.de
Hello all,
after having thought a lot about existential quantifiers in predicate
logic I came to the conclusion, that there is no need for several
instances of a specific quantifier. You can normalize each formula to a
prenex formula and afterwards combine the quantifiers to quantifiers over
vectors. So only one existential quantifier and only one all quantifier
would suffice. Am I right? a) If yes, can you tell a method for
decomposition of vectorized quantifiers? b) If not, please give an
example, where vectorization does not work.
Jens
Email Gateway (Aug 18 2022 at 14:01):From: Lawrence Paulson <lp15@cam.ac.uk>
This type of transformation may work in theory, but increases the
length of the proof enormously. Theory again tells us that the
increase in proof length could be non-elementary (inconceivably vast).
Larry Paulson
Email Gateway (Aug 18 2022 at 14:02):From: Tim McKenzie <tjm1983@gmail.com>
So you want to group all the existential quantifiers together with
each other, and likewise all the universal ones together? In
general, ALL. EX. ALL. isn't the same as EX. ALL. ALL. or ALL.
ALL. EX. For example:
ALL x. ALL y. EX z. z > x + y
is true (for various numerical types), but
ALL x. EX z. ALL y. z > x + y
is not true.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 14:02):From: Tjark Weber <webertj@in.tum.de>
That is correct, of course. On the other hand,
ALL x. EX z. ALL y. z(y) > x + y
is equivalent to the former (cf. Skolemization, axiom of choice).
Perhaps http://en.wikipedia.org/wiki/Skolem_normal_form is instructive.
Regards,
Tjark
Email Gateway (Aug 18 2022 at 14:02):From: jd@cococo.de
Hello Tim and Tjark,
thanks for the examples and explanations. Now I understand my point of
view better. Because I am into constructive proofs versus existential
statements, I am interested in resolving existential quantifiers to their
(minimal) solutions, which may be formulas or halting programs. When
replacing
"Ex x.P(y)", where P is some predicate
by it's solution
"x=f(y)"
I currently only consider the minimal solutions for f(y), which is unique.
I understand, that there are situations, when our rational mathematics
leads to existential statements, especially when considering sequences
like
"iterate until x-y**2<eps".
Regards,
Jens
Last updated: Apr 25 2024 at 12:23 UTC