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.