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

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.

Read as:

*it is the case that,*
The connector between the givens and the 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.

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.

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.

There are five

TNT Axioms.

- Va:~Sa=0
- Va:(a+0)=a
- Va:Va':(a+Sa')=S(a+a')
- Va:(a*0)=0
- 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.*