tq-System Explorer

Requires a Wolfram Notebook System

Interact on desktop, mobile and cloud with the free Wolfram CDF Player or other Wolfram Language products.

Requires a Wolfram Notebook System

Edit on desktop, mobile and cloud with any Wolfram Language product.

Contributed by: Ken Caviness (March 2011)
Open content licensed under CC BY-NC-SA



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?


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

Feedback (field required)
Email (field required) Name
Occupation Organization
Note: Your message & contact information may be shared with the author of any specific Demonstration for which you give feedback.