# Define logic `clProp` for axiom-free classical logic

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.
```

Edited by Robbert Krebbers