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

[Bruno Bentzen]

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.giarrusso at 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 <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/