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 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 3.4. Relativized independence of general premises and excluded-middle 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 with 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 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.

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)

Classical De Morgan's law

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 (i.e. without the constraint of the premise being negative) version of the Independence of Premises considered in [Troelstra73]. In the context of intuitionistic arithmetic (and actually already in the context of the theory of Boolean values), it generalizes the right distributivity of implication over disjunction (and hence Gödel-Dummett axiom). Note contrastingly that both the usual constrained independence of premises and the right distributivity of implication formula over distributivity with the constraint that the implication is from a negative formula (that is Kreisel-Putnam principle [KreiselPutnam57]) preserve the disjunction property. In the context of predicate logic, the Independence of general premises is however weaker than the right distributivity of implication over disjunction (hence of Gödel-Dummett axiom) since its restriction to a singleton domain makes it collapse to an intuitionistic propositional tautology while right distributivity of implication over disjunction is definitely not intuitionistically propositionally provable (consider the Kripke model with a root node splitting into an node with C and A and an other node with C and B). [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.

The Drinker's paradox [Smullyan78] and its dual (a weak form of indefinite description, see e.g. in [WarrenDienerMcKubreJordens18]) [Smullyan78] What is the Name of this Book? Raymond Smullyan, 1978. [WarrenDienerMcKubreJordens18] The Drinker Paradox and its Dual, Louis Warren and Hannes Diener and Maarten McKubre-Jordens, 2018, unpublished.

Independence of general premises is equivalent to the dual drinker's paradox

Independence of general premises is a consequence of (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)

Using subtypes to relativize the domain, independence of general premises is equivalent to excluded-middle in the theory of Boolean values (see Kirst and Zeng, 2024)

Similarly, using subtypes, drinker's paradox on Boolean values implies excluded-middile

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.