Basic logic [and axioms]
The formal study of logic began in antiquity (see page 1099), with verbal descriptions of many templates for valid arguments—corresponding to theorems of logic—being widely known by medieval times. Following ideas of abstract algebra from the early 1800s, the work of George Boole around 1847 introduced the notion of representing logic in a purely symbolic and algebraic way. (Related notions had been considered by Gottfried Leibniz in the 1680s.) Boole identified 1 with True and 0 with False, then noted that theorems in logic could be stated as equations in which Or is roughly Plus and And is Times—and that such equations can be manipulated by algebraic means. Boole's work was progressively clarified and simplified, notably by Ernst Schröder, and by around 1900, explicit axiom systems for Boolean algebra were being given. Often they included most of the 14 highlighted theorems of page 817, but slight simplifications led for example to the "standard version" of page 773. (Note that the duality between And and Or is no longer explicit here.) The "Huntington version" of page 773 was given by Edward Huntington in 1933, along with
{(¬ ¬ a) a, (a ∨ ¬ (b ∨ ¬ b)) a, (¬ (¬ (a ∨ ¬ b) ∨ ¬ (a ∨ ¬ c))) (a ∨ ¬ (b ∨ c))}
The "Robbins version" was suggested by Herbert Robbins shortly thereafter, but only finally proved correct in 1996 by William McCune using automated theorem proving (see page 1157). The "Sheffer version" based on Nand (see page 1173) was given by Henry Sheffer in 1913. The shorter version was devised by David Hillman as part of the development of this book. The shortest version is discussed on page 808. (See also page 1175.)
In the main text each axiom defines an equivalence between expressions. The tradition in philosophy and mathematical logic has more been to take axioms to be true statements from which others can be deduced by the modus ponens inference rule {x, x y} y (see page 1155). In 1879 Gottlob Frege used his diagrammatic notation to set up a symbolic representation for logic on the basis of the axioms
{a (b a), (a (b c)) ((a b) (a c)), (a (b c)) (b (a c)), (a b) ((¬ b) (¬ a)), (¬ ¬ a) a, a (¬ ¬ a)}
Charles Peirce did something similar at almost the same time, and by 1900 this approach to so-called propositional or sentential calculus was well established. (Alfred Whitehead and Bertrand Russell used an axiom system based on Or and Not in their original 1910 edition of Principia Mathematica.) In 1948 Jan Łukasiewicz found the single axiom version
{((a (b a)) ((((¬ c) (d (¬ e))) ((c (d f)) ((e d) (e f)))) g)) (h g)}
equivalent for example to
{((¬ a) (b (¬ c))) ((a (b d)) ((c b) (c d))), a (b a)}
It turns out to be possible to convert any axiom system that works with modus ponens (and supports the properties of ) into a so-called equational one that works with equivalences between expressions by using
Module[{a}, Join[Thread[axioms a a], {((a a) b) b, ((a b) b) (b a) a}]]
An analog of modus ponens for Nand is {x, x ⊼ (y ⊼ z)} z, and with this Jean Nicod found in 1917 the single axiom
{(a ⊼ (b ⊼ c)) ⊼ ((e ⊼ (e ⊼ e)) ⊼ ((d ⊼ b) ⊼ ((a ⊼ d) ⊼ (a ⊼ d))))}
which was highlighted in the 1925 edition of Principia Mathematica. In 1931 Mordechaj Wajsberg found the slightly simpler
{(a ⊼ (b ⊼ c)) ⊼ (((d ⊼ c) ⊼ ((a ⊼ d) ⊼ (a ⊼ d))) ⊼ (a ⊼ (a ⊼ b)))}
Such an axiom system can be converted to an equational one using
Module[{a}, With[{t = a ⊼ (a ⊼ a), i = #1 ⊼ (#2 ⊼ #2) &}, Join[Thread[axioms t], {i[t ⊼ (b ⊼ c), c] t, i[t, b] b, i[i[a, b], b] i[i[b, a], a]}]]]
but then involves 4 axioms.
The question of whether any particular statement in basic logic is true or false is always formally decidable, although in general it is NP-complete (see page 768).
