[Agda] Proof irrelevance and self-realizing formulas

[Thorsten Altenkirch]

Hi Andrej,

it is always fun to argue with you :-)

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

So in Type Theory it is a definable notion (using equality) what is  
the point of having it as a primitive notion?

>
>> I think you calculate a realizer not a proof.
>
> I think so, too. Perhaps the conclusion is that there is life after
> type theory.

To me it seems rather like life *before* Type Theory. This distinction  
of proofs and programs to me is a relict of classical logic.

> I think that was the point of my MSFP talk in Iceland
> last year, but I did not present it very well.

I think it was an excellent talk and you made your point very well.  
Maybe you should mail the link to your slides here.

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

In my view the BHK interpretation provides a notion of evidence in  
form of a functional program not a realizer.

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

There is a foundational and a pragmatic answer to this question:

Foundational: There are certainly principles which are constructlvely  
valid (i.e. can be realized) which are not intuitionistically valid  
(Markov's principle is another example), i.e. they don't follow from  
the intuitionistic explanation of the connectives. While it may be  
good to know that they are realizable this is not sufficient as  
evidence that we should accept them as ways of reasoning. E.g. it is  
better if one can provide a translation which shows that an  
intuitionistic proof can be interpreted in a non-standard way which  
validates the additional principles. I think this is possible in the  
case of Markov's principle.

Pragmatic: Adding these principles to Type Theory as computations  
would destroy normalisation of open terms. You can certainly add the  
as equational assumptions but this would destroy canonicity (i.e.  
there are terms which don't reduce).

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

No the difference is not in "computation" but in "justification".

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

I think the efficient compilation of Agda programs is an important and  
challenging question. However, I don't think we have to change the  
foundations to achieve this. And indeed proof-irrelevance (i.e. Prop)  
seems a good way to mark computationally irrelevant subterms.

Cheers,
Thorsten

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.