Re: [isabelle] Existential Quantifiers



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.