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.
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.
A formal system has the following components:
This is only progress toward understanding formal systems. We soooooo need to go to examples now.
The MIU-System was defined by Hofstadter in GEB.
{M, I, U}
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.
This formal system was also invented by Hofstadter in GEB.
{p, q, –}
p
followed by one or more hyphens followed by q
followed by
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 |
---p----q-------
a theorem? Why or why not?
---p-----q-------
a theorem? Why or why not?
---p--p--q-------
a theorem? Why or why not? Does this bother you? Should it?
You guessed it. This one too was invented by Hofstadter in GEB.
{t, q, –}
t
followed by one or more hyphens followed by q
followed by
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 |
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
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:
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:
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.
{t, q, C, –}
-+t-+q-+ | C-+
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.
Hofstadter invented this one, too.
{p, q, –}
p
followed by one or more hyphens followed by q
followed by
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".
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.
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.
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.
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: