Details

Before exploring this system, you should investigate the MIU-system and the pq-system (see links below).

This Demonstration lets you explore the tq-system [1], an example of a formal system introduced by Douglas Hofstadter in chapter 3 of [1] as a means of illustrating the important elements of formal systems (axioms, theorems, rules of inference), the mechanical and intelligent modes of treating a formal system, and the concept of a decision procedure.

Axiom schema: , where is a string composed of hyphens only.

Theorem production rule: , where , , and are strings composed of hyphens only.

Use the upper controls to identify different axioms and theorems of the system. See the patterns they follow to eventually discover a decision procedure for the system: can you tell whether a given string is a theorem before using the sliders to check? (This is thinking about the system, using "intelligent" mode: I-mode.) It will also help to use "mechanical" mode: M-mode, setting up an axiom according to the recipe (axiom schema) and then pushing the "apply rule of inference" button repeatedly to generate a sequence of theorems from it. When you think you understand the system, use the lower controls to check your answer and investigate the system from other viewpoints.

The lower slider implements an algorithm for generating all possible theorems of the system, at each step adding one axiom (shown in blue) to a "theorem bucket" and applying the rule of theorem production to all theorems that were already in the bucket, possibly generating new theorems (shown in green). This method is guaranteed to generate any given theorem of the system... eventually. Older axioms/theorems are shown in lighter colors to allow the new axiom and theorems to stand out visually.

If the "CTheorems" option is checked, an additional theorem production rule is implemented: . Any theorems generated by the new rule are shown below the regular theorem bucket display. Can you figure out the meaning of these new theorems? What is the first C-type theorem generated? Will ever be generated as a theorem? Can you describe the set of C-type non-theorems, C-strings that will never be generated?

Reference:

[1] Douglas R. Hofstadter, Gödel, Escher, Bach: An Eternal Golden Braid, New York: Basic Books, 1979.