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

[Paolo Giarrusso]

On 13 October 2017 at 10:23, Bruno Bentzen <b.bentzen at hotmail.com> wrote:
> 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).

Dear Bruno,

I understand the meaning explanation can be seen as basically a
realizability interpretation of type theory based on untyped realizers
[1]? Then let me provide my 2 cents, based on my (partial)
understanding of realizability and PER models. I welcome any
corrections.

Since we talk about truth in a model and not usual provability, I'll
write Γ ⊧ t : T, instead of Γ ⊢ t : T true.

I'm not 100% what you mean by open-ended — with an open-ended set of
terms, where you allow adding "postulates", you can't even validate
(E) [1].
But once you fix your set of terms, you can do structural induction on
them *in the metatheory*, but even untyped lambda terms cannot inspect
the structure of their arguments (as Andrej explained), unlike Turing
machines.

So, let's write U for your type Π(e : nat) (Σ (i, x : nat) T(e,i,x)) +
¬(Σ (i, x : nat) T(e,i,x)). Then, it should be provable
metatheoretically that there is no closed value of of type U (as you
say). This reasoning cannot be internalized into a lambda term,
essentially by Andrej's argument; yet, I expect the metatheoretic
argument is sufficient to prove that H: U ⊧ ⊥ (or, in your notation,
that H : U ⊢ empty true).

Specifically, just like

(E) p : Id(nat,0,1) ⊧ 1 : nat -> nat

holds because Id(nat,0,1) is empty, and vacuously for all members p of
Id(nat,0,1) we have that 1 realizes nat -> nat, I think that judgement

(B) p : U ⊧ 1 : empty

holds by a similar argument.

In either case, if we add postulates to sets of realizers so that
Id(nat,0,1) or U is non-empty [1], we get a different model where (E)
and (B) fail—however, such postulates could not be reduced, destroying
canonicity. Which is good: canonicity enables computation, so a
realizer for excluded middle can't actually be computable in all
cases. (Formally, IIUC, instead of considering closed values as
realizers, we'd allow a few free variables, and make assumptions on
what types those variables realize).

On a related note, IIUC your judgement holds in NuPRL (by a different
proof?), which appears to be also based on the meaning explanation
[2]. That's how I interpret
http://www.nuprl.org/LibrarySnapshots/Published/Version2/Standard/quot_1/no-excluded-middle-quot-true2.html
(where ⇃ is defined in
http://www.nuprl.org/LibrarySnapshots/Published/Version2/Standard/per!type!1/quotient.html
and quotients realizers together).

[1] https://ncatlab.org/nlab/show/meaning+explanation
[2] http://www.jonmsterling.com/pdfs/meaning-explanations.pdf

Cheers,
-- 
Paolo G. Giarrusso - Ph.D. Student, Tübingen University
http://ps.informatik.uni-tuebingen.de/team/giarrusso/