[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

On 26/11/12 15:44, Peter Divianszky wrote:
> I have two concerns:
>
> A)
>
> I would like to use Agda with --safe.

Coquand and Spivak have shown that MLTT remains strongly normalizing if 
you add recursion schemes such as the one used to give a proof term for 
the double-negation shift.

That should be safe enough. If it isn't for you, then, well, you won't 
have classical choice (having it is equivalent to having the 
double-negation shift).


> 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).

(2) You cannot define in Agda, or for that matter in any system for 
constructive mathematics, a boolean sequence a:N -> 2 such that a(n) == 
0 if and only the nth Turing machine halts when given input n, for example.

But you can show that such a sequence not-not-exists, and more generally 
that it K-exists. I.e. that classically it exists.

This kind of thing is precisely what is going on in the classical proof 
of the pigeonhole principle. That every boolean sequence has a constant 
subsequence cannot be proved. But you can show that such a sequence 
K-exists.


> I wish that your theorem was stated more general such that it could be
> used with both (N->2) and classical sequences.

There is no such a thing as a classical sequence. There are just 
sequences. The existence of some sequences can be proved constructively. 
The existence of other sequences can be proved classically only. And, to 
repeat, not every computable sequence can be defined in Agda, and yet 
you don't complain that your theorem cannot be used for all computable 
sequences because you can't define all them.

> B)
>
> Couldn't your way of thinking be turned against yourself?

I suppose everything I say can be turned against myself, particularly 
now that the internet exists.

> If you let others decide the meaning of (N->2), then your statement may
> not be the translation of the classical infinite pigeonhole principle
> any more.

You can only choose a meaning that is compatible with the rules of MLTT+DNS.

> Suppose that later I would like to use your theorem with OTT,
> parametricity, homotopy type theory or other development.

If you postulate DNS (to interpret classical choice), anything else you 
postulate be better consistent with DNS.

Notice that HoTT proves the negation of excluded middle, which MLTT 
doesn't. But you can have the negation of DNS together with the negation 
of EM, I believe. I believe the DNS may hold in suitable HoTT models, as 
continuity is one of the assumptions that give DNS.

I haven't thought about parametricity. I know what it means as a 
programming language concept, but it is less clear to me what it means 
as an axiom for constructive mathematics.

> The less your
> theorem says the more the meaning of it may change, am I right?

You may be right if you tell me what "the less you theorem says" means.

But of course, the fewer the axioms I have, the more situations my 
theorem apply to.

Best,
Martin