The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Hmm?

Definition Peirce := forall P Q:Prop,

  ((P -> Q) -> P) -> P.

Definition NNPP := forall P:Prop, ~~P -> P.

Definition classic := forall P:Prop, P \/ ~P.

Theorem Peirce_impl_NNPP : Peirce -> NNPP.

Proof.

intros ? P ?.

apply H with (Q := False).

intros.

contradiction.

Qed.

Theorem NNPP_impl_classic : NNPP -> classic.

Proof.

intros ? P.

apply H.

tauto.

Qed.

Theorem classic_impl_Peirce : classic -> Peirce.

Proof.

intros ? P Q.

destruct (H P); destruct (H Q); tauto.

Qed.

Print Assumptions Peirce_impl_NNPP.

Print Assumptions NNPP_impl_classic.

Print Assumptions classic_impl_Peirce.

-- 

Daniel Schepler

On Fri, Apr 18, 2014 at 9:26 AM, Gérard Huet <Gerard.Huet AT inria.fr> wrote:

Le 18 avr. 2014 à 16:54, Daniel Schepler <dschepler AT gmail.com> a écrit :

In this particular case, Peirce's law is easily equivalent to classic
(forall P:Prop, P \/ ~P).  

Actually, it is equivalent only in classical logic. 

In the Skolem cube below, it appears as point aPb, intermediate between 1 (True) and A->B.

Note also Sheffer's stroke A|B between A&B and A+B.

The cube is the implicational algebra obtained as quotient by isomorphism of the objects of the free CCC generated by objects A and B, 

and whose arrows Hom(A,B) may be thought of as the deductions of B from A.

We get hypercubes with more propositional letters, but the structure stays finite, as shown by N. de Bruijn.

GH