[TYPES] Meaning explanations and the invalidity of the law of excluded middle

[Andrej Bauer]

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