[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Paolo (and all), >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 Thank you very much for this nice observation! For the record, it took me some time but I am now fully convinced that the argument I outlined here in this thread must necessarily fail for reasons that can be seen both from the perspective of syntax (as Andrej has pointed out) or semantics (as explained by Jon). (In both cases, it seems to me that the situation looks a bit like Skolem's "paradox" in set theory: internally we can show that there is no bijection from IN to IR, but externally the theory has a countable model.) First, we can see that the do not have access to the syntax of the theory internally, so we do not have a criterion to construct the Gödel numbering function internally, even though we know externally that this function exists (besides such a function should also respect judgmental equality and assign the same Gödel number to judgmentally equal terms). Second, the reason why the meaning explanations cannot invalidate the law of the excluded middle is because they do not circumscribe the collection of all possible programs (in other words, the collection of terms is left open-ended) so they cannot rule out that oracles could be also programs. Simply put, Church's thesis is not accepted internally, even though it is true externally. Last but not least, I want to thank all of you who took the time to discuss and help me to understand these fascinating issues! Best, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ ________________________________ Von: Paolo Giarrusso <p.giarru...@gmail.com> Gesendet: Montag, 16. Oktober 2017 11:28 An: Types list Cc: Bruno Bentzen Betreff: Re: [TYPES] Meaning explanations and the invalidity of the law of excluded middle 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/
