Typographical Number Theory (TNT) is a formal
axiom
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
atic system describing the
natural numbers
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''cardinal n ...
that appears in
Douglas Hofstadter
Douglas Richard Hofstadter (born February 15, 1945) is an American scholar of cognitive science, physics, and comparative literature whose research includes concepts such as the sense of self in relation to the external world, consciousness, an ...
's book ''
Gödel, Escher, Bach
''Gödel, Escher, Bach: an Eternal Golden Braid'', also known as ''GEB'', is a 1979 book by Douglas Hofstadter.
By exploring common themes in the lives and works of logician Kurt Gödel, artist M. C. Escher, and composer Johann Sebastian Bach, t ...
''. It is an implementation of
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
that Hofstadter uses to help explain
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research i ...
.
Like any system implementing the Peano axioms, TNT is capable of referring to itself (it is
self-referential
Self-reference occurs in natural or formal languages when a sentence, idea or formula refers to itself. The reference may be expressed either directly—through some intermediate sentence or formula—or by means of some encoding. In philoso ...
).
Numerals
TNT does not use a distinct symbol for each
natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''Cardinal n ...
. Instead it makes use of a simple, uniform way of giving a compound symbol to each natural number:
:
The symbol S can be interpreted as
"the successor of", or "the number after". Since this is, however, a number theory, such interpretations are useful, but not strict. It cannot be said that because four is the successor of three that four is SSSS0, but rather that since three is the successor of two, which is the successor of one, which is the successor of zero, which has been described as 0, four can be "proved" to be SSSS0. TNT is designed such that everything must be proven before it can be said to be true.
Variables
In order to refer to unspecified terms, TNT makes use of five
variables. These are
: a, b, c, d, e.
More variables can be constructed by adding the
prime symbol
The prime symbol , double prime symbol , triple prime symbol , and quadruple prime symbol are used to designate units and for other purposes in mathematics, science, linguistics and music.
Although the characters differ little in appearance fr ...
after them; for example,
:a′, b′, c′, a″, a‴ are all variables.
In the more rigid version of TNT, known as "austere" TNT, only
:a′, a″, a‴ etc. are used.
Operators
Addition and multiplication of numerals
In Typographical Number Theory, the usual symbols of "+" for additions, and "·" for multiplications are used. Thus to write "b plus c" is to write
: (b + c)
and "a times d" is written as
:(a·d)
The parentheses are required. Any laxness would violate TNT's formation system (although it is trivially proved this formalism is unnecessary for operations which are both commutative and associative). Also only two terms can be operated on at once. Therefore, to write "a plus b plus c" is to write either
:((a + b) + c)
or
:(a + (b + c))
Equivalency
The "Equals" operator is used to denote equivalence. It is defined by the symbol "=", and takes roughly the same meaning as it usually does in mathematics. For instance,
:(SSS0 + SSS0) = SSSSSS0
is a theorem statement in TNT, with the interpretation "3 plus 3 equals 6".
Negation
In Typographical Number Theory,
negation
In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P, \mathord P or \overline. It is interpreted intuitively as being true when P is false, and false ...
, i.e. the turning of a statement to its opposite, is denoted by the "~" or negation operator. For instance,
:~((SSS0 + SSS0) = SSSSSSS0)
is a theorem in TNT, interpreted as "3 plus 3 is not equal to 7".
By negation, this means negation in
Boolean logic
In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variable (mathematics), variables are the truth values ''true'' and ''false'', usually denote ...
(
logical negation
In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P, \mathord P or \overline. It is interpreted intuitively as being true when P is false, and false ...
), rather than simply being the opposite. For example, if I were to say "I am eating a grapefruit", the opposite is "I am not eating a grapefruit", rather than "I am eating something other than a grapefruit". Similarly "The Television is on" is negated to "The Television is not on", rather than "The Television is off", because, for example, it might be broken. This is a subtle difference, but an important one.
Compounds
If x and y are well-formed formulas, and provided that no variable which is free in one is quantified in the other, then the following are all well-formed formulas
:
Examples:
*
<0=0∧~0=0>
*
*
The quantification status of a variable doesn't change here.
Quantifiers
There are two quantifiers used:
'' ∀''
and
'' ∃''
.
Note that unlike most other
logical system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
s where quantifiers over sets require a mention of the element's existence in the set, this is not required in TNT because all numbers and terms are strictly natural numbers or logical boolean statements. It is therefore equivalent to say and
*
∃
means "There exists"
*
∀
means "For every" or "For all"
*The symbol
:
is used to separate a quantifier from other quantifiers or from the rest of the formula. It is commonly read "such that"
For example:
:
("For every number a and every number b, a plus b equals b plus a", or more figuratively, "Addition is commutative.")
:
("There does not exist a number c such that c plus one equals zero", or more figuratively, "Zero is not the successor of any (natural) number.")
Atoms and propositional statements
All the symbols of
propositional calculus
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
apart from the Atom symbols are used in Typographical Number Theory, and they retain their interpretations.
Atoms are here defined as strings which amount to statements of equality, such as
2 plus 3 equals five:
:(SS0 + SSS0) = SSSSS0
2 plus 2 is equal to 4:
:(SS0 + SS0) = SSSS0
References
* {{Citation
, last1 = Hofstadter
, first1 = Douglas R.
, title = Gödel, Escher, Bach: An Eternal Golden Braid
, publisher = Basic Books
, year = 1999
, origyear = 1979
, isbn = 0-465-02656-7
, url-access = registration
, url = https://archive.org/details/gdelescherbachet00hofs
.
Formal theories of arithmetic