The TNT system is a complete formal system
for dealing with number theory. It was used in GEB
by Douglas Hoefstadter
to help explain Gödel's Theorem
, among other things
See "ASCII TNT System" in TNT for the version of it I came up with for use outside of the book.