Formal Systems

Formal Systems play an important role in computer science, linguisitics, and logic. What are they? Can they be used to model human thought?

The Basics

A formal system consists of a language over some alphabet of symbols together with (axioms and) inference rules that distinguish some of the strings in the language as theorems.


Don't worry, we'll make sense of that definition. And there'll be examples, too.

Some Motivation

There is some reason to believe that formal systems may be useful in the study of human thought. (In fact, one of the central questions explored in Hofstadter's GEB is whether human thought follows formal rules or not.) Why is this, and what do we mean by a formal system?

First, note that it would appear that every thought we can have, indeed every chunk of information we can imagine, can be captured as a string of symbols. Examples:

Furthermore, we often process information by shunting symbols around according to certain rules. Example:

(* (+ 4 3) (- 9 7))
⇒ (* 7 (- 9 7))
⇒ (* 7 2)
⇒ 14

The symbols by themselves seem to be meaningless, but when put into certain formal systems, they seem to acquire meaning. Do brains and minds and human thought work this way? After all, not many people argue that a single neuron is intelligent, but somehow when you put tens of billions of them together, each one with connections to many thousands of others, something does emerge.

When scientists study phenomena, they make models and develop theories. Formal systems can model certain behavior.

Components of a Formal System

A formal system has the following components:

This is only progress toward understanding formal systems. We soooooo need to go to examples now.

Examples of Formal Systems

The MIU-System

The MIU-System was defined by Hofstadter in GEB.

Here is an example derivation:

(2)MIIFrom (1) by Rule II
(3)MIIIIFrom (2) by Rule II
(4)MIIIIUFrom (3) by Rule I
(5)MUIUFrom (4) by Rule III
(6)MUIUUIUFrom (5) by Rule II
(7)MUIIUFrom (6) by Rule IV

This means that MI, MII, MIIII, MIIIIU, MUIU, MUIUUIU, and MUIIU are all theorems of the MIU-System.

Exercise: Show that the following are theorems of the MIU-System:
  • MIU
Exercise: Is MU a theorem of the MIU-System?

The pq-System

This formal system was also invented by Hofstadter in GEB.

Some theorems:

(2)--p--q----From (1) by Rule
(5)-----p--q-------From (4) by Rule
(6)-----p---q--------From (5) by Rule
(7)-----p----q---------From (6) by Rule
Exercise: Is ---p----q------- a theorem? Why or why not?
Exercise: Is ---p-----q------- a theorem? Why or why not?
Exercise: What do you think these theorems mean, if anything?
Exercise: Is ---p--p--q------- a theorem? Why or why not? Does this bother you? Should it?

The tq-System

You guessed it. This one too was invented by Hofstadter in GEB.

Some theorems:

(2)--t--q----From (1) by Rule
(5)-----t--q----------From (4) by Rule
(6)-----t---q---------------From (5) by Rule
(7)-----t----q--------------------From (6) by Rule

Inside and Outside the System

When generating theorems you have to follow the rules and never do anything else. This seems obvious for the MIU-system, but once you perceive the isomorphism in the pq-system that says:

you may have trouble keeping your knowlege of the system from getting in the way. For example, ---p-p--q------ is not a theorem, even if you want it to be.


Is U a theorem of the MIU-system? You could imagine a program generating theorems forever, but no sane human would. Humans would jump right out of the system, easily justifying the metatheorem that all theorems start with M.

Is MU a theorem of the MIU-system? Here it is not so clear...


So how can we tell whether something is a theorem or not? This would seem to require reasoning outside the system. No worries. But one that is worth wondering is whether the decision procedure is mechanical or not. That is, is there a formal system for reasoning about formal systems? About themselves?

What we can say:

The C-System

Let's try to create theorems that express that certain numbers are prime. It seems easier to start the notion of compositeness. The C-System is an extension of the tq-system.

The P-System

Now for primes. One might be inclined to give a rule like:

That's not at all typographical!

But wait. Is there any reason to believe that we should be able to find typographical rules for non-theorems of a formal system. That is, in general, if we have a formal system S (that generates theorems), then must a formal system S' exist which generates all and only the non-theorems of S? What do you think?

Spolier: In general, the answer is no. But for primes, we can create a formal system. FYI, here are the rules (x and y are hyphen strings):


Loosely speaking, a formal system is consistent with respect to an interpretation if all of the theorems are compatible with one another.

The Modified pq-System

Hofstadter invented this one, too.

He just added Axiom 2 to the existing pq-system. But now wait! Look at some of the theorems of this system:

(1)--p-q---Axiom 1
(2)--p-q--Axiom 2
(3)--p--q---From (2) by Rule

Don't these say, respectively, 2+1=3, 2+1=2, and 2+2=3? Is our system inconsistent?

Answer: It is only inconsistent relative to the old interpretation where q meant "equals". Changing this to "greater than or equal to" lets us "regain" consistency. This seems so obvious, but it completely parallels the story of the development of Non-Euclidean Geometry in the 19th century. After denying the 5th postulate (in different ways!), the people working on this needed to come up with new interpretations for the undefined terms "point" and "line".


Consistency tells us whether we've found an interpretation for our "meaningless" symbols that works. Completeness tells us that the formal system captures everything possible within that interpretation.

Completeness of the pq-System

The pq-system is consistent under the original interpretation because the sums are always correct. It is complete under that interpretation because all mathematical statements of the form x+y=z can be captured with a theorem of the pq-system. But is not complete for all of arithmetic.

Completeness of the Modified pq-System

The modified pq-system is consistent under the interpretation in which q means "greater-than-or-equal-to" but is not complete because there is no theorem of the system that can capture the fact that 2+9≥1. What to do? We can reinterpret q as "equals or exceeds by 1" to achieve completeness. But still, even the modified pq-system is not complete for all of arithmetic.

Completeness of Arithmetic Formal Systems in General

Is there a formal system for all or arithmetic (number theory) that is both consistent and complete? Alas, no. That is one of Gödel's incompleteness theorems. Again, loosely speaking:

Further Reading