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