Before discussing how it might be that reality is mathematics, it would be a good idea to give consideration to what mathematics, itself, really is. In other words, we need to understand what is meant by a mathematical structure. The quick answer is that a mathematical structure is a formal system.
Formal systems are an important part of the foundations of mathematics. So, by a mathematical structure we shall mean some kind of formal system. But what is a formal system? We’ll address this question by considering the various “ingredients” that go toward making a formal system.
The first essential feature of a formal system is a finite set of symbols. These symbols form something of an “alphabet” and are sometimes referred to as primitive symbols. Such symbols are inherently meaningless in the sense that they have no referents outside of themselves. By way of contrast, the word “moon” refers to the spherical body orbiting our planet:
The elements of , however, are abstract entities, mere labels, with no intrinsic meaning. Sometimes it is tempting to see meaning in certain sets of symbols because of familiarity or various other reasons. For instance, the symbols are immediately interpreted as meaning the familiar concepts of adding, taking away, multiplying and equality respectively. This is largely a matter of habit and convention, but nothing about the symbols themselves requires them to take on these meanings, or any meaning for that matter. In another post we’ll consider how meaningless symbols take on a sort of meaning by force, as it were. This is part of Hofstadter’s thesis, namely that
“…meaning cannot be kept out of formal systems when sufficiently complex isomorphisms arise. Meaning comes in despite one’s best efforts to keep symbols meaningless!”
For now, what can one do with such meaningless symbols? That such symbols form an “alphabet” is suggestive. The essential idea is to create “words”. By “words” is meant finite strings of these primitive symbols. The set of finite strings, of course, is countably infinite. For example, if the set of primitive symbols is , then the set of all finite strings would include:
Now, creating finite strings of meaningless symbols isn’t all that interesting on its own. This leads us to our next ingredient.
The second ingredient is a grammar or syntax, which governs the way “words” are formed. In other words, not just any finite string will do. Based on the grammar or syntax, some strings will be considered well-formed and others not. This is not unfamiliar. The same idea exists in natural language. In English, the word “formed” is well-formed, whereas “sbbkdvkd” is not well-formed. In logic, the string is well-formed, while is not.
These legitimate “words” are generally referred to as well-formed formulas (wff’s). So, syntax provides a set of rules that define how to create wff’s. It is also generally required that there be a decision procedure that allows one to decide whether a particular string is well-formed or not. Such a decision procedure can be thought of as some sort of criteria that must be met, which indicates whether or not a particular string has an appropriate form. As an example, let us return to logic. The primitive symbols reside in the set
where is an arbitrary set of propositional variables (usually letters) and is the set of “usual” propositional connectives, along with the “grouping” symbols “(” and “)”. One can then define wff’s as follows:
(1) Every member of is a wff (these are called atomic formulas).
(2) If is a wff, then so is (“” is considered a unary connective).
(3) If and are wff’s and is any binary propositional connective, then is a wff.
Some examples of binary propositional connectives are .
From (1)-(3), it is now clear why is well-formed, but is not. In fact, given any finite string of symbols , our decision procedure allows one to determine whether or not is a wff in a finite amount of time.
Step One: Check if .
If so, then stop. If , then proceed to step two.
Step Two: Check if , where .
If so, then stop. If not, proceed to step three.
Step Three: Locate all binary connectives in the string and check that each connective component is a wff. Note that elements of cannot be concatenated, but must be separated by binary connectives.
Okay, having an “alphabet” and an infinite set of wff’s is great, but still not terribly interesting. Let’s see what else is needed for a formal system.
With the appropriate building materials, we now need a foundation on which to build our formal system. By “foundation” is meant a set of axioms. These axioms are wff’s, which are taken as given, a starting scheme or a choice of “seeds”, if you will, which will grow into our system. In other words, even though we have an “alphabet” and well-formed formulas, none of them are really in our possession at this point. Thus, we need an axiom schema, which stands for a countably infinite set of axioms. Often, one can define these recursively. There are also systems which can be finitely axiomatized. One can think of axioms as “true statements” of the system one gets for free. Let’s consider a well known example of the former type, namely the Peano axioms for the natural numbers . There are several equivalent ways to formulate these axioms, but the following is a common way of presenting them.
: 0 is a natural number.
Here 0 is a constant symbol and is given to us as a natural number. The next few axioms deal with the relational properties of the symbol “=”, which is interpreted as equality.
: For any natural number , .
This axiom seems funny, but it says that “=” is a reflexive relation.
: For all natural numbers and , if , then .
This means that “=” is a symmetric relation.
: For all natural numbers , and , if and , then .
So, “=” is a transitive relation. Taken together, axioms – allow us to say that “=” is an equivalence relation and, hence, is why we call it “equality”.
: For all and , if is a natural number and , then is a natural number.
This axiom means that the natural numbers are closed under equality; we don’t get any weird or unwanted objects in via some bizarre equality.
For the last set of axioms, let be a function, called the “successor” function. Our notation, here, is suggestive. It embodies the following axiom.
: If is a natural number, then so is .
Since gives us a starting natural number, we get the natural number , which is defined to be 1, the “successor” of 0. Applying again we get the natural number or , which is defined to be 2, the “successor” of 1. In general, is taken to be the natural number , the “successor” of .
: For every natural number , .
In other words, 0 is not the successor of any natural number. Thus, 0 is truly the “beginning” of the natural numbers.
: For any natural numbers and , if , then .
Thus, is an injective (i.e. one-to-one) function. Finally, we have
: If is a set such that (i) 0 is a member of and (ii) for every natural number , if , then ; then contains every natural number.
This is called the induction axiom. From these axioms, one can derive all the properties of the natural numbers.
With axioms in hand, things are beginning to get interesting. But before one can get anywhere with the axioms, one needs a mechanism or a means with which to build off of the axioms. This leads to the final ingredient of a formal system.
The final ingredient necessary for a formal system is a set of inference rules, that is, a set of rules for transforming one string of symbols into another. These rules can be applied to the given/free wff’s provided by the axioms to obtain new wff’s , which are called theorems. All wff’s provided by the axioms are theorems. We might say they are complimentary theorems. All other theorems are derived from the axioms via the rules of inference. So, if the axioms are the “seeds”, the inference rules determine what these “seeds” can grow into or what kind of system they can produce. Now generally, one desires that the inference rules be recursively defined in the sense that there is a decision procedure for determining if some string is a theorem or not as in the case with wff’s.
To prevent this post from getting too long, the next post will explore a toy formal system introduce by Hofstadter called the MIU-system. This will give us occasion to understand the concepts of this post better, especially the idea of a set of inference rules.