# Library Coq.Logic.ClassicalFacts

``` ```

## Some facts and definitions about classical logic

A. Propositional degeneracy = excluded-middle + propositional extensionality

B. Classical logic and proof-irrelevance

B. 1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint

B. 2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance

B. 3. CIC |- prop. ext. -> proof-irrelevance

B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance

B. 5. CIC |- excluded-middle -> proof-irrelevance

C. Weak classical axioms

C. 1. Weak excluded middle

C. 2. Gödel-Dummet axiom and right distributivity of implication over disjunction

C. 3. Independence of general premises and drinker's paradox

``` ```

### A. Prop degeneracy = excluded-middle + prop extensionality

``` ```
i.e. ```(forall A, A=True \/ A=False) <-> (forall A, A\/~A) /\ (forall A B, (A<->B) -> A=B)```
``` ```
`prop_degeneracy` (also referred to as propositional completeness) asserts (up to consistency) that there are only two distinct formulas
``` Definition prop_degeneracy := forall A:Prop, A = True \/ A = False. ```
`prop_extensionality` asserts that equivalent formulas are equal
``` Definition prop_extensionality := forall A B:Prop, (A <-> B) -> A = B. ```
`excluded_middle` asserts that we can reason by case on the truth or falsity of any formula
``` Definition excluded_middle := forall A:Prop, A \/ ~ A. ```
We show `prop_degeneracy <-> (prop_extensionality /\ excluded_middle)`
``` Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality. Proof. intros H A B [Hab Hba]. destruct (H A); destruct (H B).   rewrite H1; exact H0.   absurd B.     rewrite H1; exact (fun H => H).     apply Hab; rewrite H0; exact I.   absurd A.     rewrite H0; exact (fun H => H).     apply Hba; rewrite H1; exact I.   rewrite H1; exact H0. Qed. Lemma prop_degen_em : prop_degeneracy -> excluded_middle. Proof. intros H A. destruct (H A).   left; rewrite H0; exact I.   right; rewrite H0; exact (fun x => x). Qed. Lemma prop_ext_em_degen :  prop_extensionality -> excluded_middle -> prop_degeneracy. Proof. intros Ext EM A. destruct (EM A).   left; apply (Ext A True); split;    [ exact (fun _ => I) | exact (fun _ => H) ].   right; apply (Ext A False); split; [ exact H | apply False_ind ]. Qed. ```

### B. Classical logic and proof-irrelevance

``` ```

#### B. 1. CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint

``` ```
We successively show that:

`prop_extensionality` implies equality of `A` and `A->A` for inhabited `A`, which implies the existence of a (trivial) retract from `A->A` to `A` (just take the identity), which implies the existence of a fixpoint operator in `A` (e.g. take the Y combinator of lambda-calculus)
``` Definition inhabited (A:Prop) := A. Lemma prop_ext_A_eq_A_imp_A :  prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A. Proof. intros Ext A a. apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ]. Qed. Record retract (A B:Prop) : Prop :=   {f1 : A -> B; f2 : B -> A; f1_o_f2 : forall x:B, f1 (f2 x) = x}. Lemma prop_ext_retract_A_A_imp_A :  prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A). Proof. intros Ext A a. rewrite (prop_ext_A_eq_A_imp_A Ext A a). exists (fun x:A => x) (fun x:A => x). reflexivity. Qed. Record has_fixpoint (A:Prop) : Prop :=   {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}. Lemma ext_prop_fixpoint :  prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A. Proof. intros Ext A a. case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2. exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))). intro f. pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *. rewrite (g1_o_g2 (fun x:A => f (g1 x x))). reflexivity. Qed. ```

#### B. 2. CC |- prop_ext /\ dep elim on bool -> proof-irrelevance

``` ```
`proof_irrelevance` asserts equality of all proofs of a given formula
``` Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. ```
Assume that we have booleans with the property that there is at most 2 booleans (which is equivalent to dependent case analysis). Consider the fixpoint of the negation function: it is either true or false by dependent case analysis, but also the opposite by fixpoint. Hence proof-irrelevance.

We then map equality of boolean proofs to proof irrelevance in all propositions.
``` Section Proof_irrelevance_gen. Variable bool : Prop. Variable true : bool. Variable false : bool. Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C. Hypothesis   bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true. Hypothesis   bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false. Let bool_dep_induction :=   forall P:bool -> Prop, P true -> P false -> forall b:bool, P b. Lemma aux : prop_extensionality -> bool_dep_induction -> true = false. Proof. intros Ext Ind. case (ext_prop_fixpoint Ext bool true); intros G Gfix. set (neg := fun b:bool => bool_elim bool false true b). generalize (refl_equal (G neg)). pattern (G neg) at 1 in |- *. apply Ind with (b := G neg); intro Heq. rewrite (bool_elim_redl bool false true). change (true = neg true) in |- *; rewrite Heq; apply Gfix. rewrite (bool_elim_redr bool false true). change (neg false = false) in |- *; rewrite Heq; symmetry in |- *;  apply Gfix. Qed. Lemma ext_prop_dep_proof_irrel_gen :  prop_extensionality -> bool_dep_induction -> proof_irrelevance. Proof. intros Ext Ind A a1 a2. set (f := fun b:bool => bool_elim A a1 a2 b). rewrite (bool_elim_redl A a1 a2). change (f true = a2) in |- *. rewrite (bool_elim_redr A a1 a2). change (f true = f false) in |- *. rewrite (aux Ext Ind). reflexivity. Qed. End Proof_irrelevance_gen. ```
In the pure Calculus of Constructions, we can define the boolean proposition bool = (C:Prop)C->C->C but we cannot prove that it has at most 2 elements.
``` Section Proof_irrelevance_Prop_Ext_CC. Definition BoolP := forall C:Prop, C -> C -> C. Definition TrueP : BoolP := fun C c1 c2 => c1. Definition FalseP : BoolP := fun C c1 c2 => c2. Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2. Definition BoolP_elim_redl (C:Prop) (c1 c2:C) :   c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1. Definition BoolP_elim_redr (C:Prop) (c1 c2:C) :   c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2. Definition BoolP_dep_induction :=   forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b. Lemma ext_prop_dep_proof_irrel_cc :  prop_extensionality -> BoolP_dep_induction -> proof_irrelevance. Proof   ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl     BoolP_elim_redr. End Proof_irrelevance_Prop_Ext_CC. ```

#### B. 3. CIC |- prop. ext. -> proof-irrelevance

``` ```
In the Calculus of Inductive Constructions, inductively defined booleans enjoy dependent case analysis, hence directly proof-irrelevance from propositional extensionality.
``` Section Proof_irrelevance_CIC. Inductive boolP : Prop :=   | trueP : boolP   | falseP : boolP. Definition boolP_elim_redl (C:Prop) (c1 c2:C) :   c1 = boolP_ind C c1 c2 trueP := refl_equal c1. Definition boolP_elim_redr (C:Prop) (c1 c2:C) :   c2 = boolP_ind C c1 c2 falseP := refl_equal c2. Scheme boolP_indd := Induction for boolP Sort Prop. Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance. Proof   fun pe =>     ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl       boolP_elim_redr pe boolP_indd. End Proof_irrelevance_CIC. ```
Can we state proof irrelevance from propositional degeneracy (i.e. propositional extensionality + excluded middle) without dependent case analysis ?

Berardi `[Berardi90]` built a model of CC interpreting inhabited types by the set of all untyped lambda-terms. This model satisfies propositional degeneracy without satisfying proof-irrelevance (nor dependent case analysis). This implies that the previous results cannot be refined.

`[Berardi90]` Stefano Berardi, "Type dependence and constructive mathematics", Ph. D. thesis, Dipartimento Matematica, Università di Torino, 1990.
``` ```

#### B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance

``` ```
This is a proof in the pure Calculus of Construction that classical logic in `Prop` + dependent elimination of disjunction entails proof-irrelevance.

Reference:

`[Coquand90]` T. Coquand, "Metamathematical Investigations of a Calculus of Constructions", Proceedings of Logic in Computer Science (LICS'90), 1990.

Proof skeleton: classical logic + dependent elimination of disjunction + discrimination of proofs implies the existence of a retract from `Prop` into `bool`, hence inconsistency by encoding any paradox of system U- (e.g. Hurkens' paradox).
``` Require Import Hurkens. Section Proof_irrelevance_EM_CC. Variable or : Prop -> Prop -> Prop. Variable or_introl : forall A B:Prop, A -> or A B. Variable or_intror : forall A B:Prop, B -> or A B. Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C. Hypothesis   or_elim_redl :     forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A),       f a = or_elim A B C f g (or_introl A B a). Hypothesis   or_elim_redr :     forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B),       g b = or_elim A B C f g (or_intror A B b). Hypothesis   or_dep_elim :     forall (A B:Prop) (P:or A B -> Prop),       (forall a:A, P (or_introl A B a)) ->       (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b. Hypothesis em : forall A:Prop, or A (~ A). Variable B : Prop. Variables b1 b2 : B. ```
`p2b` and `b2p` form a retract if `~b1=b2`
``` Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A). Definition b2p b := b1 = b. Lemma p2p1 : forall A:Prop, A -> b2p (p2b A). Proof.   unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);    unfold b2p in |- *; intros.   apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)).   destruct (b H). Qed. Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A. Proof.   intro not_eq_b1_b2.   unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);    unfold b2p in |- *; intros.   assumption.   destruct not_eq_b1_b2.   rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H.   assumption. Qed. ```
Using excluded-middle a second time, we get proof-irrelevance
``` Theorem proof_irrelevance_cc : b1 = b2. Proof.   refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.     trivial.   apply (paradox B p2b b2p (p2p2 H) p2p1). Qed. End Proof_irrelevance_EM_CC. ```
Remark: Hurkens' paradox still holds with a retract from the _negative_ fragment of `Prop` into `bool`, hence weak classical logic, i.e. `forall A, ~A\/~~A`, is enough for deriving proof-irrelevance.
``` ```

#### B. 5. CIC |- excluded-middle -> proof-irrelevance

``` ```
Since, dependent elimination is derivable in the Calculus of Inductive Constructions (CCI), we get proof-irrelevance from classical logic in the CCI.
``` Section Proof_irrelevance_CCI. Hypothesis em : forall A:Prop, A \/ ~ A. Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C)   (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a). Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C)   (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b). Scheme or_indd := Induction for or Sort Prop. Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2. Proof   proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl     or_elim_redr or_indd em. End Proof_irrelevance_CCI. ```
Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with `bool` in `Set` and since `~true=false` for `true` and `false` in `bool` from `Set`, we get the inconsistency of `em : forall A:Prop, {A}+{~A}` in the Set-impredicative CCI.
``` ```

### C. Weak classical axioms

``` ```
We show the following increasing in the strength of axioms:
• weak excluded-middle
• right distributivity of implication over disjunction and Gödel-Dummet axiom
• independence of general premises and drinker's paradox
• excluded-middle
``` ```

#### C. 1. Weak excluded-middle

``` ```
The weak classical logic based on `~~A \/ ~A` is referred to with name KC in {`ChagrovZakharyaschev97`]

`[ChagrovZakharyaschev97]` Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997.
``` Definition weak_excluded_middle :=   forall A:Prop, ~~A \/ ~A. ```
The interest in the equivalent variant `weak_generalized_excluded_middle` is that it holds even in logic without a primitive `False` connective (like Gödel-Dummett axiom)
``` Definition weak_generalized_excluded_middle :=   forall A B:Prop, ((A -> B) -> B) \/ (A -> B). ```

#### C. 2. Gödel-Dummett axiom

``` ```
`(A->B) \/ (B->A)` is studied in `[Dummett59]` and is based on `[Gödel33]`.

`[Dummett59]` Michael A. E. Dummett. "A Propositional Calculus with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol 24 No. 2(1959), pp 97-103.

`[Gödel33]` Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", Ergeb. Math. Koll. 4 (1933), pp. 34-38.
``` Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A). Lemma excluded_middle_Godel_Dummett : excluded_middle -> GodelDummett. Proof. intros EM A B. destruct (EM B) as [HB|HnotB].   left; intros _; exact HB.   right; intros HB; destruct (HnotB HB). Qed. ```
`(A->B) \/ (B->A)` is equivalent to `(C -> A\/B) -> (C->A) \/ (C->B)` (proof from `[Dummett59]`)
``` Definition RightDistributivityImplicationOverDisjunction :=   forall A B C:Prop, (C -> A\/B) -> (C->A) \/ (C->B). Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction :   GodelDummett <-> RightDistributivityImplicationOverDisjunction. Proof. split.   intros GD A B C HCAB.   destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC;     destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption.   intros Distr A B.   destruct (Distr A B (A\/B)) as [HABA|HABB].     intro HAB; exact HAB.     right; intro HB; apply HABA; right; assumption.     left; intro HA; apply HABB; left; assumption. Qed. ```
`(A->B) \/ (B->A)` is stronger than the weak excluded middle
``` Lemma Godel_Dummett_weak_excluded_middle :   GodelDummett -> weak_excluded_middle. Proof. intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA].   left; intro HnotA; apply (HnotA (HnotAA HnotA)).   right; intro HA; apply (HAnotA HA HA). Qed. ```

#### C. 3. Independence of general premises and drinker's paradox

``` ```
Independence of general premises is the unconstrained, non constructive, version of the Independence of Premises as considered in `[Troelstra73]`.

It is a generalization to predicate logic of the right distributivity of implication over disjunction (hence of Gödel-Dummett axiom) whose own constructive form (obtained by a restricting the third formula to be negative) is called Kreisel-Putnam principle `[KreiselPutnam57]`.

`[KreiselPutnam57]`, Georg Kreisel and Hilary Putnam. "Eine Unableitsbarkeitsbeweismethode für den intuitionistischen Aussagenkalkül". Archiv für Mathematische Logik und Graundlagenforschung, 3:74- 78, 1957.

`[Troelstra73]`, Anne Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.
``` Notation Local "'inhabited' A" := A (at level 10, only parsing). Definition IndependenceOfGeneralPremises :=   forall (A:Type) (P:A -> Prop) (Q:Prop),     inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x. Lemma   independence_general_premises_right_distr_implication_over_disjunction :   IndependenceOfGeneralPremises -> RightDistributivityImplicationOverDisjunction. Proof. intros IP A B C HCAB. destruct (IP bool (fun b => if b then A else B) C true) as ([|],H).   intro HC; destruct (HCAB HC); [exists true|exists false]; assumption.   left; assumption.   right; assumption. Qed. Lemma independence_general_premises_Godel_Dummett :   IndependenceOfGeneralPremises -> GodelDummett. Proof. destruct Godel_Dummett_iff_right_distr_implication_over_disjunction. auto using independence_general_premises_right_distr_implication_over_disjunction. Qed. ```
Independence of general premises is equivalent to the drinker's paradox
``` Definition DrinkerParadox :=   forall (A:Type) (P:A -> Prop),   inhabited A -> exists x, (exists x, P x) -> P x. Lemma independence_general_premises_drinker :   IndependenceOfGeneralPremises <-> DrinkerParadox. Proof. split.   intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx.   intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx).     exists x; intro HQ; apply (Hx (H HQ)). Qed. ```
Independence of general premises is weaker than (generalized) excluded middle
``` Definition generalized_excluded_middle :=   forall A B:Prop, A \/ (A -> B). Lemma excluded_middle_independence_general_premises :   generalized_excluded_middle -> DrinkerParadox. Proof. intros GEM A P x0. destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot].   exists x; intro; exact Hx.   exists x0; exact Hnot. Qed. ```