Axiom systems

In the main text I argue that there are many consequences of axiom systems that are quite independent of their details. But in giving the specific axiom systems that have been used in traditional mathematics one needs to take account of all sorts of fairly complicated details.

As indicated by the tabs in the picture, there is a hierarchy to axiom systems in traditional mathematics, with those for basic and predicate logic, for example, being included in all others. (Contrary to usual belief my results strongly suggest however that the presence of logic is not in fact essential to many overall properties of axiom systems.)

As discussed in the main text (see also page 1155) one can think of axioms as giving rules for transforming symbolic expressions—much like rules in Mathematica. And at a fundamental level all that matters for such transformations is the structure of expressions. So notation like a + b and a × b, while convenient for interpretation, could equally well be replaced by more generic forms such as f[a, b] or g[a, b] without affecting any of the actual operation of the axioms.

My presentation of axiom systems generally follows the conventions of standard mathematical literature. But by making various details explicit I have been able to put all axiom systems in forms that can be used almost directly in Mathematica. Several steps are still necessary though to get the actual rules corresponding to each axiom system. First, the definitions at the top of page 774 must be used to expand out various pieces of notation. In basic logic I use the notation u  v to stand for the pair of rules u  v and v  u. (Note that  has the precedence of  not .) In predicate logic the tab at the top specifies how to construct rules (which in this case are often called rules of inference, as discussed on page 1155). x_ ∧ y_  x_ is the modus ponens or detachment rule (see page 1155). x_  ∀_{y_} x_ is the generalization rule. x_  x_ ∧ # & is applied to the axioms given to get a list of rules. Note that while  in basic logic is used in the underlying construction of rules,  in predicate logic is just an abstract operator with properties defined by the last two axioms given.

As is typical in mathematical logic, there are some subtleties associated with variables. In the axioms of basic logic literal variables like a must be replaced with patterns like a_ that can stand for any expression. A rule like a_ ∧ (b_ ∨ ¬ b_)  a can then immediately be applied to part of an expression using Replace. But to apply a rule like a_  a ∧ (b ∨ ¬ b) requires in effect choosing some new expression for b (see page 1155). And one way to represent this process is just to have the pattern a_  a_ ∧ (b_ ∨ ¬ b_) and then to say that any actual rule that can be used must match this pattern. The rules given in the tab for predicate logic work the same way. Note, however, that in predicate logic the expressions that appear on each side of any rule are required to be so-called well-formed formulas (WFFs) consisting of variables (such as a) and constants (such as 0 or ∅) inside any number of layers of functions (such as +, ·, or Δ) inside a layer of predicates (such as  or ∈) inside any number of layers of logical connectives (such as ∧ or ⇒) or quantifiers (such as ∀ or ∃). (This setup is reflected in the grammar of the Mathematica language, where the operator precedences for functions are higher than for predicates, which are in turn higher than for quantifiers and logical connectives—thus yielding for example few parentheses in the presentation of axiom systems here.)

In basic logic any rule can be applied to any part of any expression. But in predicate logic rules can be applied only to whole expressions, always in effect using Replace[expr, rules]. The axioms below (devised by Matthew Szudzik as part of the development of this book) set up basic logic in this way.