needed in proving that such a typographical property holds. In other words,
if properties of integers are not used-or if only a few extremely simple
ones are used-then we could achieve the goal of proving TNT consistent,
by using means which are weaker than its own internal modes of reasoning.
This is the hope which was held by an important school of mathemati-
cians and logicians in the early part of this century, led by David Hilbert.
The goal was to prove the consistency of formalizations of number theory
similar to TNT by employing a very restricted set of principles of reasoning
called "finitistic" methods of reasoning. These would be the thin rope.
Included among finitistic methods are all of propositional reasoning, as
embodied in the Propositional Calculus, and additionally some kinds of
numerical reasoning. But Coders work showed that any effort to pull the
heavy rope of TNT's consistency across the gap by using the thin rope of
finitistic methods is doomed to failure. Codel showed that in order to pull
the heavy rope across the gap, you can't use a lighter rope; there just isn't a
strong enough one. Less metaphorically, we can say: Any system that is strong
enough to prove TNT's consistency is at least as strong as TNT itself. And so
circularity is inevitable.(^230) Typographical Number Theory