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 

"Ex x.P(y)", where P is some predicate

by it's solution


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 

"iterate until x-y**2<eps".


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