[Agda] Proof irrelevance and self-realizing formulas

[Thorsten Altenkirch]

Hi Conor & everybody,

>> If I may also interject, as I'm also far from an expert:
>>
>> There seems to be a school of thought that argues that assigning  
>> "irrelevance"
>> to certain _types_ is wrong-headed in general. Rather, the  
>> correctness of
>> erasing certain terms from the computation (which is, correct me if  
>> I'm wrong,
>> the point of irrelevance) is dependent on how they're used, not  
>> whether their
>> types are in Prop or Set.
>
> There's room for both views. If we're in the business of
> detecting/ensuring absence of computational content, we
> can do so either when there is nothing to see, or when
> we choose not to look.

Indeed. The theory sketched below is closely related to box types as  
described in Bauer and Awodey's paper "Propositions as  
[Types 
]".??????????????????????????????????????????????????????????????????????????? ??"Pro

> It seems plausible, for example, to extend Prop with
>
> Inhabited : Set -> Prop
> witness : (x : X) -> Prf (Inhabited X)
> exploit : (P : Inhabited X -> Prop) ->
>         ((x : X) -> Prf (P (witness x))) ->
>         (i : Inhabited X) -> Prf (P i)
>
> P \/ Q then becomes Inhabited (Prf P + Prf Q) but,
> crucially, one can only exploit inhabitation to
> construct proofs, not values in sets.

And given P : A -> Prop, exists x:A.P x becomes inhabited( Sigma  
x:A.Prf (P x) ).

> It's not clear
> to me whether this is enough to cause the damage that
> Shin managed to code up. Must try to find out: it
> would be terribly interesting if the above is toxic.

It is possible to justify the above using a setoid model where  
"inhabited A" is the setoid with the trivial equality (i.e. the one  
which is alway true). Hence, we should be able to show that this is  
not toxic.

However, if we add for A:Set, B: A -> Set

f : (a:A) -> inhabited (B a)
---------------------------------------
lift f:  inhabited( (a:A) -> B a))

we are in deep water. Why? The rule is not validated by the setoid  
translation, because from the premise we get a function f_set :  
(a:A.set) -> (B a).set but there is no reason to assume that given  a  
~A a' -> f_set a ~Ba f_set a', which is what we need to construct  
(lift f).set.

However, everything is fine, *if* ~A is just equality, because if a =  
a' then trivially _set a ~Ba f_set a'.

I haven't had time to go through Shin's blog post in detail, but if I  
am not mistaken then he is reconstructing Diaconescu's construction.  
Basically to derive excluded middle from "lift" we need to construct a  
very non-trivial setoid A.

lift entails the "propositional" axiom of choice, i.e. give A,B:Set  
and R:A -> B -> Prop

	h : (a:A) -> Prf (exists b:B . R a b)
	---------------------------------------------------------------------------------
	pac h : Prf (exists f : A -> B . inhabited ((a:A) -> Prf (R a (f a))))

using the encoding of exists suggested above. Sorry, maybe there are  
too many Prfs and inhabiteds - here is a more readable variant

	h : (a:A) -> exists b:B.R a b
	---------------------------------------------------
	pac h : exists f:A -> B. (a:A) -> R a (f a)

There is no good reason to accept this principle (unlike the version  
where exists is replaced by Sigma). The premise h says that we are  
have decided to ignore the identity of the witness, while in the  
conclusion we change our mind and decide that we should peek into it  
after all.

Maybe surprising that this lie is not inconsistent after all. But then  
this is what classical logic is all about : you are allowed to lie as  
long as you don't get caught... :-)

Cheers,
Thorsten

P.S. This is related to a discussion on the old epigram mailing list  
in Feb 2007.
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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090530/ebaaba56/attachment.html