Library Coq.Logic.ClassicalFacts

Some facts and definitions about classical logic
Table of contents:
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
3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction
3 3. Independence of general premises and drinker's paradox

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.
    bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true.
    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.
[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.
    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).
    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).
    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).

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

Using excluded-middle a second time, we get proof-irrelevance
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.

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.

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
  • 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]
[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).

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.

(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

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

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.

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)