TNT (thing)

ASCII TNT System

Here y'all go! The TNT system for dummies and/or people with normal character sets. For those of you not in the know, TNT is a fully functional formal system for expressing (and deriving) number theory. It is just as complete in the realm of number theory as anything else, according to the author of GEB.

---

TNT Symbology

• E - This replaces the backwards E in the book.

• V - replacement for the inverted A. I chose V, because it more closely resembles the original shape, and also because a is in use already.
• c - replacement for the symbol resembling a U rotated 90 degrees to the left.

• 0 - Zero. The numeral.

• S - The letter S.

• ( - Left parentheses.
• ) - Right parentheses.
• < - Left pointy bracket.
• > - Right pointy bracket.
• [ - Left bracket. (In everything, you need to type &#91)
• ] - Right bracket. (In everything, you need to type &#93)
• ^ - Replacement for the similarly shaped symbol in GEB.
• u - Replacement for the inverted caret.
• , - A comma.
• : - A colon.

• a - The letter A.
• ' - The prime tick.
• ~ - A tilde

• * - The multiplication operator.
• + - The addition operator.

---

TNT Strings

A string of TNT is a in the following format:

given,given,...:Expression

I will go through each of the three parts (given, colon, expression) and explain their significance.

Givens

Some examples of this section:

Ea,Va'

Read as: There exists an a, and for all a',

~Va

Read as: Not for all a, or For no a. The ~ negates.

The givens section defines any variables (in this case, the a's and the a primes') used in the expression. If you don't define it here, then it is a malformed string.

:(colon)

Read as: it is the case that,

The connector between the givens and the expression.

Expression

This is where it gets sticky, and interesting.

Some example strings:

Ea,Ea':Sa=a'*a'

That string can be read as:

There exists an a, and there exists an a-prime, where the succesor of a is equal to a' times a'.

Or, in other words, two numbers exist such that one plus one of them is equal to the square of the other. An example of such a pair is 5 and 2. 2 square is 4, and 1 plus 4 is 5.

Meanings of the Symbols

This is only one of many, theoretically infinite, meanings. It is an isomorphism between human thought processes and the system. See GEB for more on this.

• E - There exists

• V - For all
• c - Then.

• 0 - Zero.

• S - The successor of.

• ( - Left parentheses.
• ) - Right parentheses. These are used for grouping.
• < - Left pointy bracket.
• > - Right pointy bracket. More grouping.
• [ - Push into a fantasy.
• ] - Pop out of a fantasy.
• ^ - And.
• u - Or.
• , - Seperator between givens.
• : - Seperator between all givens and the expression.

• a - Free variable.
• ' - The prime tick. Used to differentiate between free variables. This is austere TNT, so we don't have b, c, d, etc.
• ~ - Negation. Read this as "not", in most cases.

• * - The multiplication operator. It is only binary. That is, you can't say: (a*a'*a''). Instead, you must say: ((a*a')*a'').
• + - The addition operator. Also binary.

Now that you know the basics, you should be able to play around with the system to some extent.

Rules of TNT

RULE OF SPECIFICATION:

Suppose u is a variable which occurs inside the string x. If the string Vu:x is a theorem, then so is x, and so are any string made from x by replacing u, wherever it occurs, by one and the same term.

(Restriction: The term which replaces u must not contain any variable that is quantified in x.)

RULE OF GENERALIZATION:

Suppose x is a theorem in which u, a variable, occurs free. Then Vu:x is a theorem.

(Restriction: No generalization is allowed in a fantasy on any variable which appeared free in the fantasy's premise.)

RULE OF INTERCHANGE

Suppose u is a variable. Then the strings Vu:~ and ~Eu: are interchangeable anywhere inside any theorem.

RULE OF EXISTENCE

Suppose a term (which may contain variables as long as they are free) appears once, or multiply, in a theorem. Then any (or several, or all) of the appearances of the term may be replaced by a variable which otherwise does not occur in the theorem, and the corresponding existential quanitfier must be placed in front.

RULES OF EQUALITY

• SYMMETRY: If r = s is a theorem, then so is s = r.
• TRANSITIVITY: If r = s and s = t are theorems, then so is r = t.

RULES OF SUCCESSORSHIP

• ADD S: If r = t is a theorem, then Sr = St is a theorem.
• DROP S If Sr = St is a theorem, then r = t is a theorem.

RULE OF INDUCTION

Suppose u is a variable, and X{u} is a well-formed formula in which u occurs free. If both Vu: and X{0/u} are theorems, then Vu:X{u} is also a theorem.

Axioms

There are five TNT Axioms.

1. Va:~Sa=0
2. Va:(a+0)=a
3. Va:Va':(a+Sa')=S(a+a')
4. Va:(a*0)=0
5. Va:Va':(a*Sa')=((a*a')+a)

---

NOTE: This may not be completely accurate, as I've written it from memory. Corrections are welcome. /msg s_alanet with them, please.