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.

What?

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:

91442.3
Stay behind the yellow line!
/Pecs/Los Angeles/Berlin/Madrid//1 2/3 0/2 2/2 0/3 2///
(* (+ 4 3) (- 9 7))
int average(int x, int y) {return (x + y) / 2;}
<dog id="30024"><name>Lisichka</name><age>13</age></dog>
∀α β. α⊥β ⇔ (α•β = 0)
1. f3 e5 2. g4 ♛h4++

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:

A finite alphabet of symbols. The alphabet must be finite because if it were not, each symbol could stand for any thought and so what kind of a model would that be? There would be no need to "process" anything. Furthermore, we are finite beings and let's keep in mind what we are trying to model.
A syntax that defines which strings of symbol are in the language of our formal system.
A decidable set of axioms and a finite set of rules from which the set of theorems of the system is generated. The rules must take a finite number of steps to apply.

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.

Alphabet: {M, I, U}
Syntax: All strings over the alphabet are in the language.
Inference Rules: Let x and y be arbitrary strings of zero or more symbols.

Here is an example derivation:

(1)	`MI`	Axiom
(2)	`MII`	From (1) by Rule II
(3)	`MIIII`	From (2) by Rule II
(4)	`MIIIIU`	From (3) by Rule I
(5)	`MUIU`	From (4) by Rule III
(6)	`MUIUUIU`	From (5) by Rule II
(7)	`MUIIU`	From (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
MIUIUIUIU
MUIIIIU

Exercise: Is MU a theorem of the MIU-System?

The pq-System

This formal system was also invented by Hofstadter in GEB.

Alphabet: {p, q, –}
Syntax: The strings of the language have the form one or more hyphens followed by p followed by one or more hyphens followed by q followed by one or more hyphens.
Inference Rules: Let x and y be strings of one or more hyphens:

Some theorems:

(1)	`--p-q---`	Axiom
(2)	`--p--q----`	From (1) by Rule
(3)	`-p-q--`	Axiom
(4)	`-----p-q------`	Axiom
(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.

Alphabet: {t, q, –}
Syntax: The strings of the language have the form one or more hyphens followed by t followed by one or more hyphens followed by q followed by one or more hyphens.
Inference Rules: Let x, y, and z be strings of one or more hyphens:

Some theorems:

(1)	`--t-q--`	Axiom
(2)	`--t--q----`	From (1) by Rule
(3)	`-t-q-`	Axiom
(4)	`-----t-q-----`	Axiom
(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:

p ⇔ plus
q ⇔ equals
string of n dashes ⇔ n

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.

Distinguish:

M-mode (Mechanical Mode): Working completely within the system
I-mode (Intelligent Mode): Reasoning about the system
U-mode (Un-Mode): The Zen way of looking at things

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...

Decidability

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:

For formal systems with lengthening rules only, there does exist a decision procedure.
For formal systems with lengthening and shortening rules, there may or may not be. What does your intuition tell you?

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.

Alphabet: {t, q, C, –}
Syntax: The strings in the language are described by the pattern (yeah, we're getting technical):
```
-⁺t-⁺q-⁺ |  C-⁺
```
Inference Rules: Let x, y, and z be strings of one or more hyphens:

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):

Consistency

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.

Alphabet: {p, q, –}
Syntax: The strings of the language have the form of one or more hyphens followed by p followed by one or more hyphens followed by q followed by one or more hyphens.
Inference Rules: Let x and y be strings of one or more hyphens:

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".

Completeness

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:

If the formal system is powerful enough to capture all the things we do in arithmetic, you can represent a statement (call it G) that asserts its own non-theoremhood.
- If G really is a theorem, your system is inconsistent!
- If G is not a theorem, your system is incomplete!
So you can't have both. Is this really surprising?
Normally we take the latter case, that is, we take G to be true and say the system is incomplete because there are true statements that just can't be proven.
So we are doomed to always be incomplete: systems like the pq-system are consistent and complete under weak interpretations, so they are incomplete for arithmetic by virtue of their weakness. But once a system is strong enough to formalize the reasoning we do in full-blown arithmetic, it becomes incomplete by virtue of its strength.
Hofstadter's analogy with records and record players is beautiful here.
- A (hi-fi) record player that tries to playing every possible sound can't actually play its own self-breaking sound, so it is incomplete by virtue of its strength.
- A (low-fi) record player that refuses to play all sounds (in order to avoid destruction from its self-breaking sound) is incomplete by virtue of its weakness.