[Agda] Proof irrelevance and self-realizing formulas

[Thorsten Altenkirch]

Hi Andrej,

> Let us temporarily forget the interpretation
>
> "P is proof irrelevant" = "all proofs of P are equal"
>
> because we don't like equality of proofs.

Why?

> An alternative
> interpretation of "P is proof irrelevant" is:
>
> "Anything that can be computed using a proof p : P, can also be
> computed without it."
>
> The extreme case of this is that an inhabitant of P can be computed
> without using p, i.e., an inhabitant of P can be constructed out of
> thin air, provided P has inhabitants.

How do we explain that we are using the fact that p has inhabitants  
w.o. looking at them?

I mean this is exactly what is achieved by saying P has at most one  
proof, hence there is no information in knowing that proof.

> Just to make discussion less
> prone to misunderstanding let us not use the phrase "proof
> irrelevant". Call a proposition P "self-realizing" if an inhabitant of
> P can be computed, provided one exists.
>
> Self-realizing propositions are closed under false, truth,
> conjunction, universal quantification and implication.

Indeed, the same holds for "having at most one inhabitant".

> Furthermore,
> decidable propositions are self-realizing. A function rz computing a
> proof of a self-realizing proposition can be defined as follows (it
> takes an environment mapping free variables to their values and a
> proposition):
>
> rz env false = do some magic, this can't happen
> rz env true = *
> rz env (p and q) = (rz env p, rz env q)
> rz env (forall x, p) = lambda x', rz ((x,x')::env) p
> rz env (p -> q) = lambda _, rz env q

I think you calculate a realizer not a proof.

> Please excuse my non-Agda notation. If p : A -> Prop is a decidable
> proposition and d inhabits forall x : A, p x or not (p x) then
>
> rz env (p t) =
> match d (eval env t) with
> Left r -> r
> Right _ -> "not (p x)" cannot happen, do some magic
>
> So we have covered Pi01 propositions. I am being pretty vague here, I
> hope you can see what the idea is. Perhaps an example can help.
>
> Goldbach's conjecture is of the form:
>
> forall n : nat, exists j, k <= n, prime j /\ prime k /\ 2 * n + 4 =  
> j  + k.
>
> The inner "exists" is decidable. Let check_goldbach be the obvious
> algorithm which takes n and looks for prime j, k <= n such that j + k
> = 2 * n + 4. Now, if Goldbach's conjecture has any inhabitants, then
>
> lambda n : nat, check_goldbach n
>
> inhabits it as well.

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

>
> But I don't know if Agda can deal with this sort of thinking (which
> comes from realizability). It seems to me that some meta-level support
> is needed (i.e., in the Agda engine), especially for the "do some
> magic" part above.

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

>
> Am I making any sense to you?

It seems to me that realizability is based on the distinction of  
proofs and programs, while the BHK semantics suggests that they should  
be identified. Leading to Type Theory. Why should one give this up?

Thorsten

>
>
> Andrej
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


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.