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

[Paolo Giarrusso]

On 14 October 2017 at 15:38, Jon Sterling <jon at jonmsterling.com> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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).

Thanks to Jon for his clarification (also elsewhere)!

For those interested in more details, the same argument was laid out
by Thierry Coquand. This thread (linked from nLab) clarifies why it
does not apply to meaning explanations:

http://uf-ias-2012.wikispaces.com/file/view/IAS+-+MEANING+EXPLANATION+DISCUSSION/390300226/IAS%20-%20MEANING%20EXPLANATION%20DISCUSSION

Thierry Coquand writes A = forall n. exists m T(n,n,m) \/ not (exists
m T(n,n,m)) T Kleene predicate (*almost* the same as the above U = Π(e
: nat) (Σ (i, x : nat) T(e,i,x)) + ¬(Σ (i, x : nat) T(e,i,x))), and
gives a similar argument. IIUC, the discussion explains in more detail
why the argument works in a realizability PER-model but not in the
meaning explanations.
These quotes appear to me most relevant (though I recommend the rest,
especially on 'pre-mathematics' and the underlying philosophical
considerations):

> [Bob Constable:] The type A that Thierry is reasoning about is only known to be unrealizable if we accept Church's Thesis (CT).  We don't accept that in CTT.  If the reasoning is in the meta theory, using Church's Rule, then we might say that A is unrealizable based on an external analysis, but this is not expressible inside the theory and \x.0 is not a realizer inside for ~A.

> [Bob Harper:] it is a delicate point about the nature of the meaning semantics and the concept of "pre-mathematics" that peter has been defending.  the formula that thierry gave is indeed independent of HA viewed as a formal system, and if the meaning of the negation were given by provability in that formal system, then we would be in a situation where every unrealizable statement would be positively false.  but that is not the case.  the fact that thierry's A is unrealizable requires church's thesis, which we do not accept in the pre-mathematics (nor should we) in which the semantics is given.

> [Peter Dybjer:] I agree with the conclusion of this discussion that if you consider the "meaning explanations" as being about a fixed language of computable realizers, then we can justify anti-classical principles. Relating this to my talk, I see this as one of the "global" conditions that we do not want to assume in the "meaning explanations". The meaning of a judgement should only depend on its constituent terms, not on properties of the language in which it is embedded.

On Church's thesis in NuPRL, I also found
https://existentialtype.wordpress.com/2012/08/09/churchs-law/ helpful.

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