The Coq mailing list

[Dominik Kirst <kirst AT ps.uni-saarland.de>]

Dear Coq community,

studying the proof in the standard library (https://coq.inria.fr/library/Coq.Logic.Berardi.html) that excluded middle (XM) implies proof irrelevance (PI), I found that the assumption of XM can be weakened to (logically) decidable equality of propositions (DEP). I have attached a short Coq script which simplifies and strengthens the original idea by Barbanera and Berardi (1996) accordingly. Has this fact been known before and is there work on related ideas? I have only found the overview of propositions independent from Coq in the wiki (https://github.com/coq/coq/wiki/The-Logic-of-Coq) where the implication from decidable equality to proof irrelevance is missing.

The proof structure is to first derive uniqueness of identity proofs (UIP) for propositions from DEP following Hedberg (1998). Using UIP and DEP, every inhabited proposition X admits a surjection U -> U -> X, where U := forall Y, Y -> X.

Hence every function X -> X has a fixed-point (Lawvere). So in particular negation on an inductive proposition Bool with two constructors T and F has a fixed-point, hence T = F, which implies PI. The proof in the script is a more direct and shorter version directly starting from the inductive proposition Bool and inlining the fixed-point theorem.

The trick for defining the inverse (U -> X) -> U is to take h : U -> X and Y : Prop and do a case analysis whether Y = U. If so, one returns h (transported along the equality Y = U which must be reflexivity), if not, any dummy value will do. Interestingly, this insight generalises to other impredicative type theories, in the sense that adding a combinator for type casts allows to derive a fixed-point combinator for inhabited types (cf. Harper & Mitchel (1999)).

Kind regards,

Dominik

-----------------------------------------
Programming Systems Lab
Saarland University
http://www.ps.uni-saarland.de/~kirst/

Attachment: signature.asc
Description: Message signed with OpenPGP