# Library Coq.Logic.ClassicalFacts

Some facts and definitions about classical logic
1. Propositional degeneracy = excluded-middle + propositional extensionality
2. Classical logic and proof-irrelevance
2.1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint
2.2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance
2.3. CIC |- prop. ext. -> proof-irrelevance
2.4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance
2.5. CIC |- excluded-middle -> proof-irrelevance
3. Weak classical axioms
3.1. Weak excluded middle and classical de Morgan law
3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction
3 3. Independence of general premises and drinker's paradox
4. Principles equivalent to classical logic
4.1 Classical logic = principle of unrestricted minimization
4.2 Classical logic = choice of representatives in a partition of bool

# 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)
A weakest form of propositional extensionality: extensionality for provable propositions only

# Classical logic and proof-irrelevance

## 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)

Local Notation inhabited A := A (only parsing).

Lemma prop_ext_A_eq_A_imp_A :
prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.

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

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.

Remark: prop_extensionality can be replaced in lemma ext_prop_fixpoint by the weakest property provable_prop_extensionality.

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

Lemma ext_prop_dep_proof_irrel_gen :
prop_extensionality -> bool_dep_induction -> proof_irrelevance.

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 := eq_refl c1.
Definition BoolP_elim_redr (C:Prop) (c1 c2:C) :
c2 = BoolP_elim C c1 c2 FalseP := eq_refl 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.

End Proof_irrelevance_Prop_Ext_CC.

Remark: prop_extensionality can be replaced in lemma ext_prop_dep_proof_irrel_gen by the weakest property provable_prop_extensionality.

## 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 := eq_refl c1.
Definition boolP_elim_redr (C:Prop) (c1 c2:C) :
c2 = boolP_ind C c1 c2 falseP := eq_refl c2.
Scheme boolP_indd := Induction for boolP Sort Prop.

Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance.

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.

## 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

Let p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
Let b2p b := b1 = b.

Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).

Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A.

Using excluded-middle a second time, we get proof-irrelevance
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 a weak version of proof-irrelevance. This is enough to derive a contradiction from a Set-bound weak excluded middle with an impredicative Set universe.

Section Proof_irrelevance_WEM_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 wem : forall A:Prop, or (~~A) (~ A).

Local Notation NProp := NoRetractToNegativeProp.NProp.
Local Notation El := NoRetractToNegativeProp.El.

Variable B : Prop.
Variables b1 b2 : B.

p2b and b2p form a retract if ~b1=b2

Let p2b (A:NProp) := or_elim (~~El A) (~El A) B (fun _ => b1) (fun _ => b2) (wem (El A)).
Let b2p b : NProp := exist (fun P=>~~P -> P) (~~(b1 = b)) (fun h x => h (fun k => k x)).

Lemma wp2p1 : forall A:NProp, El A -> El (b2p (p2b A)).

Lemma wp2p2 : b1 <> b2 -> forall A:NProp, El (b2p (p2b A)) -> El A.

By Hurkens's paradox, we get a weak form of proof irrelevance.

## 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) := eq_refl (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) := eq_refl (g b).
Scheme or_indd := Induction for or Sort Prop.

Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2.

End Proof_irrelevance_CCI.

The same holds with weak excluded middle. The proof is a little more involved, however.

Section Weak_proof_irrelevance_CCI.

Hypothesis wem : forall A:Prop, ~~A \/ ~ A.

Theorem wem_proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), ~~b1 = b2.

End Weak_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.

# Weak classical axioms

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

## Weak excluded-middle

The weak classical logic based on ~~A \/ ~A is referred to with name KC in [ChagrovZakharyaschev97]. See [SorbiTerwijn11] for a short survey.
[ChagrovZakharyaschev97] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997.
[SorbiTerwijn11] Andrea Sorbi and Sebastiaan A. Terwijn, "Generalizations of the weak law of the excluded-middle", Notre Dame J. Formal Logic, vol 56(2), pp 321-331, 2015.

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

Classical De Morgan's law

Definition classical_de_morgan_law :=
forall A B:Prop, ~(A /\ B) -> ~A \/ ~B.

## 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(2), pp 97-103, 1959.
[Gödel33] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", Ergeb. Math. Koll. 4, pp. 34-38, 1933.
(A->B) \/ (B->A) is equivalent to (C -> A\/B) -> (C->A) \/ (C->B) (proof from [Dummett59])
(A->B) \/ (B->A) is stronger than the weak excluded middle
The weak excluded middle is equivalent to the classical De Morgan's law

## 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.
Independence of general premises is equivalent to the drinker's paradox
Independence of general premises is weaker than (generalized) excluded middle
Remark: generalized excluded middle is preferred here to avoid relying on the "ex falso quodlibet" property (i.e. False -> forall A, A)

# Axioms equivalent to classical logic

## Principle of unrestricted minimization

However, minimization for a given predicate does not necessarily imply decidability of this predicate

## Choice of representatives in a partition of bool

This is similar to Bell's "weak extensional selection principle" in [Bell]
[Bell] John L. Bell, Choice principles in intuitionistic set theory, unpublished.