The Coq mailing list

[Meven Lennon-Bertrand <mgapb2 AT cam.ac.uk>]

    Hi Mukesh,
    
    One thing that you can do is use normalisation: by normalisation, if
    there is any proof at all, there must be a proof in normal form. But
    the proof that you tried and failed to complete basically
    demonstrates there is no such normal form. So the statement is not
    provable.
    
    More generally, the way to demonstrate formally that a statement in
    Coq is not provable is to construct a model where the interpretation
    of the statement is empty. In the case above, this model is the very
    syntactic one of normalisation, but there are other, more "semantic"
    instances, for instance set-theoretic models, or the ones given by
    homotopy-based ideas.
    
    Hope this helps,
Meven LENNON-BERTRAND
Postdoc – Computer Lab, University of Cambridge
www.meven.ac

On 06/10/2023 17:11, 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
  *)