Formal Systems - an Example

A simple formal system (MIU-system) borrowed from D. Hofstadter's Gödel, Escher, Bach has a three letter (M, I, U) alphabet. A sentence in the MIU-stem is a finite string formed by the three letters of the alphabet: IMU, IIMMUU, UIMUUIIIIIIIII, etc. There is one axiom (MI) and four rules of deduction. An application of a rule produces a theorem which is inserted at the top of the list in the main area of the applet. Originally there is only one item: the axiom MI.

Rule 1

If xI is a theorem then so is xIM.

(Here and below, x and later y, stands for any sentence of the system and plays the role of a metavariable, a place holder. For this reason, axioms like that are often called axiom schema. Significantly, x is not a symbol of the MIU-system nor it is included into its alphabet.)

Rule 2

If Mx is a theorem then so is Mxx.

(Although x stands for an arbitrary MIU-sentence, the sentence x stands for is the same in all three occurrences of x.)

Rule 3

If MxIIIy is a theorem then so is MxUy.

(As before, x and now also y stand for an arbitrary MIU-sentence, which are the same in all occurrences of x and, respectively, y.)

Rule 4

If MxUUy is a theorem then so is Mxy.

The MIU-system is presented by the author as a puzzle: is the sentence MU a theorem?

The applet below affords you an opportunity to deduce theorems in the MIU-system. To apply one of the for deduction rules to the topmost statement on the right just press one of the buttons on the left. An ambiguity may arise in applying Rules 3 or 4. For example, the string MIIII may be reduced by Rule 3 to either MUI or MIU. On such occasions, the string is displayed at the bottom of the applet where you should select the occurrence of the triple "III" (to apply Rule 3) or the double "UU" (to apply Rule 4) by clicking on the first letter of the pattern. If there is no ambiguity the rule applies automatically.

(The applet has a built-in limitation: you can't prove theorems that are longer than 10000 characters.)


If you are reading this, your browser is not set to run Java applets. Try IE11 or Safari and declare the site as trusted in the Java setup.

Formal Systems - an Example

What if applet does not run?



  1. D. Hofstadter, Gödel, Escher, Bach: An Eternal Golden Braid, Basic Books, 1999

|Activities| |Contact| |Front page| |Contents| |Eye opener| |Algebra|

Copyright © 1996-2018 Alexander Bogomolny

The answer to the puzzle is that MU is not a theorem in the MIU-system.

To see that let's observe that any theorem in the MIU starts with M, with rest of the string consisting entirely from U's and I's. This is true of the axiom MI. Furthermore, if any of the rules 1-4 applies to a string of U's and I's preceded by M, the result is a string with the same property.

Next, let's establish the following theorem about MIU-system from which the impossibility for MU to be a theorem will follow immediately.


The number of I's in a theorem of the MIU-system is never divisible by 3.


Let's N(x) denote the number of I in string x. N(MI) = 1. The rules 1 and 4 do not affect the number of I's in a string. Rule 2 doubles that number so that, if Rule 2 converts a string x into a string y then 2N(x) = N(y), obviously. But, if N(y) = 2N(x) is divisible by 3, then so is N(x), for 2 and 3 are primes. It follows that if N(x) is not divisible by 3, N(y) is also is not divisible by 3.

Lastly, if y is produced by applying rule 3 to x, then N(y) = N(x) - 3, so, again either both N(x) and N(y) are divisible by 3 or both are not. This proves the (meta)theorem.

Since N(MU) = 0 and is divisible by 3, hence MU is not a theorem in the MIU-system.

Back to What Is Infinity?

|Activities| |Contact| |Front page| |Contents| |Eye opener| |Algebra|

Copyright © 1996-2018 Alexander Bogomolny