[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

Hi Dan,

(I am answering the four questions backwards.)

I think it may be easier to make sense of this if you think of
X + (X->0) as a set (or space) rather than as a proposition.

Then ¬¬(X + (X->0)) says that the set X + (X->0) is nonempty (rather
than inhabited), and this is provable, as you said.

It is true that for any set X, the set X + (X->0) is nonempty.

¬EM says that there is no function (X : Type) -> X + (X->0)
that picks an inhabitant of the set X + (X->0) for any given X.

Martin

On 27/11/12 20:58, Dan Licata wrote:
> Hi Martin,
>
> Thanks!  That makes more sense.
>
> I'm still a little confused about the difference between
>
>    Exists X : Type. ¬(X + ¬ X)
>
> which we cannot prove (it would be contradictory with the usual fact
> that Pi X:Type. ¬¬(X + ¬ X) holds) and
>
>    ¬Em = ¬(Pi X : Type. X + ¬X)
>
> which we can prove with univlanece.
>
> I guess this is just saying that classical logic is inconsistent with
> univalence, but it's a little surprising to me that a mere de Morgan
> will do us in.
>
> Do you have any intuition for this?  I want to say that it has something
> to do with continuity:   ¬Em is asserting the absence of a "continuous"
> proof of excluded middle.
>
> -Dan
>
> On Nov27, Martin Escardo wrote:
>>
>> On 27/11/12 00:05, Dan Licata wrote:
>>> I'd like to understand exactly what statement is true in HoTT but not
>>> plain MLTT.
>>
>>
>> Let EM be the (large) type (Pi X : Type. X + ¬X).
>>
>>     (1) MLTT cannot inhabit EM (of course).
>>
>>     (2) MLTT cannot inhabit ¬EM (because classical ZF gives a model in
>>     which EM is inhabited).
>>
>> So EM is independent of MLTT.
>>
>> Now consider MLTT with the univalence axiom.
>>
>> By Hedberg's theorem, any type with decidable equality in an hset. So, if
>> EM holds, then every type is an hset.
>>
>> But if univalence holds, then there are large types which are not
>> hsets, as is well known.
>>
>> Combining these two procedures, you get an inhabitant of ¬EM.
>>
>> Martin
>>
>>
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe