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

[Bruno Bentzen]

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 <andrej.bauer at andrej.com>
Gesendet: Freitag, 13. Oktober 2017 04:14
An: types-list at lists.seas.upenn.edu; 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