[Agda] Classical Mathematics for a Constructive World

Dan Doel dan.doel at gmail.com
Mon Nov 26 21:42:30 CET 2012

On Mon, Nov 26, 2012 at 3:21 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

> On 26/11/12 15:44, Peter Divianszky wrote:
>> I would like to do classical math with
>> A \/ B = ((A + B) -> 0) -> 0
>> A => B = (A -> 0) \/ B
>> etc.
>> or use R instead of 0.
>> Suppose that I have a classical sequence which cannot be defined in
>> (N->2). Then I can't use your theorem with that sequence.
> Why not?
> (1) That it cannot be defined doesn't mean that it isn't there.
> (For example, the vast majority of the computable sequences N->2 is *not*
> definable in Agda or MLTT. What is more, what *is* definable depends on
> whether you have universes, how many of them you have, and whether or not
> you have W-types, etc. Moreover, for any extension of MLTT that remains
> strongly normalizing, there will necessarily remain plenty of non-definable
> computable sequences (by diagonalization).

For another example of this, consider classical formalisms like ZF.

Because of downward Loewenheim-Skolem, we could make a similar argument
that N -> 2 in ZF is merely the set of ZF-definable boolean sequences.
Everything you can prove about N -> 2 in ZF must hold true of the
ZF-definable sequences; a countable set (externally, anyhow).

But no one seems to think that the properties provable in ZF about N -> 2
are true _only_ of the ZF-definable sequences, and not of the set of 'all'
boolean sequences.

-- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121126/1aa49ced/attachment-0001.html

More information about the Agda mailing list