### 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 [)
- ] - Right bracket. (In everything, you need to type ])
- ^ - 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

SupposeRULE OF SPECIFICATION:

*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*.)

SupposeRULE OF GENERALIZATION:

*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.)

SupposeRULE OF INTERCHANGE

*u*is a variable. Then the strings

*Vu:~*and

*~Eu:*are interchangeable anywhere inside any theorem.

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.RULE OF EXISTENCE

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.

SupposeRULE OF INDUCTION

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

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