[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

On 25/11/12 22:11, Peter Divianszky wrote:
> So you use a variant of the infinite pigeonhole principle in which ₂ℕ is
> computable.
> This is fine, I am impressed that you have got computational content
> from a very classical proof.

Thanks for the compliment, which should apply not to me, but to the
logicians who came up with such ideas and techniques before me. My
tiny contribution here is to show how these ideas and techniques can
be materialized in Agda, in a syntax-free treatment (I don't need to
perform syntactical transformations of classical proofs into
constructive proofs like in the usual logical treatment).

> 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