[Agda] Classical Mathematics for a Constructive World

[Dan Doel]

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