The Coq mailing list

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

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