The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Mukesh,

Some ideas:

1: formalize the syntax of CoC explicitly, and then show that a CoC proof of Peirce's law would let you do impossible things like decide the truth of all propositions.

2: show that Pierce's law implies some other principle whose non-provability you already believe in (maybe excluded middle for example).

3: show that Pierce's law contradicts some well-known non-constructive principle such as parametricity (e.g., there is only one inhabitant of (forall A, A -> A), extensionally) or univalence, whose admissibility you also believe in.

    Cheers,

Li-yao

On 2023-10-06 5:11 PM, mukesh tiwari wrote:

Hi everyone,

This question is just out of curiosity. I understand that Peirce's law is not provable in Coq (constructive logic) 
(I tried it in Coq and reached a point where it was impossible to construct an element of type Q from the context). 
I am wondering if there is a formal way to say what is and what is not provable in Coq. 


Best, 
Mukesh 

Require Import List Utf8.
Import Notations.


Lemma peirce_law : 
  ∀ (P Q : Prop), ((P -> Q) -> P) -> P.
Proof.
  refine
    (λ P Q f, f (λ p,  _ )).
  (* There is no way I can construct 
  an element of Q from the given context:
  P, Q: Prop
  f: (P → Q) → P
  p: P
  *)