12.1 Mechanizing Reasoning

Humans have been attempting to mechanize reasoning for thousands of years. Aristotle's Organon developed rules of inference known as syllogisms to codify logical deductions in approximately 350 BC.

Euclid went beyond Aristotle by developing a formal axiomatic system. An axiomatic system is a formal system consisting of a set of axioms and a set of inference rules. The goal of an axiomatic system is to codify knowledge in some domain.

The axiomatic system Euclid developed in The Elements concerned constructions that could be drawn using just a straightedge and a compass.

Euclid started with five axioms (more commonly known as postulates); an example axiom is: A straight line segment can be drawn joining any two points. In addition to the postulates, Euclid states five common notions, which could be considered inference rules. An example of a common notion is: The whole is greater than the part.

Starting from the axioms and common notions, along with a set of definitions (e.g., defining a circle), Euclid proved 468 propositions mostly about geometry and number theory. A proposition is a statement that is stated precisely enough to be either true or false. Euclid's first proposition is: given any line, an equilateral triangle can be constructed whose edges are the length of that line.

A proof of a proposition in an axiomatic system is a sequence of steps that ends with the proposition. Each step must follow from the axioms using the inference rules. Most of Euclid's proofs are constructive: propositions state that a thing with a particular property exists, and proofs show steps for constructing something with the stated property. The steps start from the postulates and follow the inference rules to prove that the constructed thing resulting at the end satisfies the requirements of the proposition.

A consistent axiomatic system is one that can never derive contradictory statements by starting from the axioms and following the inference rules. If a system can generate both $A$ and not $A$ for any proposition $A$, the system is inconsistent. If the system cannot generate any contradictory pairs of statements it is consistent.

A complete axiomatic system can derive all true statements by starting from the axioms and following the inference rules. This means if a given proposition is true, some proof for that proposition can be found in the system. Since we do not have a clear definition of true (if we defined true as something that can be derived in the system, all axiomatic systems would automatically be complete by definition), we state this more clearly by saying that the system can decide any proposition. This means, for any proposition P, a complete axiomatic system would be able to derive either P or not P. A system that cannot decide all statements in the system is incomplete. An ideal axiomatic system would be complete and consistent: it would derive all true statements and no false statements.

The completeness of a system depends on the set of possible propositions. Euclid's system is consistent but not complete for the set of propositions about geometry. There are statements that concern simple properties in geometry (a famous example is any angle can be divided into three equal sub-angles) that cannot be derived in the system; trisecting an angle requires more powerful tools than the straightedge and compass provided by Euclid's postulates.

Figure 12.1 depicts two axiomatic systems. The one on the left one incomplete: there are some propositions that can be stated in the system that are true for which no valid proof exists in the system. The one on the right is inconsistent: it is possible to construct valid proofs of both P and not P starting from the axioms and following the inference rules. Once a single contradictory proposition can be proven the system becomes completely useless. The contradictory propositions amount to a proof that true = false, so once a single pair of contradictory propositions can be proven every other false proposition can also be proven in the system. Hence, only consistent systems are interesting and we focus on whether it is possible for them to also be complete.

Figure 12.1: Incomplete and inconsistent axiomatic systems.

Russell's Paradox. Towards the end of the 19$^{th}$ century, many mathematicians sought to systematize mathematics by developing a consistent axiomatic system that is complete for some area of mathematics. One notable attempt was Gottlob Frege's Grundgestze der Arithmetik (1893) which attempted to develop an axiomatic system for all of mathematics built from simple logic.

Bertrand Russell discovered a problem with Frege's system, which is now known as Russell's paradox. Suppose $R$ is defined as the set containing all sets that do not contain themselves as members. For example, the set of all prime numbers does not contain itself as a member, so it is a member of $R$. On the other hand, the set of all entities that are not prime numbers is a member of $R$. This set contains all sets, since a set is not a prime number, so it must contain itself.

The paradoxical question is: is the set $R$ a member of $R$? There are two possible answers to consider but neither makes sense:

Yes: $R$ is a member of $R$: We defined the set $R$ as the set of all sets that do not contain themselves as member. Hence, $R$ cannot be a member of itself, and the statement that $R$ is a member of $R$ must be false. No: $R$ is not a member of $R$: If $R$ is not a member of $R$, then $R$ does not contain itself and, by definition, must be a member of set $R$. This is a contradiction, so the statement that $R$ is not a member of $R$ must be false.

The question is a perfectly clear and precise binary question, but neither the "yes" nor the "no" answer makes any sense. Symbolically, we summarize the paradox: for any set $s$, $s \in R$ if and only if $s \notin s$. Selecting $s = R$ leads to the contradiction: $R \in R$ if and only if $R \notin R$.

Whitehead and Russell attempted to resolve this paradox by constructing their system to make it impossible to define the set $R$. Their solution was to introduce types. Each set has an associated type, and a set cannot contain members of its own type. The set types are defined recursively:

  • A type zero set is a set that contains only non-set objects.
  • A type-$n$ set can only contain sets of type $n-1$ and below.

This definition avoids the paradox: the definition of $R$ must now define $R$ as a set of type $k$ set containing all sets of type $k-1$ and below that do not contain themselves as members. Since $R$ is a type $k$ set, it cannot contain itself, since it cannot contain any type $k$ sets.

In 1913, Whitehead and Russell published Principia Mathematica, a bold attempt to mechanize mathematical reasoning that stretched to over 2000 pages. Whitehead and Russell attempted to derive all true mathematical statements about numbers and sets starting from a set of axioms and formal inference rules. They employed the type restriction to eliminate the particular paradox caused by set inclusion, but it does not eliminate all self-referential paradoxes.

For example, consider this paradox named for the Cretan philosopher Epimenides who was purported to have said "All Cretans are liars". If the statement is true, than Epimenides, a Cretan, is not a liar and the statement that all Cretans are liars is false. Another version is the self-referential sentence: this statement is false. If the statement is true, then it is true that the statement is false (a contradiction). If the statement is false, then it is a true statement (also a contradiction). It was not clear until Godel, however, if such statements could be stated in the Principia Mathematica system.