Previously, we explored the nature of formal systems in a more technical manner. In this post I hope to illustrate the concepts and features of formal systems via a toy formal system called the MIU-system. Douglas Hofstadter introduces this system in his book Gödel, Escher, Bach: An Eternal Golden Braid. Let’s see how it works.
In case you haven’t already guessed, the finite set of (meaningless) symbols in this case is . Why these symbols? Well, it doesn’t matter. They are meaningless. But if you hate them, you are more than welcome to swap them out with your favorites.
With this “alphabet” one can make all sorts of finite strings (a countably infinite amount). For example,
The syntax of this system is very easy. All strings made up of symbols from are legitimate. So, the examples I gave above are actually wff’s. But remember, we don’t currently “possess” any wff’s. What we need is a set of axioms.
This particular system is an example of one that is finitely axiomatized. In fact, it has but one axiom.
This means that the only wff in our possession to work with is the string . Okay, but what can we do with it? This is where we need a set of inference rules. There are four.
(1) If you possess a string ending in , you can add a to the end.
Here is a good place to point out, as Hofstadter does, that in any string order matters! One must always be careful not to assume that certain relational properties hold that aren’t given by the inference rules. For instance, one cannot assume that symbols are interchangeable – i.e. commutative. is not the same as ; cannot be swapped out with . They are different strings.
(2) Let be any string. Then if you possess a string of the form , you also possess .
For example, suppose we had the string Then, in this case and hence we would get the string .
(3) If occurs anywhere within a string in your possession, you may replace with .
For instance, suppose we have the string . Then we also get the string .
(4) If occurs anywhere within a string in your possession, you may drop it.
So, if we had the string , then we would also have .
With these four inference rules and the axiom string , we can proceed to produce theorems for our -system. Note that because we have we can immediately apply (1) to get as part of our collection. We can alternatively apply (2) to to get .
One thing you will quickly notice is that all theorems of the -system begin with . However, it is not the case that every string beginning with is a theorem.
Here is an exercise: Given , can you produce ? If so, show how. If not, explain why not. (I’ll post a solution at some point)
In the next post I’ll talk a little about a decision procedure for the -system and then we’ll move on to other matters.