Classical vs. Constructive Logic

We have seen that it is not possible to test whether a proposition p is true or not by defining a Kind function. You may be surprised to find out that a similar restriction applies to proofs! In other words, the following principle of intuitive reasoning is not derivable in Kind:

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
}

To understand operationally why this is the case, recall that to prove a statement of the form Either p q, we use the pattern matches Left and Right, which require knowing which side of the disjunction is true. But the universally quantified proposition p in Excluded_middle is an arbitrary proposition about which we know nothing. We do not have enough information to choose which of Left or Right to apply, just as Kind does not have enough information to mechanically decide whether p is true or not within a function.

However, if we know that p is reflected in some Boolean term b, determining whether it is true or not is trivial: we just check the value of b.

#![allow(unused)]
fn main() {
Restricted_excluded_middle <p> <q> (b: Bool)(e: Equivalence p (Equal b Bool.true)) : Either p (Not p) 
Restricted_excluded_middle p q Bool.true  (Equivalence.new pb bp) = Either.left (bp Equal.refl)
Restricted_excluded_middle p q Bool.false (Equivalence.new pb bp) = Either.right (Empty.absurd (Not_implies_our_not pb))
}

In particular, the third excluded is valid for equations n = m, between natural numbers n and m.

#![allow(unused)]
fn main() {
Restricted_excluded_middle_eq (n: Nat) (m: Nat) : Either (Equal n m) (Not (Equal n m))
Restricted_excluded_middle_eq n m = ?

To_reme (n: Nat) (m: Nat) (e: Equal n m) : Equal (Nat.equal n m) Bool.true
To_reme Nat.zero Nat.zero e         = Equal.refl
To_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) (Nat.succ m) e = To_reme n m (Succ_injective n m e)

From_reme (n: Nat) (m: Nat) (e: Equal (Nat.equal n m) Bool.true) : Equal n m
From_reme Nat.zero Nat.zero e         = Equal.refl
From_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) (Nat.succ m) e = Equal.apply (x => Nat.succ x) (From_reme n m e)
}

It may seem strange that the principle of the excluded middle is not available by default in Kind; after all, any assertion must be true or false. However, there is an advantage in not assuming the principle of the excluded middle: statements in Kind can make stronger claims than the analogous statements in standard mathematics. Notably, if there is a proof in Kind of (Sigma a (x => (p x))), we can explicitly exhibit a value of x for which we can prove p x — in other words, every proof of existence is necessarily constructive. Logics like Kind, which do not assume the principle of the excluded middle, are referred to as constructive logics. More conventional logical systems, such as ZFC, in which the principle of the excluded middle is valid for arbitrary propositions, are referred to as classical.

The following example illustrates why assuming the principle of the excluded middle can lead to non-constructive proofs:

Statement: There are irrational numbers a and b, such that a^b is rational.

Proof: It is not difficult to show that the square root of 2 is irrational. If square root of 2 ^ square root of 2 is rational, we can simply take a = b = square root of 2, and we are done .Otherwise, if square root of 2 ^ square root of 2 is irrational, we can take a = square root of 2 ^ square root of 2 and b = square root of 2, since a ^ b = square root of 2 ^ (square root of 2 * square root of 2) = square root of 2 ^ 2 = 2.

Did you notice what happened here? We used the principle of the excluded middle to separately consider the cases where square root of 2 ^ square root of 2 is rational and where it is not, without knowing which one is true! Because of this, we know that such a and b exist, but we cannot determine their actual values (at least, using this line of argument).

As useful as constructive logic is, it has its limitations: there are many statements that can be easily proven in classical logic but have much more complicated constructive proofs, and there are some for which no constructive proof is known! Fortunately, just like the functional extensionality, the principle of the excluded middle is known to be compatible with Kind logic, allowing us to safely add it as an axiom. However, we will not need to do this in this book: the results we cover can be developed entirely within constructive logic at a negligible extra cost.

It takes some practice to understand which proof techniques should be avoided in constructive reasoning, but arguments by contradiction, in particular, are infamous for leading to non-constructive proofs. Here's a typical example: suppose we want to show that there exists an x with some property p, i.e., such that p x. We start by assuming that our conclusion is false; that is Not (Sigma a (x => (p x))). From this premise, it is not difficult to deduce (x: a) -> Not (p x). If we can show that this intermediate fact leads to a contradiction, we arrive at a proof of existence without ever exhibiting a value of x for which p x is true!

The technical failure here, from a constructive standpoint, is that we claim to prove Sigma a (x => (p x)) using a proof o Not (Not (Sigma a (x =>(p x)))). Allowing us to remove double negations from arbitrary statements is equivalent to assuming the excluded middle, as shown in one of the exercises below. Thus, this line of reasoning cannot be encoded in Kind without assuming additional axioms.

Excluded_middle_irrefutable

The consistency of Kind with the general axiom of the excluded middle requires complicated reasoning that cannot be carried out within Kind itself. However, the following theorem implies that it is always safe to assume a decidability axiom (i.e., an instance of the excluded middle) for any specific type p. Why? Because we cannot prove the negation of such an axiom; if we could, we would have both Not (Either p (Not p)) and Not (Not (Either p (Not p))), which is a contradiction.

#![allow(unused)]
fn main() {
Excluded_middle_irrefutable <p> : Not (Not (Either p (Not p)))
Excluded_middle_irrefutable p = ?
}

Not_exists_dist

It is a theorem of classical logic that the following two statements are equivalent:

#![allow(unused)]
fn main() {
Not (Sigma a (k => Not (p k))))
(x : a) -> p x
}

The dist_not_exists theorem above proves one side of this equivalence. Interestingly, the other direction cannot be proven in constructive logic. Your task is to show that it is implied by the excluded middle.

#![allow(unused)]
fn main() {
Not_exists_dist <a> (p: a -> Type) (s: Not (Sigma a (k => Not (p k)))) : (x: a) -> p x
Not_exists_dist a p s = ?
}

where

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
// Excluded_middle p = Confia 
}

Classical_axioms

For those who like a challenge, here's an exercise taken from the book Coq'Art by Bertot and Casteran (p. 123). Each of the following four statements, together with excluded_middle, can be regarded as characterizing classical logic. We cannot prove any of them in Kind, but we can consistently add any one of them as an axiom if we want to work in classical logic.

Prove that all five propositions (these four plus excluded_middle) are equivalent.

#![allow(unused)]
fn main() {
Peirce <p> <q>(pq: (p -> q) -> p) : p

Double_negation_elimination <p> (np: Not (Not p)) : p

De_morgan_not_not <p> <q> (np: Pair (Not p) (Not q)) : Either p q

Implies_to_or <p> <q> (pq: p -> q) : Either (Not p) q
}