[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Bruno, the problem with your argument is that inside type theory you cannot extract the Godel code of an argument from the argument, and so your outline of a proof won't work. That is, we cannot derive H : Π(e : nat) (Σ (i, x : nat) T(e,i,x)) + ¬(Σ (i, x : nat) T(e,i,x)) ⊢ empty because for that we would need to go somewhat like this: 1. Suppose we have such an H. 2. Then there is a (a code of) Turing machine e which computes like H. 3. We diagonalize against this e, and we get a contradiction. You cannot pass from 1 to 2 in type theory. With kind regards, Andrej
