The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Coq.Logic.ClassicalFacts shows that excluded middle (LEM) implies proof irrelevance.  I'm working with a form of proof relevance, but would still like some alternative to LEM - which would allow me to have "forall P, P \/ something else about P" that would still form an excluded middle in that both sides of the "\/" could not be true at the same time.  Because, it looks like if I can have such a thing, then I can get the benefits of proof irrelevance without full proof irrelevance:  It would allow me to easily find for any arbitrary Prop P, a P' such that P <-> P' and P' is irrelevant (forall p q : P', p = q).  As pointed out in the "Proof irrelevant Specif?" thread, coincidentally, this is already possible in Coq without any axioms for all P that are type-decidable ({P}+{~P}) - because that allows a version of P that is a boolean predicate.  The form of proof relevance I'm working with makes it the case for any P that is prop-decidable (P \/ ~P : locally LEM).  This last bit I'm looking for would make it the case for all P period.

The first thing I though of was "forall P, P \/ (P \/ ~P -> ~P)".  Interestingly, this is not a tautology in Coq (at least tauto doesn't think so), but it seems like it's just stating the obvious.  Could it be possible that "forall P, P \/ (P \/ ~P -> ~P)" does not imply proof irrelevance?  If so, then it's just what I need.

Otherwise, there is an infinite regress of these:

Fixpoint nlem(n : nat)(P : Prop) :=
P \/ (match n with
      | 0 => True
      | S m => nlem m P
      end -> ~P).

Arguments nlem : simpl nomatch.

Lemma nlem0_is_lem : (forall P, nlem 0 P) <-> (forall P, P \/ ~P).
Proof.
  cbn. split; intros H P.
  all: specialize (H P); tauto.
Qed.

Lemma nlem1_is_ : (forall P, nlem 1 P) <-> (forall P, P \/ (P \/ ~P -> ~P)).
Proof.
  cbn. split; intros H P.
  all: specialize (H P); tauto.
Qed.

Lemma nlem_inc : forall n P, nlem n P -> nlem (S n) P.
Proof.
  cbn. destruct n.
  - cbn in *. tauto.
  - destruct n. all: cbn in *; tauto.
Qed.

If not "nlem 1 P", what about "nlem n P" for some high enough n?

As it turns out, I really only need to claim the existence of some arbitrary "something else about P":

Axiom lemlike : forall (P:Prop), exists (Q:Prop), (P \/ Q) /\ (P /\ Q -> False).

Might that be safe enough (not imply proof irrelevance)?

-- Jonathan