(2) (2) <~P>
(3)
(4) <~Q3~P>.
(5) <~P^Q>
(6) <~Q3~~ P>.
(V) ]
(8) ~Q
push
Ganto's axiom
separation
contrapositive
separation
contrapositive
push again
premise
The Propositional Calculus
197
(9)
<~Q3~P>.
carry-over of line 4
(10)
~P
detachment
(11)
<~Q3~~ P>.
carry-over of line 6
(12)
~~P
detachment (lines 8 and 11)
(13)
<~Pa~~P>
joining
(14)
<~p v ~~P>
De Morgan
(15)
]
pop once
(16)
<~Qz>~**
vc:~3b:(b+b)=c ~3c:Sc=d
OPEN FORMULAS contain at least one free variable.
Examples: — c=c b=b <¥b:b=bn — c=c>
CLOSED FORMULAS (SENTENCES) contain no free variables.
Examples: 50=0 ~¥d:d=0 3c:<¥b:b=bA~c=c>
Typographical Number Theory
222
This completes the table of Rules of Formation for the well-formed formulas of TNT.
A Few More Translation Exercises
And now, a few practice exercises for you, to test your understanding of the notation of
TNT. Try to translate the first four of the following N-sentences into TNT-sentences, and
the last one into an open formed formula.
All natural numbers are equal to 4.
There is no natural number which equals its own square.
Different natural numbers have different successors.
If 1 equals 0, then every number is odd.
b is a power of 2.
The last one you may find a little tricky. But it is nothing, compared to this one:
b is a power of 10.
Strangely, this one takes great cleverness to render in our notation. I would caution you to
try it only if you are willing to spend hours and hours on it — and if you know quite a bit
of number theory!
A Non typographical System
This concludes the exposition of the notation of TNT; however, we still left with the
problem of making TNT into the ambitious system which we have described. Success
would justify the interpretations which we given to the various symbols. Until we have
done that, however, particular interpretations are no more justified than the "horse-apple
happy" interpretations were for the pq-system's symbols.
Someone might suggest the following way of constructing TNT: (1|) Do not have
any rules of inference; they are unnecessary, because (2) We take as axioms all true
statements of number theory (as written in TNT-notation). What a simple prescription!
Unfortunately it is as empty as instantaneous reaction says it is. Part (2) is, of course, not
a typographical description of strings. The whole purpose of TNT is to figure out if and
how it is possible to- characterize the true strings typographically.
The Five Axioms and First Rules of TNT
Thus we will follow a more difficult route than the suggestion above; we will have
axioms and rules of inference. Firstly, as was promised, all of the rules of the
Propositional Calculus are taken over into TNT. Therefore one theorem of TNT will be
this one:
**