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

[Jon Sterling]

Hi Paolo and Bruno,

I just want to clarify that Nuprl is based on a very different and much
more complex 'meaning explanation' than Martin-Löf's; while Nuprl's
semantics validate the negation of the the principle of excluded middle
for types, it is compatible with classical reasoning at the
proof-irrelevant level (Constable calls this "virtual evidence
semantics").

On the other hand, my impression is that the MLTT meaning explanation
does not validate either the excluded middle for types, nor its
negation. The argument given by Andrej explains why...

Relatedly, both MLTT and Nuprl's meaning explanations refute Church's
Thesis if formulated internally (not only does it fail to hold, it is
false).

Best,
Jon



On Fri, Oct 13, 2017, at 05:37 AM, Paolo Giarrusso wrote:
> [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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/