### 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 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.

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.