[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

Hi Martin,

Your way of thinking is quite convincing.
First I was totally convinced and relieved but later I became suspicious.
I have two concerns:

A)

I would like to use Agda with --safe.
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.

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

B)

Couldn't your way of thinking be turned against yourself?
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.

Suppose that later I would like to use your theorem with OTT, 
parametricity, homotopy type theory or other development. The less your 
theorem says the more the meaning of it may change, am I right?

Thanks,
Peter


>> I guess in your example ₂ℕ should be computable.
>
> No, no, no. You have to be very careful here. There are many things
> (N->2) can be, and also many things it cannot be.
>
> Let's notice a few things about Agda and type theory.
>
> First of all, excluded middle is not false. It is not provable, which
> is quite different from being false.
>
> To be precise, excluded middle is independent.
>
>     EM : (X : Type) -> X + (X -> 0).
>
> Here 0 is the type with no elements, and _+_ is the disjoint sum of
> two types.
>
> EM cannot be proved in type theory, and its "negation" (EM -> 0)
> cannot be proved either. It cannot be proved because it is false in
> recursive models of type theory. Its negation cannot be proved because
> EM is true in the classical model of type theory.
>
> Type theory doesn't make any commitment regarding excluded middle.
>
> Likewise, type theory doesn't make any commitment regarding what the
> type (N->2) should be. In particular, the statement (suitably
> formalized) "all elements of (N->2) are computable" is
> independent. It cannot be proved. Its negation cannot be proved.
>
> Intuitively, this should be clear to you as an Agda
> programmer/prover. When you have a variable a:N->2 in a context, you
> don't have together with "a" a proof term stating that "a" is
> computable. Whatever you do with "a" in your program/proof, can only
> be done by using "a" (by applying it to arguments), and not by using
> the "fact" that "a" would be computable.
>
> The proof of the pigeon-hole principle offered here doesn't need to
> say what (N->2) is (not). However, there is something to pay attention
> to. We do assume continuity (but only at the meta-level) to show that
> the proof term for the double-negation shift "computes" (rather than
> loops).
>
> Anyway, in general, (N->2) can mean many things, and Agda is
> compatible with many possible meanings for (N->2).
>
> My private meaning of (N->2) is "all boolean sequences".
>
> However, my proof in Agda is written in such a way that I don't reveal
> my private meaning to you or to anybody.
>
> You can use any meaning you like, provided it is compatible with the
> rules of type theory. When you or I compute a closed term of natural
> numbers type (possibly containing subterms of type (N->2)), we will
> get the same result, independently of whatever private maning we have
> for the type formers, in particular (N->2).
>
> But one thing is clear: you cannot prove in Agda that any hypothetical
> element of (N->2) is computable. You can if, you wish, take this as
> your private interpretation of (N->2).
>
> (The subtle thing about the double-negation shift used in this
> particular application is that it restricts the possible private
> interpretations of e.g. (N->2)->N. But this is another story (told in
> the publications).)
>
> Best,
> Martin