[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Andrej and Ahmad, Thank you very much for your kind replies, with which I fully agree. At this point, I feel that I should emphasize that I am well aware that Martin-Löf type theory (MLTT) is fully compatible with classical logic formally speaking, which means that the theory has no derivation of the judgments (A) and (B) (A) ¬Π(A : U) A + ¬A true (B) H : Π(e : nat) (Σ (i, x : nat) T(e,i,x)) + ¬(Σ (i, x : nat) T(e,i,x)) ⊢ empty true However, regardless of not being derivable in MLTT, my question is: are (A) and (B) validated by the meaning explanation? In order to illustrate why I think this question may be plausible in principle, please let me recall you that both judgments (R) and (E) below are inderivable in (intensional) MLTT, yet they are both validated by Martin-Löf's (1982, 1984) meaning explanations. (R) Π(A : U)(x : A)(p : Id(A,x,x)) p = refl_x true (E) Π(p : Id(nat,0,1)) ⊢ 1 : nat -> nat Consequently, a judgment that is inderivable in MLTT need not be invalid by the meaning explanations. In the context of MLTT, that is, from inside the theory, I could not agree more with Andrej's point here: >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. but I would like to understand why, from the perspective of the meaning explanations alone (where terms are open-ended programs in a computation system resulted from an untyped notion of computation), the inference from 1 to 2 fails? Perhaps because programs are open-ended (as it was pointed out to me by Bob Harper), so that we have no means of recursively enumerate them all (because one can always extend the computational system with new programs)? But if this is the case, I fail to see why it is acceptable to rule out Kleene's T as a program (since programs are open-ended). Best, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ ________________________________ Von: Andrej Bauer <[email protected]> Gesendet: Freitag, 13. Oktober 2017 04:14 An: [email protected]; Bruno Bentzen Betreff: Re: [TYPES] Meaning explanations and the invalidity of the law of excluded middle 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
