propositional logic, propositional calculus, intuitionistic, logic, propositional, minimal, constructive, intuitionist, computer, independent, constructive logic, minimal logic, intuitionistic logic, calculus, Glivenko, independence, embedding

Back to title page

2. Propositional Logic

George Boole (1815-1864): "In 1854 he published An investigation into the Laws of Thought, on Which are founded the Mathematical Theories of Logic and Probabilities. Boole approached logic in a new way reducing it to a simple algebra, incorporating logic into mathematics. He pointed out the analogy between algebraic symbols and those that represent logical forms. It began the algebra of logic called Boolean algebra which now finds application in computer construction, switching circuits etc." (according to MacTutor History of Mathematics archive).

See also:

G.Boole. The Calculus of Logic. The Cambridge and Dublin Mathematical Journal, vol. 3 (1848) (available online at http://www.maths.tcd.ie/pub/HistMath/People/Boole/CalcLogic/).

2.1. Proving Formulas Containing Implication only

Let us return to the Exercise 1.4.1(d), where you produced a sequence of 9 formulas proving the following:

d) [L₁, L₂, MP]: A->(A->B) |- A->B.

Did you try the next step - proving of

d') [L₁, L₂, MP]: |- (A->(A->B))->(A->B)?

For proving directly - almost an impossible task!

Now, having deduction theorems, we can greatly simplify the task of proving d), and make the task proving of d') feasible. More precisely - the task of proving that d) and d') are provable. Indeed,

Thus, we have established that A->(A->B), A |- B. Now, by Deduction Theorem 1, [L₁, L₂, MP]: A->(A->B) |- A->B. Let us apply this theorem once more, [L₁, L₂, MP]: |- (A->(A->B))->(A->B).

Note. In fact, we did not prove d) and d'), i.e. we did not produce the corresponding sequences of formulas. We just proved the these sequences do exist! To produce them really, we must apply the algorithm described in the above proof of Deduction Theorem 1 (see also Exercise 1.5.2).

Warning! Be careful when selecting hypotheses. For example, to prove the strange formula (the so-called Peirce's Law) |- ((A->B)->A)->A (it is provable in the classical logic, not in the constructive logic!), you can try proving that (A->B)->A |- A, but not A->B, A |- A. Why? Because, by Deduction Theorem 1, from A->B, A |- A it follows that A->B |- A->A and |- (A->B)->(A->A), or A |- (A->B)->A and |- A->((A->B)->A). Where do you see |- ((A->B)->A)->A here?

Exercise 2.1.1. Prove the following [L₁, L₂, MP]:

a) |- ((A->B)->(A->C))->(A->(B->C)). What does this formula mean?

b) |- (A->B)->((B->C)->(A->C)). What does this formula mean? It's another version of the so-called Law of Syllogism (by Aristotle), or the transitivity property of implication. Explain the difference between this formula and Theorem 1.4.2: A->B, B->C |- A->C.

c) |- (A->(B->C))->(B->(A->C)). What does this formula mean? It's another version of the so-called Premise Permutation Law. Explain the difference between this formula and Exercise 1.4.1(c): A->(B->C) |- B->(A->C).

2.2. Proving Formulas Containing Conjunction

Theorem 2.2.1. a) [L₅, MP] A, B |- A&B,

b) [L₃, L₄, MP]: A&B |- A, A&B |- B.

Let us prove (a).

Now, let us prove (b).

Thus, A&B |- A.

Thus, A&B |- B.

Theorem 2.2.1 allows proving of equivalencies. Let us recall that B<->C is defined as a shortcut for (B->C)&(C->B). Of course, we will call B and C equivalent formulas, iff |- B<->C. For example, by Theorem 1.4.1, [L₁, L₂, MP] |- A->A, hence, [L₁, L₂, L₅, MP] |- (A->A)&(A->A), i.e.

[L₁, L₂, L₅, MP] |- A<->A.

Of course, (a) of the Exercise 2.1.1 is the reverse formula of the axiom L₂. Hence, by Theorem 2.2.1:

[L₁, L₂, L₅, MP] |- (A->(B->C)) <-> ((A->B)->(A->C)).

By (b) and (c) of the Exercise 2.1.1, and Theorem 2.2.1:

[L₁, L₂, L₅, MP] |- (A->(B->C))<->(B->(A->C))

Now, let us prove another form of the law of syllogism, or Theorem 1.4.2 [L₁, L₂, MP]: A->B, B->C |- A->C:

[L₁, L₃, L₄, MP] |- (A->B)&(B->C)->(A->C).

Thus, we have established that (A->B)&(B->C) |- A->C. By Deduction Theorem 1, |- ((A->B)&(B->C))->(A->C).

Exercise 2.2.1. Prove the following [L₁- L₅, MP]:

a) A->B, A->C |- A->B&C. What does it mean?

b) |- (A->B)&(A->C)->(A->B&C). What does it mean?

c) A->B&C |- A->B. What does it mean?

d) A->B&C |- A->C. What does it mean?

e) |- (A->B&C)->(A->B)&(A->C). What does it mean?

Hence,

[L₁- L₅, MP]: |- (A->B&C)<->(A->B)&(A->C).

Now let us prove that conjunction is commutative:

[L₁- L₅, MP]: |- A&B<->B&A.

Thus, we have established that A&B |- B&A. By Deduction Theorem 1, |- A&B->B&A. To prove |- B&A->A&B repeat the above proof.

Exercise 2.2.2..Prove the following [L₁- L₅, MP]:

a) |- A&(B&C)<->(A&B)&C. What does it mean? That conjunction is associative.

b) |- (A->(B->C))<->(A&B->C). What does it mean?

c) |- (A->B)->(A&C->B&C). What does it mean? The converse formula (A&C->B&C)->(A->B) cannot be true. Explain, why.

Let us prove that conjunction is idempotent:

[L₁- L₅, MP]: |- A&A<->A.

|- A&A->A

It's the axiom L₃: B&C->B with B = A, C = A.

|- A->A&A

By Theorem 2.2.1(a) and Deduction Theorem 1.

Theorem 2.2.2. [L₁- L₅, MP]: A |- B<->B&A. What does it mean?

Hence, by Deduction Theorem 1, A |- B->B&A.

Hence, by Deduction Theorem 1, A |- B&A->B.

Exercise 2.2.3. Let us recall that the equivalence connective A<->B is defined as a shortcut for (A->B)&(B->A). Prove the following properties of this connective [L₁- L₅, MP]:

(a) |- A<->A (reflexivity),

(b) |- (A<->B)->(B<->A) (symmetricity),

(c) |- (A<->B)&(B<->C)->(A<->C) (transitivity).

2.3. Proving Formulas Containing Disjunction

Exercise 2.3.1. Prove the following [L₁, L₂, L₆-L₈, MP]:

a) [L₈, MP]: A->C, B->C |- AvB->C. What does it mean?

b) [ L₅, L₆-L₈, MP]: |- AvB<->BvA. What does it mean? That disjunction is commutative.

c) [L₁, L₂, L₅, L₆-L₈, MP]: |- AvA<->A. What does it mean? That disjunction is idempotent.

Exercise 2.3.2. [L₁, L₂, L₈, MP]: If there is a proof of A₁, A₂, ..., A_n, B |- D, and a proof of A₁, A₂, ..., A_n, C |- D, then there is a proof of A₁, A₂, ..., A_n , BvC |- D.

Surprisingly, proving that disjunction is associative requires some sophistication (do not read the proof below, try proving yourself):

[L₁, L₂, L₅, L₆-L₈, MP]: |- Av(BvC)<->(AvB)vC.

The main idea: let us first prove that |- A->Av(BvC), |- B->Av(BvC), |- C->Av(BvC).

Exercise 2.3.3. a) Prove the converse: [L₁, L₂, L₆-L₈, MP]: |- Av(BvC)->(AvB)vC.

b) Prove (use Deduction Theorem 1) that [L₁, L₂, L₆-L₈, MP]: |- (A->B)->(AvC->BvC). What does it mean? The converse formula (AvC->BvC)->(A->B) cannot be true. Explain, why.

c) Prove that [L₁, L₂, L₆-L₈, MP]: |- A->B, C->D |- AvC->BvD. What does it mean?

The following theorem corresponds to the well-known distributive property of (number) addition to multiplication: (a+b)c = ac+bc. Of course, the "dual" distributive property (i.e. - of multiplication to addition) does not hold for numbers: ab+c=(a+c)(b+c) would imply ab+c=ab+ac+bc+cc, c=ac+bc+cc, and, if c<>0, then 1=a+b+c. Still, surprisingly, in logic,

Theorem 2.3.1. Conjunction is distributive to disjunction, and disjunction is distributive to conjunction:

[L₁-L₈, MP]: |- (A&B)vC<->(AvC)&(BvC).
[L₁-L₈, MP]: |- (AvB)&C<->(A&C)v(B&C).

First, let us prove that |- (A&B)vC->(AvC)&(BvC).

Exercise 2.3.4. a) Prove (1) and (2).

b) Do not read the following proof. Try proving yourself.

Now, let us prove the converse: |- (AvC)&(BvC)->(A&B)vC.

Note. The proof below starts with C as a hypothesis. Why not with (AvC)&(BvC)? Because, we will use Deduction Theorem 1 to prove the intermediate formula (6) C->(BvC->(A&B)vC), not the final result!

Now, we must prove that |- (AvB)&C->(A&C)v(B&C).

Exercise 2.3.5. Prove the above (1), (2) and (3).

Finally, we must prove that |- (A&C)v(B&C)->(AvB)&C

Exercise 2.3.6. Prove (4).

2.4. Formulas Containing Negation - Minimal Logic

Theorem 2.4.1. a) [L₁, L₂, L₉, MP]: If A₁, A₂, ..., A_n, B |- C, and A₁, A₂, ..., A_n, B |- ~C, then A₁, A₂, ..., A_n |- ~B. What does it mean?

b) [L₃, L₄, L₉, MP]: |- ~(A&~A). What does it mean? It's the so-called Law of Non-Contradiction.

c) [L₁, L₂, L₉, MP]: A, ~B |- ~(A->B). Or, [L₁-L₄, L₉, MP]: |- A&~B -> ~(A->B). What does it mean?

d) |- [L₁, L₂, L₉, MP]: (A->~A)->~A. What does it mean?

Attention: non-constructive reasoning! In Section 2.6, we will use the classical logic [L₁-L₁₁, MP] to prove the converse formula of (c): ~(A->B)->A&~B, i.e. the equivalence ~(A->B)<->A&~B. This formula cannot be proved in the constructive logic [L₁-L₁₀, MP] (see Section 2.8).

Let us prove (a). Indeed, by Deduction Theorem 1, A₁, A₂, ..., A_n |- B->C, and A₁, A₂, ..., A_n |- B->~C. Let us continue this proof by adding the axiom L₉: (B->C)->((B->~C)->~B) as the next step. After this, by MP, we obtain ~B. Q.E.D.

For the proof of (b) see Exercise 1.4.2 (e).

Let us prove (c): A, ~B, A->B |- B, and A, ~B, A->B |- ~B, hence, by (a), A, ~B |-~( A->B).

Exercise 2.4.1. a) Prove the second version of (c), i.e. [L₁-L₄, L₉, MP]: |- A&~B -> ~(A->B).

b) Prove (d).

Theorem 2.4.2. [L₁, L₂, L₉, MP]: |- (A->B)->(~B->~A). What does it mean? It's the so-called Contraposition Law.

Thus, by Deduction Theorem 1, |- (A->B)->(~B->~A).

Note. The following form of Theorem 2.4.2 is called Modus Tollens:

[L₁, L₂, L₉, MP]: |- A->B, ~B |- ~A.

Attention: non-constructive reasoning! In Section 2.6, we will use the classical logic [L₁-L₁₁, MP] to prove the converse formula (~B->~A)->(A->B), i.e. the equivalence (A->B)<->(~B->~A). We will see also that these formulas cannot be proved in the constructive logic [L₁-L₁₀, MP] (see Section 2.8).

Exercise 2.4.2. Verify that, in our axiom system, the Law of Non-Contradiction and the Contraposition Law could be used instead of the axiom L₉. More precisely: prove L₉ in the logic [L₁-L₈, Law of Non-Contradiction, Contraposition Law, MP].

Theorem 2.4.3. [L₁-L₉, MP]: |- (A->~B)<->(B->~A). What does it mean?

First we prove that |- (A->~B)->(B->~A).

Thus, by Deduction Theorem 1, |- (A->~B)->(B->~A). By swapping A and B we obtain the converse formula: |- (B->~A)->(A->~B). Q.E.D.

Attention: non-constructive reasoning! Warning! The (very similar to Theorem 2.4.3) formula (~A->B)<->(~B->A) can be proved only in the classical logic!

Theorem 2.4.4. [L₁, L₂, L₉, MP]: |- A->~~A. What does it mean?

Indeed, let us take A = ~A and B = A in Theorem 2.4.3, |- (~A->~A)<->(A->~~A). By Theorem 1.4.1, [L₁, L₂, MP]: |- ~A->~A, hence, |- A->~~A. Q.E.D.

Attention: non-constructive reasoning! In Section 2.6, we will use the classical logic [L₁-L₁₁, MP] to prove the converse formula |- ~~A->A, i.e. the equivalence |- ~~A<->A (the so-called Double Negation Law). We will see also (Section 2.8) that these formulas cannot be proved in the constructive logic [L₁-L₁₀, MP].

Still, in the minimal logic we can prove (Brouwer, 1923?):

Theorem 2.4.5. [L₁-L₉, MP]: |- ~~~A<->~A. What does it mean?

Indeed, by Theorem 2.4.4, |- ~A->~~~A. By the Contraposition Law (Theorem 2.4.2), |- (A->~~A)->(~~~A->~A). Hence, by Theorem 2.4.4, |- ~~~A->~A. Q.E.D.

Theorem 2.4.5 (and some of the following formulas in this and in the next section containing double negations) may seem uninteresting to people believing unconditionally in the equivalence ~~A<->A. Still, it seems interesting (at least - for a mathematician) to obtain a general characterization of logical formulas that do not depend on the Law of the Excluded Middle. In Section 2.7 we will use these formulas to prove the elegant and non-trivial Glivenko's theorem: a) A is provable in the classical propositional logic (i.e. in [L₁-L₁₁, MP]), iff ~~A is provable in the constructive propositional logic (i.e. in [L₁-L₁₀, MP]), b) ~A is provable in the classical propositional logic, iff ~A is provable in the constructive propositional logic.

Theorem 2.4.6. [L₁-L₉, MP]:

a) |- (~A->A)->~~A. What does it mean?

b) |- ~~(Av~A). What does it mean? In this weak form, the Law of the Excluded Middle can be "proved constructively". (Hint: derive a contradiction from ~(Av~A).)

Exercise 2.4.3. Prove (a) and (b) of Theorem 2.4.6.

Theorem 2.4.7. [L₁-L₉, MP]: a) |- (A->B)->(~~A->~~B). What does it mean?

b) |- ~~(A->B)->(~~A->~~B). What does it mean?

c) |- (A->(B->C))->(~~A->(~~B->~~C)). What does it mean?

d) ~~(A->B), ~~(B->C) |- ~~(A->C). What does it mean?

e) ~~A, ~~(A->B) |- ~~B. What does it mean?

The converse of (a): (~~A->~~B)->(A->B) cannot be proved in the constructive logic (see Section 2.8).

To prove (a), we must simply apply twice the Contraposition Law: (A->B)->(~B->~A)->(~~A->~~B). And, of course, (e) is an easy consequence of (b).

Now, let us prove (b).

Thus, by Deduction Theorem 1, |- ~~(A->B)->(~~A->~~B).

Let us prove (c).

Thus, by Deduction Theorem 1, |- (A->(B->C))->(~~A->(~~B->~~C)).

Now we can prove (d). First, let us take (c) with A = A->B, B = B->C, C = A->C:

(1) |- ((A->B)->((B->C)->(A->C)))->(~~(A->B)->(~~(B->C)->~~(A->C))).

Theorem 2.4.8. [L₁-L₉, MP]: a) |- ~~(A&B)<->(~~A & ~~B). What does it mean?

b) |- ~~A v ~~B -> ~~(AvB). What does it mean?

Attention: non-constructive reasoning! The converse of (b): ~~(AvB) -> ~~A v ~~B cannot be proved in the constructive logic (see Section 2.8). What does it mean? If we simply succeed in deriving a contradiction from ~(AvB), then, perhaps, we do not have a method allowing to decide, which part of ~~A v ~~B is true - ~~A, or ~~B?

First, let us prove |- ~~(A&B)->(~~A & ~~B).

Let us prove |- (~~A & ~~B)->~~(A&B).

Let us prove (b): |- ~~A v ~~B ->~~(AvB).

Theorem 2.4.9. [L₁, L₂, L₉, MP] |- ~A->(A->~B) (compare with Exercise 1.4.2(d)). What does it mean?

It's a weak form of the "crazy" axiom L₁₀: ~A->(A->B). This axiom says: "Contradiction implies anything". In the minimal logic we can prove 50% of L₁₀: "Contradiction implies that all is wrong". Of course, the 50%-provability of L₁₀ decreases the significance of the minimal logic accordingly.

Thus, by [L₁, L₂] Deduction Theorem 1, [L₁, L₂, L₉, MP] |- ~A->(A->~B).

Theorem 2.4.10. [L₁-L₉, MP] a) |- ~Av~B -> ~(A&B). It's a half of the so-called First de Morgan Law. What does it mean?

b) |- ~(AvB) <-> ~A&~B. It's the so-called Second de Morgan Law. What does it mean?

Attention: non-constructive reasoning! The second half of (a) - the converse implication, i.e. the equivalence ~(A&B) <-> ~Av~B can be proved in the classical logic, yet not in the constructive logic (see Section 2.8). Explain, why.

Augustus de Morgan (1806-1871): "He recognised the purely symbolic nature of algebra and he was aware of the existence of algebras other than ordinary algebra. He introduced de Morgan's laws and his greatest contribution is as a reformer of mathematical logic." (according to MacTutor History of Mathematics archive).

Prove (a) and (b->) in Exercise 2.4.4.

Let us prove (b<-).

Thus, by [L₁, L₂] Deduction Theorem 1, [L₁-L₉, MP] |- ~A&~B -> ~(AvB).

Exercise 2.4.4. Prove: a) (a) and (b->) of Theorem 2.4.10.

b) [L₁-L₉, MP]: |- (A->B)->~(A&~B). What does it mean? Compare with Theorem 2.4.1(c).

c) [L₁-L₈, MP]: |- AvB -> ((A->B)->B). What does it mean?

Attention: non-constructive reasoning! The converse implication of (a), ~(A&~B)->(A->B) cannot be proved in the constructive logic (see Section 2.8). Explain, why. Still, we will prove this formula in the classical logic.

The converse of (b): ((A->B)->B) -> AvB cannot be proved in the constructive logic (see Section 2.8). Explain, why. Still, we will prove this formula in the classical logic.

2.5. Formulas Containing Negation - Constructive Logic

In this book, constructive logic is used as a synonym of intuitionistic logic!

Constructive logic includes the "crazy" axiom L₁₀: ~B->(B->C), but rejects the Law of the Excluded Middle L₁₁: Bv~B as a general logical principle.

Theorem 2.5.1. a) [L₁₀, MP]: A, ~A |- B. What does it mean?

b) [L₁, L₂, L₈, L₁₀, MP]: |- AvB->(~A->B). What does it mean?

c) [L₁, L₂, L₈, L₁₀, MP]: |- ~AvB->(A->B). What does it mean?

Attention: non-constructive reasoning! The converse of (b), i.e. (~A->B)->AvB cannot be proved in the constructive logic (see Section 2.8). Explain, why. The converse of (c), i.e. (A->B)->~AvB cannot be proved in constructive logic (see Section 2.8). Explain, why.

Of course, (a) follows directly from L₁₀, by MP.

Let us prove (b).

Hence, by [L₁, L₂, MP] Deduction Theorem 1, [L₁, L₂, L₈, L₁₀, MP]: |- AvB->(~A->B).

Surprisingly, (b), i.e. the rule AvB, ~A |- B seems to be a quite a "natural" logical principle, yet it cannot be proved without the "crazy" axiom L₁₀! Why not? Because it implies L₁₀! Indeed,

Hence, by Deduction Theorem 1, [L₁, L₂, L₆, MP]: AvB->(~A->B) |- ~A->(A->B).

In Section 2.8 we will prove that L₁₀ cannot be derived from L₁-L₉, hence, (b) also cannot be derived from L₁-L₉ (i.e. without L₁₀).

Exercise 2.5.1. Prove (c) of Theorem 2.5.1.

Theorem 2.5.2. [L₁-L₁₀, MP]: a) |- (~~A->~~B)->~~(A->B). It's the converse of Theorem 2.4.7(b). Hence, [L₁-L₁₀, MP]: |- ~~(A->B)<->(~~A->~~B).

b) |- ~~A->(~A->A). It's the converse of Theorem 2.4.6(a). Hence, [L₁-L₁₀, MP]: |- ~~A<->(~A->A).

c) |- Av~A->(~~A->A). What does it mean?

d) |- ~~(~~A->A). What does it mean?

Of course, (b) is an instance of the axiom L₁₀.

To prove (a), let us prove that [L₁-L₁₀, MP]: ~~A->~~B, ~(A->B) |- ~B, ~~B. Then, by Theorem 2.4.1, (a) |- (~~A->~~B)->~~(A->B).

Let us prove (c) |- Av~A->(~~A->A).

Let us prove (d) |- ~~(~~A->A).

Exercise 2.5.2. Prove that in [L₁-L₁₀, MP]:

a) A |- B<->Bv~A. What does it mean?

b) |- Bv(A&~A) <-> B. What does it mean?

c) |- ((A&~A)&B)vC <-> C. What does it mean?

2.6. Formulas Containing Negation - Classical Logic

If you agree to adopt the formula Bv~B, i.e. the Law of the Excluded Middle (Axiom L₁₁ in the list of Section 1.3), you can prove, first of all, the so called Double Negation Law:

Theorem 2.6.1. [L₁-L₁₁, MP]: |- ~~A <-> A.

A half of this Law we proved in the minimal logic as Theorem 2.4.4: [L₁, L₂, L₉, MP]: |- A->~~A. Let us prove the remaining half: [L₁-L₁₁, MP] |- ~~A -> A.

By Theorem 2.5.2, [L₁-L₁₀, MP]: |- Av~A->(~~A->A), hence, [L₁-L₁₁, MP]: |- ~~A->A. Q.E.D.

Attention: non-constructive reasoning! The formula ~~A->A cannot be proved in the constructive logic, see Section 2.8. Why? Because it represents a kind of non-constructive reasoning. Indeed, imagine, you wish to prove that ExB(x). Assume the contrary - ~ExB(x), and derive a contradiction. Thus you have proved... the negation of ~ExB(x), i.e. ~ ~ExB(x). To conclude ExB(x) from ~ ~ExB(x), you need the Double Negation Law. Hence, by adopting this law as a logical principle, you would allow non-constructive existence proofs - if you prove ExB(x) by assuming ~ExB(x), and deriving a contradiction, then you may not obtain a method allowing to find a particular x satisfying B(x).

Exercise 2.6.1. Prove that [L₈, L₁₁, MP]: A->B, ~A->B |- B. Or, by Deduction Theorem 1, [L₁, L₂, L₈, L₁₁, MP]: (A->B)->((~A->B)->B). What does it mean? This formula cannot be proved in the constructive logic (see Section 2.8). Explain, why.

In the classical logic, you can prove also the full form of the Contraposition Law:

Theorem 2.6.2. [L₁-L₁₁, MP]: |- (A->B) <-> (~B->~A).

We proved a half of this Law in the minimal logic as Theorem 2.4.2: [L₁, L₂, L₉, MP]: |- (A->B)->(~B->~A). Let us prove the remaining half: [L₁-L₁₁, MP] |- (~B->~A) -> (A->B).

By Deduction Theorem 1, [L₁-L₁₁, MP] |- (~B->~A) -> (A->B).

Attention: non-constructive reasoning! The formula (~B->~A) -> (A->B) cannot be proved in the constructive logic, see Section 2.8. Explain, why.

Exercise 2.6.1A. Prove that in [L₁-L₁₁, MP]:

a) |- (~A->B)<->(~B->A) (compare with Theorem 2.4.3).

b) |- (A->B)->((~A->~B)->(B<->A)).

Attention: non-constructive reasoning! These two formulas cannot be proved in the constructive logic, see Section 2.8.

Theorem 2.6.3. [L₁-L₁₁, MP]: |- ~(A&B) <-> ~Av~B. It's the so-called First de Morgan Law.

A half of this Law we proved in the minimal logic as Theorem 2.4.10(a)a: [L₁-L₉, MP] |- ~Av~B -> ~(A&B). Let us prove the remaining half: [L₁-L₁₁, MP] |- ~(A&B) -> ~Av~B.

Attention: non-constructive reasoning! This formula cannot be proved in the constructive logic, see Section 2.8. Explain, why.

Let us start by proving ~( ~Av~B) -> A&B.

Thus, by Deduction Theorem 1, [L₁-L₉, MP] |- ~( ~Av~B) -> ~~(A&B). By applying the first half of the Contraposition Law (provable in the minimal logic): [L₁-L₉, MP] |- ~~~(A&B) ->~ ~(~Av~B). By Theorem 2.4.5: [L₁-L₉, MP] |- ~(A&B)->~~~(A&B), hence, [L₁-L₉, MP] |- ~(A&B)->~ ~(~Av~B). Now, by the Double Negation Law, [L₁-L₁₁, MP] |- ~~(~Av~B)->~Av~B, hence, [L₁-L₁₁, MP] |- ~(A&B)->~Av~B. Q.E.D.

In the classical logic, you can express implication by negation and disjunction. Indeed, we already know that [L₁-L₁₀, MP]: |- ~AvB->(A->B) (Theorem 2.5.1(c)).

Theorem 2.6.4. a) [L₁-L₈, MP]: AvC |- (A->B)->BvC. Hence, [L₁-L₈, MP]: Av~A |- (A->B)->~AvB.

b) [L₁-L₁₁, MP]: |- (A->B)<->~AvB.

Of course, (b) follows from (a) and Theorem 2.5.1(c). Let us prove (a).

Exercise 2.6.2. Prove that in [L₁-L₁₁, MP]:

a) |- B&(Av~A) <-> B. What does it mean?

b) |-( (Av~A)vB)&C <-> C. What does it mean?

c) |- ((A->B)->B) -> AvB. What does it mean? Hence, by Exercise 2.4.4(c), [L₁-L₁₁, MP]: |- ((A->B)->B) <-> AvB.

Exercise 2.6.3. Prove that in [L₁-L₁₁, MP]:

a) |- (A->B) <-> ~(A&~B). What does it mean?

b) |- ~(A->B) <-> A&~B. What does it mean?

c) |- AvB <-> (~A->B). What does it mean?

d) |- A&B <-> ~(A->~B). What does it mean?

e) (For smart students) Try detecting, which parts of these equivalencies are provable: 1) in the minimal logic, 2) in the constructive logic.

Strange formulas

Exercise 2.6.4. Prove in [L₁-L₁₁, MP] the following strange formulas:

a) |- Av(A->B). What does it mean? Does it mean anything at all?

b) |- (A->B)v(B->A). What does it mean? Does it mean anything at all? The most crazy theorem of the classical propositional logic?

c) |- ((A->B)->A)->A. What does it mean? Does it mean anything at all? It is the so-called Peirce's Law from

C.S.Peirce. On the algebra of logic: A contribution to the philosophy of notation. Amer. jour. math., 1885, vol.7, pp.180-202.

Charles S. Peirce (1839-1914): "... He was also interested in the Four Colour Problem and problems of knots and linkages... He then extended his father's work on associative algebras and worked on mathematical logic and set theory. Except for courses on logic he gave at Johns Hopkins University, between 1879 and 1884, he never held an academic post." (according to MacTutor History of Mathematics archive).

2.7. Constructive Embedding. Glivenko's Theorem

Let us recall some of the results of previous sections concerning double negations:

Theorem 2.4.4. [L₁, L₂, L₉, MP]: |- A->~~A.

Theorem 2.4.5. [L₁-L₉, MP]: |- ~~~A<->~A.

Theorem 2.4.6(b). [L₁-L₉, MP]: |- ~~(Av~A). In this weak form, the Law of the Excluded Middle can be "proved constructively".

Theorem 2.4.7. [L₁-L₉, MP]: a) |- (A->B)->(~~A->~~B).

b) |- ~~(A->B)->(~~A->~~B).

c) |- (A->(B->C))->(~~A->(~~B->~~C)).

d) ~~(A->B), ~~(B->C) |- ~~(A->C).

e) ~~A, ~~(A->B) |- ~~B.

Theorem 2.4.8. [L₁-L₉, MP]: a) |- ~~(A&B)<->(~~A & ~~B).

b) |- ~~A v ~~B -> ~~(AvB).

Theorem 2.5.2. [L₁-L₁₀, MP]: a) |- (~~A->~~B)->~~(A->B). It's the converse of Theorem 2.4.7(b).

d) |- ~~(~~A->A).

Theorem 2.6.1. [L₁-L₁₁, MP]: |- ~~A <-> A.

Does it mean that for any formula A: if [L₁-L₁₁, MP]: |- A, then [L₁-L₁₀, MP]: |- ~~A? (The converse is obvious: if [L₁-L₁₀, MP]: |- ~~A, then [L₁-L₁₁, MP]: |- A by Theorem 2.6.1.)

Imagine, we have a proof of [L₁-L₁₁, MP]: |- A. It is a sequence of formulas R₁, R₂, ..., R_n, where R_n = A. If this sequence does not contain instances of the axiom L₁₁, then it is a proof of [L₁-L₁₀, MP]: |- A as well. Hence, according to Theorem 2.4.4, [L₁-L₁₀, MP]: |- ~~A

If the sequence R₁, R₂, ..., R_n contains some instances of L₁₁, i.e. formulas having the form Bv~B, then, according to Theorem 2.4.6(b), we could try replacing each such formula by a sequence proving that [L₁-L₉, MP]: |- ~~(Bv~B). It appears that each of the formulas ~~R₁, ~~R₂, ..., ~~R_n is provable in [L₁-L₁₀, MP].

a) If R_k is an instance of the axioms L₁-L₁₀, then [L₁-L₁₀, MP]: |- ~~R_k (Theorem 2.4.4).

b) If R_k is an instance of the axiom L₁₁, then [L₁-L₁₀, MP]: |- ~~R_k (Theorem 2.4.6(b)).

c) Now, let us assume that i, j < k, and R_i, R_j |- R_k directly by MP, i.e. R_j is R_i->R_k. We know already that [L₁-L₁₀, MP]: |- ~~R_i and [L₁-L₁₀, MP]: |- ~~(R_i->R_k). By Theorem 2.4.7(b), [L₁-L₉, MP]: |- ~~(R_i->R_k)->(~~R_i->~~R_k). Hence, [L₁-L₁₀, MP]: |- ~~R_k.

Because A = R_n, we have proved the remarkable Glivenko's theorem from 1929:

V.Glivenko. Sur quelques points de la logique de M. Brouwer. Academie Royale de Belgique, Bulletins de la classe des sciences, 1929, ser.5, vol.15, pp.183-188.

On the web, very little can be found about Valery Ivanovich Glivenko (1896-1940), best known by the so-called Glivenko-Cantelli theorem in probability theory (see http://www.vgd.ru/G/glinka.htm, in Russian).

Glivenko's Theorem. [L₁-L₁₁, MP]: |- A, iff [L₁-L₁₀, MP]: |- ~~A. Or: a formula A is provable in the classical propositional logic, if and only if ~~A is provable in the constructive propositional logic.

This theorem provides a kind of a "constructive embedding" for the classical propositional logic: any classically provable formula can be "proved" in the constructive logic, if you put two negations before it.

Corollary. [L₁-L₁₁, MP]: |- ~A, iff [L₁-L₁₀, MP]: |- ~A. Or: a "negative" formula ~A is provable in the classical propositional logic, if and only if it is provable in the constructive propositional logic.

Indeed, if [L₁-L₁₁, MP]: |- ~A, then by Glivenko's theorem, [L₁-L₁₀, MP]: |- ~~~A, and by Theorem 2.4.5, [L₁-L₁₀, MP]: |- ~A. Q.E.D.

Exercise 2.7.1. Prove the following version of Glivenko's theorem (see Kleene [1952]):

a) If [L₁-L₁₁, MP]: A₁, A₂, ..., A_n |- C, then [L₁-L₁₀, MP]: ~~A₁, ~~A₂, ..., ~~A_n |- ~~C.

b) If [L₁-L₁₁, MP]: ~A₁, ~A₂, ..., ~A_n, B₁, B₂, ..., B_p |- ~C, then [L₁-L₁₀, MP]: ~A₁, ~A₂, ..., ~A_n , ~~B₁, ~~B₂, ..., ~~B_p |- ~C.

2.8. Axiom Independence. Using Computers in Mathematical Proofs

If one of our axioms L_i could be proved by using the remaining n-1 axioms, then we could simplify our logical system by dropping L_i as an axiom. A striking example:

Theorem 2.8.1. The axiom L₉: (A->B)->((A->~B)->~A) can be proved in [L₁, L₂, L₈, L₁₀, L₁₁, MP].

This fact was established by A.Kurmitis:

A.A.Kurmitis. On independence of a certain axiom system of the propositional calculus. Proc. Latvian State University, 1958, Vol. 20, N3, pp. 21-25 (in Russian).

The following proof of L₉ in [L₁, L₂, L₈, L₁₀, L₁₁, MP] is due to Janis Sedols.

First, let us establish that the formula (A->~A)->~A can be proved in [L₁, L₂, L₈, L₁₀, L₁₁, MP] (in the above Theorem 2.4.1 we established only that [L₁, L₂, L₉, MP]: |- (A->~A)->~A):

Now let us establish that in [L₁, L₂, L₁₀, MP]: A->B, A->~B |- A->~A.

Finally, let us merge the proofs of (6) and (13), then by MP we obtain ~A, i.e.

[L₁, L₂, L₈, L₁₀, L₁₁, MP]: A->B, A->~B |- ~A.

Now, by Deduction Theorem 1 (which is valid for any propositional system containing [L₁, L₂, MP]) we obtain the axiom L₉:

[L₁, L₂, L₈, L₁₀, L₁₁, MP]: (A->B)->((A->~B)->~A).

Q.E.D.

Do you think, we should drop L₉ as an axiom of our logical system? Still, L₉ cannot be proved in [L₁-L₈, L₁₀, MP] (see Theorem 2.8.2 below). Hence, if we would drop L₉, then, instead of the simplest definition

"classical logic = constructive logic + L₁₁",

we would have a more complicated one:

"constructive logic = classical logic - L₁₁ + L₉".

Now, the question of questions: could we prove the Law of the Excluded Middle (the axiom L₁₁: Bv~B) by using the other axioms (i.e. [L₁-L₁₀, MP]) as we proved L₉ in [L₁, L₂, L₈, L₁₀, L₁₁, MP]? If not, how could we demonstrate that this is impossible at all? How could we demonstrate that some logical principle is independent, i.e. that it cannot be derived from other principles?

Let us assume, we have an algorithm q computing for each formula A some its "property" q(A) such that:

a) q(L₁) is true, q(L₂) is true, ..., q(L₁₀) is true (axioms possess property q).

b) If q(A) is true and q(A->B) is true, then q(B) is true (i.e. MP "preserves" property q). Hence, q(F) is true for all the formulas F that are provable in [L₁-L₁₀, MP].

c) q(L₁₁) is false (L₁₁ does not possess property q).

If we could obtain such a property q, then, of course, this would demonstrate that L₁₁ cannot be proved in [L₁-L₁₀, MP], i.e. that the Law of the Excluded Middle is an independent logical principle.

The most popular way of introducing such properties of formulas are the so-called "multi-valued logics", introduced by Jan Lukasiewicz and Emil Post:

J.Lukasiewicz. O logice trojwartosciowej. Ruch Filozoficzny (Lwow), 1920, vol. 5, pp. 169-171

E.Post. Introduction to a general theory of elementary propositions. Amer. journ. math., 1921, vol. 21, pp.163-195

For example, let us consider a kind of "three-valued logic", where 0 means "false", 1 - "half true", 2 - "(absolutely) true". Then it would be natural to define conjunction and disjunction as

A&B = min(A,B)
AvB = max(A,B).

But how should we define implication and negation?

Thus, theoretically, we have here to explore: 3⁹ = 19683 variants of implication definitions and 3³ = 27 negation definitions.

Exercise 2.8.1. Develop a simple (recursive) computer program receiving as input:

a) Any such "truth tables".

b) Any formula F consisting of letters A, B, C, and propositional connectives.

and printing out "truth values" of the formula F, for example, if F = B->(A->B):

In this example the axiom L₁ always takes "true" values. Perhaps, we should be interested only in those variants of our "truth tables" that "satisfy" at least the axioms L₁, L₂, ..., L₈ letting them always take "true" values.

Note. See my version of the program in C++: header file, implementation, download the entire Borland C++ project (about 200K zip).

So, let us consider

"under the above truth tables, formula A always takes "true" values"

as a kind of "property" q(A).

Will MP preserve this property? If A is "true", and A->B is "true", how could B be not? Let us consider the relevant part of the above truth tables (i.e. the part where A is "true"):

If we would consider only those variants of our "truth tables" where i₇ = 0 or 1, i₈ = 0 or 1, and i₉ = 2, then, if B would not be 2 for some values of its arguments, then A->B also would not be 2 for the same values of arguments.

Hence, if we restrict ourselves to "truth tables" with i₇ = 0 or 1, i₈ = 0 or 1, and i₉ = 2, then MP preserves the property of "being true". I.e., from "true" formulas MP can derive only "true" formulas.

Note that, if we wish the axiom L₆: A->AvB always taking the value "true" (i.e. the value 2), then, if A<=B, then A->B must be 2. Thus, of all the 3⁹ = 19683 possible implication definition variants only the following 3*2*2 = 12 variants are worth of exploring:

Exercise 2.8.2. a) Verify that under any of these 12 implication definitions the axioms L₃, L₄, L₆, L₇ always take the value 2, i.e. you do not need testing these axioms any more.

b) For each of the axioms, L₁, L₂, L₅ and L₈, determine all the possible combinations of the values of i₄, i₇, i₈ forcing it to take always the value 2.

Note. The "intersection" of b) consists of 5 combinations (see the results file #00).

Exercise 2.8.3. Extend your previous computer program by adding 6 nested loops: for i4=0 to 2, for i7=0 to 1, for i8=0 to1, for ia=0 to 2, for ib=0 to 2, for ic=0 to 2. Let the program print out only those variants of "truth tables" that make "true" all the axioms L₁-L₈. (My program yields 135 such variants, see the results file #00).

In Theorem 2.8.1 we established that the axiom L₉: (A->B)->((A->~B)->~A) can be proved in [L₁-L₈, L₁₀, L₁₁, MP]. Still,

Theorem 2.8.2. The axiom L₉ cannot be proved in [L₁-L₈, L₁₀, MP].

Proof. Let your program print out only those variants of "truth tables" that make "true" all the axioms L₁-L₈, and make: L₉ - not "true", and L₁₀ - "true". My program yields 66 such variants, see the results file #01. I like especially the (most natural?) variant #33:

Implication variant #3:
2 2 2 2 2 2 0 1 2 L1-L8 true.
Variant #33. Negation: 2 1 0 L9 not true. L10 true. L11 not true.

See the extended results file #1 for this variant.

Under this variant the axioms L₁-L₈ and L₁₀ are "true". As we know, under this variant, by MP, from "true" formulas only "true" formulas can be derived. The axiom L₉ is not "true" under this variant:

Hence, L₉ cannot be proved in [L₁-L₈, L₁₀, MP]. Q.E.D.

In a similar way, we can obtain other independence results, for example,

Theorem 2.8.3. The "crazy" axiom L₁₀: ~B->(B->C) cannot be proved in the minimal logic [L₁-L₉, MP], and even not in [L₁-L₉, L₁₁, MP].

Proof. Let your program print out only those variants of "truth tables" that make "true" all the axioms L₁-L₈, and make: L₉ - "true", L₁₀ - not "true", and L₁₁ - "true". My program yields 6 such variants, see the results file #02. I like especially the (somewhat natural?) variant #1:

Implication variant #1:
2 2 2 0 2 2 0 1 2 L1-L8 true.
Variant #1. Negation: 2 2 1 L9 true. L10 not true. L11 true.

See the extended results file #2 for this variant.

Under this variant the axioms L₁-L₉ and L₁₁ are "true". As we know, under this variant, by MP, from "true" formulas only "true" formulas can be derived. The axiom L₁₀ is not "true" under this variant:

Hence, L₁₀ cannot be proved in [L₁-L₉, L₁₁, MP]. Q.E.D.

Now, let us prove the main result of this section:

Theorem 2.8.4. The Law of the Excluded Middle L₁₁: Bv~B cannot be proved in the constructive propositional logic [L₁-L₁₀, MP]. I.e. the Law of the Excluded Middle is an independent logical principle.

Proof. Let your program print out only those variants of "truth tables" that make "true" all the axioms L₁-L₈, and make: L₉ - "true", L₁₀ - "true", L₁₁ - not "true". My program yields only one such variant, see the results file #03:

Implication variant #1:
2 2 2 0 2 2 0 1 2 L1-L8 true.
Variant #1. Negation: 2 0 0 L9 true. L10 true. L11 not true.

See the extended results file #3 for this variant.

Under this variant the axioms L₁-L₁₀ are "true". As we know, under this variant, by MP, from "true" formulas only "true" formulas can be derived. The axiom L₁₁ is not "true" under this variant:

Hence, L₁₁ cannot be proved in [L₁-L₁₀, MP]. Q.E.D.

The results file #03 proves also the following

Theorem 2.8.5. The following (classically provable) formulas cannot be proved in the constructive propositional logic [L₁-L₁₀, MP]:

~~A -> A
(~B -> ~A) -> (A->B)
(~A->B)->(~B->A)
(~~A -> ~~B) -> (A->B)
(A->B) -> ~AvB
((A->B)->B)-> AvB
((A->B)->A)->A
~(A&~B)->(A->B)
~(A->B)->A&~B
Av(A->B)
(A->B)->((~A->~B)->(B->A))

Indeed, all these formulas take non-"true" values under the "truth tables" from the proof of Theorem 2.8.4.

The following three formulas also cannot be proved in the constructive propositional logic, yet, unfortunately, the "truth tables" from our proof of Theorem 2.8.4 do not allow proving this:

~(A&B) -> ~A v ~B
~~(AvB) -> ~~A v ~~B
(A->B)->((~A->B)->B)
(A->B)v(B->A)

Indeed, under the above "truth tables", these formulas always take "true" values (see results file #03). A more interesting conclusion: add these four formulas as additional axioms to [L₁-L₁₀, MP] - and L₁₁ will remain still unprovable!

Exercise 2.8.4. a) (For smart students) Verify that the latter four formulas cannot be proved in the constructive propositional logic [L₁-L₁₀, MP]. Or, see Section 4.4.

b) Verify that any of the following formulas could be used - instead of Bv~B - as the axiom L₁₁ of the classical propositional logic: i) (A->B) -> ~AvB, ii) ~~B->B, iii) ~(A->B)->A (Hint: since all these formulas are provable in [L₁-L₁₁, MP], it remains to prove L₁₁ in [L₁-L₁₀, MP] + (i), in [L₁-L₁₀, MP] + (ii), and [L₁-L₁₀, MP] + (iii)).

c) Verify that with ~~B->B instead of L₁₁ the "crazy" axiom L₁₀ becomes 100% derivable from the other ("honest"?) axioms. Perhaps, this is why many textbooks prefer the combination L₁ - L₉ + ~~B->B as the axiom list for the classical propositional logic. But, then, we are forced to define the constructive propositional logic not as a subset of the classical one, but as the classical logic with the axiom ~~B->B replaced by the "crazy" axiom L₁₀: ~B->(B->C)!

Finally, let us check which of the main results of Sections 2.5 (constructive logic) and 2.6 (classical logic) depend on the "crazy" axiom L₁₀: ~A->(A->B). Let your program print out only those variants of "truth tables" that make "true" all the axioms L₁-L₈, and make: L₉ - "true", L₁₀ - not "true". My program yields 6 such variants, see the results file #04. Surprisingly, in all these variants L₁₁ also is "true" (thus, the results file #04 equals the results file #02). As the most productive appears

Implication variant #1:
2 2 2 0 2 2 0 1 2 L1-L8 true.
Variant #1. Negation: 2 2 1 L9 true. L10 not true. L11 true.
Constructively provable formulas
Not true: (AvB)->((~A)->B)
Not true: ((~A)vB)->(A->B)
Not true: ((~~A)->(~~B))->(~~(A->B))
Not true: (~~A)->((~A)->A)
Not true: (Av(~A))->((~~A)->A)
Not true: ~~((~~A)->A)

Classically provable formulas
True: (~~(AvB))->((~~A)v(~~B))
True: (~(A&B))->((~A)v(~B))
Not true: (~~A)->A
Not true: ((~B)->(~A))->(A->B)
Not true: ((~A)->B)->((~B)->A)
Not true: ((~~A)->(~~B))->(A->B)
True: (A->B)->((~A)vB)
Not true: ((A->B)->B)->(AvB)
Not true: ((A->B)->A)->A
Not true: (~(A&(~B)))->(A->B)
Not true: (A->B)->((~A->B)->B)
Not true: (~(A->B))->(A&(~B))
Not true: Av(A->B)
True: (A->B)v(B->A)
Not true: (A->B)->(((~A)->(~B))->(B->A))

Thus, the following constructively provable formulas cannot be proved in the minimal logic [L₁-L₉, MP] (and even in [L₁-L₉, L₁₁, MP]), i.e. they cannot be proved without the "crazy" axiom L₁₀:

(AvB)->(~A->B)
~AvB -> (A->B)
(~~A->~~B) -> ~~(A->B)
~~A -> (~A->A)
Av~A -> (~~A->A)
~~(~~A->A)

And the following classically provable formulas cannot be proved without the "crazy" axiom L₁₀:

~~A->A
(~B->~A)->(A->B)
(~A->B)->(~B->A)
(~~A->~~B)->(A->B)
((A->B)->B) -> AvB
((A->B)->A)->A
~(A&~B)->(A->B)
(A->B)->((~A->B)->B)
~(A->B)->A&~B
Av(A->B)
(A->B)->((~A->~B)->(B->A))

Exercise 2.8.5 (thanks to Stanislav Golubcov for the idea). But how about the remaining four (classically provable) formulas:

a) (A->B) -> ~AvB
b) ~(A&B) -> ~Av~B,
c) ~~(AvB) -> ~~Av~~B
d) (A->B)v(B->A)?

Show that the formulas (a, b, c) can be proved without the "crazy" axiom L₁₀, i.e prove them in [L₁-L₉, L₁₁, MP]. (Hint: use Theorem 2.6.4 (a) [L₁-L₈, MP]: Av~A |- (A->B)->~AvB.). For smart students: how about the remaining formula (d)?

Do you trust the above proofs? Personally, I trust much more my ability to write (relatively) error-free computer programs than my ability to carry out error-free mathematical proofs. But how about you? Of course, you do not need trusting my (or your own) program generating the results files #00, #01, #02, #03 and #04. We used these files only to select the "truth table" variants allowing to prove our independence results. The critical points to be trusted are (see my implementation file) : a) the recursive program

int MyFormula::ValueAt(int A, int B, int C)

and b) the character string analyzer

int MyFormula::Analyze(int *pOperation, AnsiString *pSubFormula1, AnsiString *pSubFormula2)

You may wish to remove your worries by verifying directly that under all the 3 truth table variants used above: a) the axioms L₁-L₈ are true, and b) the axioms L₉, L₁₀, L₁₁ and other formulas are true or not true according to the goal of each particular proof. Before you have performed this 100%, you can feel the flavor of using computers in mathematical proofs (I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it, I trust this proof, I do not trust it,...)

Unfortunately, in more complicated cases the situation does not allow the above simple exit (i.e. manual verification of the solution found by a computer):

"The Four Colour Theorem was the first major theorem to be proved using a computer, having a proof that could not be verified directly by other mathematicians. Despite some worries about this initially, independent verification soon convinced everyone that the Four Colour Theorem had finally been proved. Details of the proof appeared in two articles in 1977. Recent work has led to improvements in the algorithm." (According to the article The Four Colour Theorem in MacTutor History of Mathematics archive).

The proof of the Four Colour Theorem was completed in 1976 by Kenneth Appel and Wolfgang Haken, see their biographies published on the web by Ryan Proper.

"The best-known, and most debated, instance is the use of computer analysis by Kenneth Appel and Wolfgang Haken of the University of Illinois in their 1976 proof of the four-colour conjecture (that four colours suffice to colour in any map drawn upon a plane in such a way that countries which share a border are given different colours). First put forward in 1852, the conjecture had become perhaps the most famous unsolved problem in mathematics, resisting a multitude of efforts at proof for over a century. Appel and Haken's demonstration rested upon computerized analysis, occupying 1,200 hours of computer time, of over 1,400 graphs. The analysis of even one of those graphs typically went beyond what an unaided human being could plausibly do: the ensemble of their demonstration certainly could not be checked in detail by human beings. In consequence, whether that demonstration constituted "proof" was deeply controversial..." (according to COMPUTERS AND THE SOCIOLOGY OF MATHEMATICAL PROOF by Donald MacKenzie).

For a popular overview of the controversy around the Four Colour Theorem, see

Andreea S.Calude. The Journey of the Four Colour Theorem Through Time. The New Zealand Mathematics Magazine, 38, 3, (2001), 1-10 (available online at http://matholymp.com/ARTICLES/4color.pdf).

But how about proving the following theorem?

Theorem 2.8.6. Appel and Haken's computer program is correct.

(See also the article Fermat's Last Theorem in MacTutor History of Mathematics archive.)

See logical software links selected by Peter Suber.

Visit the Mizar Project.

Back to title page

propositional logic, propositional calculus, intuitionistic, logic, propositional, minimal, constructive, intuitionist, computer, independent, constructive logic, minimal logic, intuitionistic logic, calculus, Glivenko, independence, embedding