The Coq mailing list

[Gérard Huet <Gerard.Huet AT inria.fr>]

What you are toying with in the free Heyting algebra generated by one element (P).

It is not finite, this is Nishimura’s lattice. Your infinite regress is going up this lattice, but True is unreacheable by unions of P’s and ~P’s (in intuitionistic propositional calculus).

P \/ (P \/ ~P -> ~P) is not just stating the obvious, anymore than his sister at the first level ~P->P.

GH 

Le 28 mai 2016 à 17:47, Jonathan Leivent <jonikelee AT gmail.com> a écrit :

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