Skip to content

Embedding of classical logic in Coq + proof mode support.

Robbert Krebbers requested to merge robbert/clprop into master

This MR defines a new logic clProp that embeds classical logic into Coq. It uses essentially the Gödel-Gentzen translation, so the propositions of clProp are defined as the subset of Prop propositions that are stable under double negation, and the pure, ∨, ∃ connectives of clProp are defined using a double negation.

The logic clProp is a BI, so this MR allows one to use the proof mode to carry out proofs in classical logic, without axioms! For example:

Lemma test_excluded_middle P Q : ⊢ P ∨ ¬P.
Proof.
  iApply clProp.dn; iIntros "#H". iApply "H".
  iRight. iIntros "HP". iApply "H". auto.
Qed.

Lemma test_peirces_law P Q : ((P → Q) → P) ⊢ P.
Proof.
  iIntros "#H". iApply clProp.dn; iIntros "#HnotP". iApply "HnotP".
  iApply "H". iIntros "HP". iDestruct ("HnotP" with "HP") as %[].
Qed.

Merge request reports