Create a formal system that captures some numerical property

Create a formal system that captures some numerical property that is not included in G¨odel, Escher, Bach. Define the formal system and demonstrate that the system is purely typographical and is isomorphic to the desired numeric property.

Solution

Let us consider a simple formal system, the ab-system: Alphabet: {a, b, -} Axioms: ha-bh-, where h contains hyphens only Rule: haibj hai-bj-, where h, i, and j contain hyphens only There is a procedure called decision procedure to find a given string is a theorem of the ab-system! Because there are no shortening of rules, all theorems can be generated in increasing length. ab-system’s theorem corresponds to the true statements of the form h + i = j over natural numbers. This is an isomorphism. This system does not include in GEB but is purely typographical and is isomorphic to desired numeric system.