Tags:
General,
science,
Biography & Autobiography,
music,
Computers,
Artificial intelligence,
Genres & Styles,
Philosophy,
Art,
Science & Technology,
Mathematics,
Individual Artists,
Classical,
Logic,
Symmetry,
Bach; Johann Sebastian,
Metamathematics,
Intelligence (AI) & Semantics,
G'odel; Kurt,
Escher; M. C
get it.
Just try it out a bit-the main thing is for you to get the flavor of this MU -puzzle. Have fun.
Theorems, Axioms, Rules
The answer to the MU-puzzle appears later in the book. For now, what important is not finding the answer, but looking for it. You probably hay made some attempts to produce MU. In so doing, you have built up your own private collection of strings. Such strings, producible by the rules, are called theorems . The term "theorem" has, of course, a common usage mathematics which is quite different from this one. It means some statement in ordinary language which has been proven to be true by a rigorous argument, such as Zeno's Theorem about the "unexistence" of motion, c Euclid's Theorem about the infinitude of primes. But in formal system theorems need not be thought of as statements-they are merely strings c symbols. And instead of being proven , theorems are merely produced , as if F machine, according to certain typographical rules. To emphasize this important distinction in meanings for the word "theorem", I will adopt the following convention in this book: when "theorem" is capitalized, its meaning will be the everyday one-a Theorem is a statement in ordinary language which somebody once proved to be true by some sort of logic argument. When uncapitalized, "theorem" will have its technical meaning a string producible in some formal system. In these terms, the MU-puzzle asks whether MU is a theorem of the MIU -system.
I gave you a theorem for free at the beginning, namely MI. Such "free" theorem is called an axiom -the technical meaning again being qui different from the usual meaning. A formal system may have zero, or several, or even infinitely many axioms. Examples of all these types v appear in the book.
Every formal system has symbol-shunting rules, such as the four rules of the MIU -
system. These rules are called either rules of production or rules of inference . I will use both terms.
The last term which I wish to introduce at this point is derivation. Shown below is a derivation of the theorem MUIIU :
(1) MI
axiom
(2) MII
from (1) by rule II
(3) MIII
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
A derivation of a theorem is an explicit, line-by-line demonstration of how to produce that theorem according to the rules of the formal system. The concept of derivation is modeled on that of proof, but a derivation is an austere cousin of a proof. It would sound strange to say that you had proven MUIIU , but it does not sound so strange to say you have derived MUIIU .
Inside and Outside the System
Most people go about the MU-puzzle by deriving a number of theorems, quite at random, just to see what kind of thing turns up. Pretty soon, they begin to notice some properties of the theorems they have made; that is where human intelligence enters the picture. For instance, it was probably not obvious to you that all theorems would begin with M , until you had tried a few. Then, the pattern emerged, and not only could you see the pattern, but you could understand it by looking at the rules, which have the property that they make each new theorem inherit its first letter from an earlier theorem; ultimately, then, all theorems' first letters can be traced back to the first letter of the sole axiom MI -and that is a proof that theorems of the MIU -system must all begin with M .
There is something very significant about what has happened here. It shows one difference between people and machines. It would certainly be possible-in fact it would be very easy-to program a computer to generate theorem after theorem of the MIU -
system; and we could include in the program a command to stop only upon generating U .
You now know that a computer so programmed would never stop. And this does not amaze you. But what if you asked a friend to try to generate U ? It would not surprise
Lisa Black
Margaret Duffy
Erin Bowman
Kate Christensen
Steve Kluger
Jake Bible
Jan Irving
G.L. Snodgrass
Chris Taylor
Jax