06:06
@Wildcard Yes. Informally, we can say that the diagonal argument does not care whether S = Func(N,bool) and Func(N,S) are constructively interpreted or not. As long as the formal system permits us to reason about objects and syntactically verify their types, then it goes through. I'm very glad that my last explanation worked. =)
@Wildcard I'm a realist, by the way, so I accept the type of natural numbers, but not the complete collection as a single infinite entity, and I also accept function types in a slightly broader sense than just programs, but not the 'full' power-set.
I remember at one point you said you didn't believe in the existence of anything that isn't computable. If you don't mind, I would like to ask you again, whether you believe the halting problem always has an answer. To be precise, do you believe that given any program on an input, executed on an ideal Turing machine, it either halt or does not halt?
