Definition
The pq-system is a toy formal system in Gödel, Escher, Bach Topic 2. Its symbols are p, q, and the hyphen -. Its axiom schema is xp-qx- for any string x of hyphens. Its single rule: from theorem xpyqz derive xpy-qz-. Under the interpretation "hyphens are integers, p is plus, q is equals," every theorem decodes to a true addition equation, and every true addition equation decodes from some theorem.
Why it matters
How it works
The axiom schema generates infinitely many base theorems: -p-q-- (1+1=2), -p--q--- (1+2=3), --p-q--- (2+1=3), etc. The rule takes any theorem and extends its middle and right parts by one hyphen each, producing longer theorems. By induction, every theorem has the form xpyqz where |x| + |y| = |z| — exactly the addition relation. The isomorphism is structural: the rule preserves the equation, and the axioms instantiate the equation with one term equal to 1.