Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

Hello Bill, Ramana and all,

having printed out your opus as of June/4 and reading it byte by byte, I'm still struggling with several propositions. The most important one is the (allegation of a) diagonalization function

 Then B&J define

 diagonalization: E --->  E

Has anyone seen a constructive version of the diagonalization function, i.e. is (e.g. Cantor's) diagonalization function computable?

Heavy Reasoning,

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