[Agda] Proof irrelevance and self-realizing formulas

[James McKinna]

Hank,
>
> What I'm picking up from this nice discussion is the difference
> between a proof being computationally uninteresting, and intellectually
> interesting.  I understand that Alex Wilkie has spent a lot of his
> considerable intellectual energy in figuring out whether Wiles' proof
> of Fermat's Last Theorem can be coded in Peano Arithmetic.  Perhaps
> we should put him out of his misery and tell him it is just \x.*,
> and can be written in a very small fragment of PA?
>   

To reiterate an earlier point: proof irrelevance a la Conor Thorsten for 
Wiles would *not* mean that the proof is just \x.*

It means that every proof you might find of Wiles is equal to \x.p, 
where p is "one" of the possible proofs. The term * need *not* be one of 
them (perhaps it is consistent, albeit troubling for decidable 
typechecking, to assert that it is).

But to know any one of such p (and hence all of them, because they would 
then be identified), we need to do more work than simply assert "p=*" 
and let the poor old typechecker try to check whether * has the claimed 
type.

Maybe Andrej's RZ interpretation would allows us to claim that p=* would 
do, but I imagine you still have to know a proposition phi is *true* 
before you can assert that * realises it.

Can we agree to distinguish

P:Prop, p,q:P |- p = q:P

from

P,Q:Prop, p:P, q:Q |- P=Q:Prop

as, respectively "proof irrelevance" and "strong proof irrelevance" (or 
some other terminology). Categorically- (and esp. topos-) minded people 
seem to favour the latter principle (all true propositions are (equal 
to) True) from the former, which is (clearly?!) weaker... and what I 
think we have up till now been discussing (or getting confused about).



James.