[Agda] Proof irrelevance and self-realizing formulas

[Andrej Bauer]

On Thu, May 28, 2009 at 1:13 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
> How do we explain that we are using the fact that p has inhabitants w.o.
> looking at them?

This would probably have to be a primitive notion (hence my claim that
you need support at the meta-level).

> I think you calculate a realizer not a proof.

I think so, too. Perhaps the conclusion is that there is life after
type theory. I think that was the point of my MSFP talk in Iceland
last year, but I did not present it very well. I never understood why
the BHK interpretation has to assume that there are no other forms of
computation apart from realizers of proofs in intuitionistic logic.
For example, why isn't the fan functional (a realizer for Brouwer's
fan theorem from which compactness of [0,1] follows) a "good"
computation? It's certainly useful, as Martin Escardo has been
showing.

> Indeed, and this is certainly not a *proof* because it doesn't tell us why
> Goldbach;s conjecture is true.

I agree it's not a proof. On the other hand, the computational content
of Goldbach's conjecture is void.  If I gave Thorsten a constructive
proof of Goldbach's conjecture and I gave Connor a classical proof,
could Thorsten compute more than Connor? So I am not sure proofs
should be identified with (terminating) computations.

> Not sure about Agda, but I don't see the advantahe.

The advantage of having "proof irrelevance" as a basic notion is that
the resulting system would be more expressive. For example,  we could
express the fact that certain parts of a proof are "computationally
boring". Perhaps Agda already has a way of erasing the boring part of
an extracted realizer/proof? (I readily admit I know very little about
Agda, but I would like to learn more.)

With kind regards,

Andrej