Definition
Typographical Number Theory (TNT) is Hofstadter's formal system in Gödel, Escher, Bach, introduced in Topic 8. It is essentially Peano arithmetic in string-rewriting form. Its alphabet includes the numeral 0, the successor S, variables, +, ×, parentheses, the propositional connectives, the quantifiers ∀ and ∃, and the scope colon. Its axioms encode addition, multiplication, induction, and the basic Peano properties. Its rules of inference extend propositional logic with quantifier rules.
Why it matters
How it works
TNT formulas are built from the alphabet via recursive grammar rules — atoms are equations between terms (where terms are built from 0, S, +, ×, and variables); complex formulas combine atoms with connectives and quantifiers. The five axiom schemes encode 0 has no predecessor, successor is injective, addition is recursive, multiplication is recursive, induction. Inference rules: propositional rules plus universal generalization, existential introduction, and the related quantifier rules. Theoremhood is undecidable; consistency cannot be proved inside TNT itself.