[Agda] Classical Mathematics for a Constructive World
Dan Licata
drl at cs.cmu.edu
Tue Nov 27 21:58:59 CET 2012
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
More information about the Agda
mailing list