Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



I certainly do not want to get dragged into these interminable discussions. However, as a general remark: there is nothing mysterious about diagonalization functions. For example, the one for Russell's paradox is simply {X. X notin X}. Here, of course, the notion of computable is irrelevant, but it's certainly easily defined.

For proving undecidability of the halting problem, the definition is equally simple and it is computable if you assume the halting test itself to be computable, which is the point of the theorem.

Larry

On 6 Jun 2012, at 09:09, Jens Doll wrote:

> 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,
> Jens
> 






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