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

prop_extensionality asserts that equivalent formulas are equal

excluded_middle asserts that we can reason by case on the truth or falsity of any formula

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)

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

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.

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.

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.

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

p2b and b2p form a retract if ~b1=b2

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 wih an impredicative Set universe.

p2b and b2p form a retract if ~b1=b2

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.

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

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.

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)

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.

(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

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.