One page 212, Hofstadter considers the problem of translating the
sentence "5 is prime" into TNT.
He proposes the following translation:
These observations raise the question of what it actually means to
translate a sentence into TNT.
I think it is straightforward to say what it means to translate a
predicate into TNT: a formula is a translation of a predicate if it
expresses
that predicate.
But I don't think it is quite so clear what it means to translate a
sentence into TNT; one could argue that any formula that is true under
the intended interpretation is a translation of a true sentence, and
any formula that is false under the intended interpretation is a
translation of a false sentence.
In this sense Hofstadter's proposed translation is correct, since it
is true under the intended interpretation and "5 is prime" is a true
sentence.
I don't see any logical reason why "~G" could not be a theorem of TNT,
although as Hofstadter notes it would be very strange if it were, as
it would imply that the natural numbers are not, in fact, a model of
TNT.
Elsewhere Hofstadter seems to have a different definition of
consistency in mind.
For example, on page 229 he says
There is a third notion of consistency, semantic consistency, that is
sometimes used: a system is said to be semantically consistent iff it
has a model.
Since TNT has a model (the natural numbers), it is semantically
consistent.
Let us now consider how these different notions of consistency pertain
to the question of whether "~G" could be a theorem of TNT.
First, note that if TNT were syntactically inconsistent it
would mean that every formula of TNT is a theorem, and if TNT were
Hofstadter inconsistent it would mean that there is some theorem of
TNT that is false under the intended interpretation.
Thus, it seems to me that Hofstadter consistency is a much stronger
assumption than syntactic consistency (as already noted, Hofstadter
consistency implies syntactic consistency).
On page 451, Hofstadter says
it follows that
"~G" is not a theorem of TNT.
Are there undecidable formulas of TNT?
On page 459, Hofstadter says that it might be possible that there
are no undecidable formulas of TNT:
"Perhaps every consistent formalization of number theory which humans
invent will imply the existence of supernaturals, by being
omega-inconsistent.
This is a queer thought, but it is conceivable.
If this were the case--which I doubt, but there is no disproof
available--then G would not have to be undecidable.
In fact, there might be no undecidable formulas of TNT at all.
There could simply be one unbifurcated theory of numbers--which
necessarily includes supernaturals.".
I think Hofstadter is wrong here; I think there must be undecidable
formulas of TNT.
Even if "~G" were a theorem of TNT, there other sentences, such as the
Rosser sentence, that can be shown to be undecidable on the weaker
assumption of syntactic consistency, rather than omega-consistency
(note that omega-consistency implies syntactic consistency).
Names and Quotation
To talk about TNT it is useful to assign names to formulas, where a
name is an arbitrary string of uppercase and lowercase letters.
Here I describe some notation for naming formulas.
Given a formula and its name, I will refer to the name by enclosing the
name in single-quotation marks, and I will refer to the formula to which
the name is assigned by enclosing the name in double-quotation marks.
For example, let us assign the name 'Bletch' to the formula '0=0'.
The first character of 'Bletch' is 'B', and the first character of
"Bletch" is '0'.
The formulas "Bletch" and '0=0' are identical.
It is also useful to be able to define new formulas in terms of
previously named formulas.
To allow such definitions, let us extend the TNT grammar so that names
can stand in place of formulas, and let us call the formulas that
result from this extended grammar "extended formulas".
I will enclose an extended formula in single-quotation marks to refer
to the extended formula itself, and I will enclose an extended formula
in double-quotation marks to refer to the formula that results when
all the names in the extended formula are replaced with the formulas
to which the names are assigned.
For example, consider the extended formula 'Ex:~Bletch'.
The last character of 'Ex:~Bletch' is 'h', and the last character of
"Ex:~Bletch" is '0'.
The formulas "Ex:~Bletch" and 'Ex:~0=0' are identical.
Note that one can assign names to formulas that are defined using
extended formulas.
For example, let us assign the name 'Bar' to the formula "Ex:~Bletch".
The first character of 'Bar' is 'B', the first character of "Bar" is
'E', the last character of 'Bar' is 'r', and the last character of
"Bar" is '0'.
The formulas "Bar", "Ex:~Bletch", and 'Ex:~0=0' are all identical.
In what follows, we will write
"Bletch" = '0=0'
to indicate that the formula '0=0' is assigned the name 'Bletch'.
In [Quine, 1987], under the entry "Use versus Mention", Quine defines
a notion of quasi-quotation that is similar to my double-quotation
mark notation.
Substitution
To talk about TNT it is useful to be able to construct new formulas
by substituting terms for free variables in previously named formulas.
Here I describe two different notations for describing substitution.
Curly-bracket substitution notation
Hofstadter defines a curly-bracket substitution notation as follows:
"Let us abbreviate a well-formed formula in which the variable
'a' is free by the following notation: "X{a}".
(There may be other free variables, too, but that is irrelevant.)
Then the notation "X{Sa/a}" will stand for that string but with every
occurrence of 'a' replaced by 'Sa'.
Likewise, "X{0/a}" would stand for the same string, with each
appearance of 'a' replaced by '0'.".
(page 224)
Later on Hofstadter uses the curly-bracket notation with
multiple free variables, but he never explains exactly what he means
by this notation.
The notation is ambiguous when multiple variables are used, because
the order in which the substitutions are performed is important.
For example, suppose we define
"Square" = '(a*a)=b'.
Consider the formula "Square{b/a,a/b}".
If the substitutions are performed simultaneously, then
"Square{a/b,b/a}" = '(b*b)=a'.
If we first substitute 'b' for 'a', and then substitute 'a' for 'b',
then
"Square{a/b,b/a}" = '(a*a)=a'.
If we first substitute 'a' for 'b', and then substitute 'b' for 'a',
then
"Square{a/b,b/a}" = '(b*b)=b'.
Let us resolve the ambiguity by assuming that the substitutions are to
be performed simultaneously.
Note that the order in which the variables occur in the curly brackets
is irrelevant, and that not all of the free variables need to be
listed.
For example,
"Square" = "Square{a}" = "Square{b}" = "Square{a,b}" =
"Square{b,a}" = '(a*a)=b'.
If we want to substitute "S0" for "a" in "Square", we could denote
this by
"Square{S0/a}" = "Square{S0/a,b}" = "Square{b,S0/a}" = "(S0*S0)=b".
If we want to substitute 'SS0' for 'a' and '0' for 'b' in 'Square', we
could denote this by
"Square{SS0/a,0/b}" = "Square{0/b,SS0/a}" = '(S0*S0)=0'.
Often people define a substitution notation like the curly-bracket
notation, but without the requirement that the variables listed in the
curly bracket be free variables of the formula.
(See section 1.1.6, "Substitutions in a propositional formula", in
[Cori, 2000] for a substitution notation defined along these lines.)
Square-bracket substitution notation
The curly-bracket notation can cause problems when the term being
substituted contains variables that are bound in the formula.
For example, define a formula
"Even" = 'Ea:(a+a)=x',
which asserts that 'x' is even.
Then
"Even{y/x}" = 'Ea:(a+a)=y'
asserts that 'y' is even.
But
"Even{a/x}" = 'Ea:(a+a)=a'
does not assert that 'a' is even; rather, it is a closed formula, which
expresses the true statement that there is a number, namely 0, equal
to twice itself.
To get around this problem, I will define a new square-bracket
notation for variable substitution.
Consider a formula "Bletch" with a single free variable 'x'.
In the new notation this formula will be assigned the name 'Bletch[x]'.
Suppose we want to substitute the variable 'a' for the variable 'x'.
If 'a' is not bound in "Bletch" then we define
"Bletch[a]" = "Bletch{a/x}".
If 'a' is bound in "Bletch" then the situation is more complicated.
We first need introduce an arbitrary ordering of the variables; for
example, we could order the variables as follows:
a, b, c, ..., z, a', b', c', ..., z', a'', b'', c'', ..., z'', ...
We find the first variable in the ordering that is not equal to 'a' or
'x' and is not bound in "Bletch"; let us assume that this variable is
'b'.
We then define
"Bar" = "Bletch{b/a}",
"Bletch[a]" = "Bar{a/x}".
For example, suppose we define
"Even[x]" = 'Ea:(a+a)=x',
Then
"Even[y]" = 'Ex:(x+x)=y',
"Even[a]" = 'Eb:(b+b)=a'.
It is straightforward to generalize the square-bracket notation to
allow for the substitution of a term for a variable.
For example,
"Even[SS0]" = 'Ex:(x+x)=SS0',
"Even[(a+b)]" = 'Ec:(c+c)=(a+b)'.
We can also generalize the square-bracket notation to allow for formulas
with multiple free variables.
We will stipulate that all the free variables in the formula are to be
listed in the brackets, so the name 'X[a,b]' indicates that variables
'a' and 'b' are free in "X[a,b]", and "X[a,b]" has no other free
variables.
For example, suppose we define
"Square[a,b]" = '(a*a)=b'.
Then
"Square[S0,b]" = '(S0*S0)=b',
"Square[S0,0]" = '(S0*S0)=0'.
Note that the order of the terms enclosed in the square brackets is
important:
"Square[x,y]" = '(x*x) = y',
"Square[y,x]" = '(y*y) = x'.
The advantage of the square bracket notation is that we do not need
to keep track of which variables are bound in a formula, which makes it
easier to define new formulas in terms of old formulas.
We can make an analogy between TNT and a computer programming
language: predicates correspond to functions, and the bound variables
in a predicate defined via the square-bracket notation are analogous
to local variables.
I have written a
computer program that develops
this analogy and makes use of the square-bracket substitution
notation.
The square-bracket substitution notation is similar to a substitution
notation described on page 18 of [Smullyan, 1992], in the section
"Substitution of Variables".
Use of the curly-bracket substitution notation in GEB
Hofstadter is not always consistent in his use of the curly-bracket
substitution notation.
For example, on page 444, Hofstadter introduces a formula
"Sub{a,a',a''}", and on page 446 he defines a formula
"Arithmoquine{a'',a'}" by
"Arithmoquine{a'',a'}" = "Sub{a'',a'',a'}".
To be consistent with the above use of the curly bracket notation,
this should be
"Arithmoquine{a'',a'}" = "Sub{a''/a, a''/a', a'/a''}".
Note that one could also express these formulas in the square-bracket
notation by defining
"Sub[a,a',a'']" = "Sub{a,a',a''}",
"Arithmoquine[a'',a']" = "Arithmoquine{a'',a'}".
In this notation, it would be correct to write
"Arithmoquine[a'',a']" = "Sub[a'',a'',a']".
Tarski's definition of truth
Hofstadter relies on an intuitive understanding of what it means to
say that a formula of TNT is true under an interpretation, but it is
possible to give a rigorous definition of this notion.
Here I describe a rigorous definition of truth for formal
languages due to Alfred Tarski.
An interpretation of TNT consists of a set D, which is called
the domain of the interpretation, a pair of functions A
and M from DxD to D, a function S from D to D, a two-place relation
E on D, and a fixed element Z of D.
Let TERMS denote the set of terms of TNT, and define a set SEQ of
infinite sequences of elements of D.
Define an ordering of the variables of TNT, and let "v_n" denote the
nth variable of this ordering.
Given a sequence s in SEQ, let "s_n" denote the nth element of s.
Let us recursively define a function f from SEQxTERMS to D as
follows:
- f(s, "(t1+t2)") = A(f(s, "t1"), f(s, "t2")),
- f(s, "(t1*t2)") = M(f(s, "t1"), f(s, "t2")),
- f(s, "St") = S(f(s, "t")),
- f(s, "v_n") = s_n,
- f(s, "0") = Z.
Here s is an arbitrary sequence, and "t", "t1", and "t2", are
arbitrary terms.
Given a formula "X", we will say that a sequence s does or does not
satisfy "X" by using the following recursive definition of
satisfaction:
-
A sequence s satisfies "Ev_n:X" iff there is a sequence r that
satisfies "X" and r_i = s_i when i is not equal to n.
-
A sequence s satisfies "Av_n:X" iff s satisfies "~Ev_n~:X".
-
A sequence s satisfies "~X" iff s does not satisfy "X".
-
A sequence s satisfies "t1=t2" iff E(f(s, "t1"), f(s, "t2")).
Here "X" is an arbitrary formula and "t1" and "t2" are arbitrary terms.
Given an interpretation, we say that a formula "X" is satisfiable
iff there is at least one sequence s that satisfies "X".
Given an interpretation, we say that a formula "X" is true iff it
is satisfied by every sequence in SEQ.
We say that a formula "X" is logically valid iff it is true under
every interpretation.
Note that satisfiability, truth, and logical validity form a
hierarchy: a formula that is logically valid is true for every
interpretation, and a formula that is true for some interpretation is
satisfiable for every sequence of elements in the domain of the
interpretation.
Note: On page 207, Hofstadter says that open formulas are neither true nor
false.
The usual convention, which agrees our above definition of truth, is
that an open formula is true if its closure is true, false if the negation
of its closure is true, and neither true nor false otherwise.
For example, the open formula 'x=x' would be considered true, because its
closure 'Ax:x=x' is true.
The axioms of TNT are true under the intended interpretation, but none
of the axioms are logically valid.
An example of a logically valid formula is '<0=0|~0=0>'.
A model of TNT is an interpretation for which all the
theorems of TNT are true.
Here are some examples of interpretations of TNT:
-
The intended interpretation of TNT is the natural numbers.
For this interpretation D is taken to be the set of natural numbers, A
and M are taken to be addition and multiplication, S is taken to be
the successorship function, E is taken to be the identity relation,
and Z is taken to be the number 0.
All the theorems of TNT are true for this interpretation, so it is a
model of TNT.
For this interpretation there is a one-to-one correspondence between
numerals and elements of the domain.
-
There also are unintended models of TNT, for which the domain includes
elements that do not correspond to any numeral (Hofstadter calls such
elements "supernatural" numbers).
-
As another example of an interpretation, we could interpret TNT in the
domain of integers modulo N, where N is an arbitrary natural number.
For this interpretation D is taken to be the set of natural numbers
from 0 to N-1, A and M are taken to be addition and multiplication
modulo N, S is taken to be the successorship function modulo N, E is
taken to be the identity relation, and Z is taken to be the number 0.
Some theorems are false under this interpretation (e.g., the first
axiom, 'Ax:~Sa=0'), so it is not a model of TNT.
Since the domain is finite, there is a decision procedure for
determining whether a given formula is true under this interpretation.
I have written a
computer program
to implement this decision procedure.
One can show that every consistent system has a model.
A system is said to be categorical iff if has exactly one
model.
All models of TNT have infinite domains, as can be understood from the
following considerations.
One can show that the formula 'x=y'
represents the equality
relation.
Thus, for any pair of distinct integers n and m, the formula
'~<n>=<m>' is a theorem, so the numerals
'<n>' and '<m>' must correspond to distinct elements of
the domain.
Since there are an infinite number of numerals, there must be an
infinite number of elements of the domain.
One can show that if a system is consistent and a formula "X" is
undecidable in that theory (that is, neither "X" nor "~X" is a
theorem), then one can add either "X" or "~X" as an axiom and the
resulting system will still be consistent.
Since every consistent theory has at least one model, this result
implies that a system with an undecidable formula has at least two
models: one in which the formula is true, and one in which it is
false.
Thus, systems with undecidable formulas are not categorical.
For example, consider formal system for group theory.
In this system a formula that stated that the group product was
commutative would be undecidable, because some groups are abelian and
some are non-abelian.
By adding this formula or its negation to the system, we would
restrict the possible interpretations to abelian or non-abelian
groups.
Properties of TNT
-
TNT is syntactically consistent:
-
There is no formula "A" such that both "A" and "~A" are theorems.
-
TNT is syntactically incomplete:
-
There is a formula "G", the Gödel sentence, such that neither "G"
nor "~G" is a theorem.
-
TNT is semantically consistent:
-
TNT has a model (e.g., number theory).
-
TNT is semantically complete with respect to logical validity:
-
If a formula is logically valid, then it is a theorem.
-
TNT is undecidable:
-
There is no effective procedure for distinguishing theorems from
non-theorems.
-
TNT is not categorical:
-
The set TNT-theorems has more than one model (e.g., there are some
models in which the Gödel sentence "G" is true and other models
in which "G" is false; see [DeLong, 1998], page 182).
Expressing versus representing a predicate
Here I describe the notions of expressing and representing a predicate
in TNT.
Consider a property p that applies to natural numbers; for example, p
could be the property of being prime.
Consider a formula "P{x}" that has one free variable 'x'.
Let "<n>" denote the numeral corresponding to the natural number
n; for example,
"<0>" denotes '0',
"<1>" denotes 'S0',
"<2>" denotes 'SS0', and so forth.
Suppose that for all natural numbers n the formula "P{<n>/x}" is
true under the intended interpretation iff property p holds for n.
Then we say that "P{x}" expresses property p.
Suppose that for all natural numbers n the formula
"P{<n>/x}" is a theorem if p holds for n, and
"~P{<n>/x}" is a theorem if p does not hold for n.
Then we say that "P{x}" represents property p.
Note that if a formula represents a property then it also expresses
that property, but if a formula expresses a property it does not
necessarily represent that property.
Here are some examples:
-
The property of being zero is expressed and represented in TNT by the
formula 'x=0', since the following formulas are all theorems:
'0=0',
'~S0=0'
'~SS0=0',
'~SSS0=0', ...
-
All primitive recursive properties are expressed and represented in
TNT.
-
The property of being the Gödel number of a theorem of TNT is
expressed by the formula "Provable{x}", but this property is not
representable.
(This result is a consequence of
Gödel's first theorem.)
-
The property of being the Gödel number of a formula that is true
under the intended interpretation is neither expressible nor
representable.
(This result is a consequence of
Tarski's theorem.)
Gödel's first theorem
On page 448 Hofstadter summarizes his proof of Gödel's first
theorem:
"Is G a TNT-theorem? If so, then it must assert a truth. But what in
fact does G assert? Its own nontheoremhood. Thus from its
theoremhood would follow its nontheoremhood: a contradiction.
Now what about G being a nontheorem? This is acceptable, in that it
doesn't lead to a contradiction. But G's nontheoremhood is what G
asserts--hence G asserts a truth. And since G is not a theorem,
there exists (at least) one truth which is not a theorem of TNT.".
Hofstadter's proof relies on semantic notions like truth and
interpretation; in particular, it relies on interpreting "G" in the
domain of natural numbers.
It is also possible to prove Gödel's first theorem using purely
syntactic notions; I describe such a proof here.
Assume that we have a Gödel coding that allows us to code both
formulas and sequences of formulas as natural numbers.
Given a formula "A", let "[A]" be the numeral corresponding to the
Gödel number of "A", and
given a sequence of formulas "A1", ..., "An", let "[A1, ..., An]" be
the numeral corresponding to the Gödel number of the sequence.
We now define a series of formulas:
- "Proves{x,z}":
-
Under the intended interpretation
"Proves{[A1, ..., An]/x, [B]/z}"
is true iff "A1", ..., "An" is a
proof of "B".
The relation
expressed
by "Proves{x,z}" is primitive recursive, and "Proves{x,z}"
represents
this relation in TNT.
Thus, if "A1", ..., "An" is a proof of "B" then
"Proves{[A1, ..., An]/x, [B]/z}" is a theorem, otherwise
"~Proves{[A1, ..., An]/x, [B]/z}" is a theorem.
The formula "Proves{x,z}" is equivalent to Hofstadter's
"TNT-Proof-Pair{x,z}".
- "Quine{y,z}":
-
Under the intended interpretation,
"Quine{[A]/y,[B]/z}" is true iff "B" is the arithmoquinification of
"A"; that is, iff substituting "[A]" for all the free variables in "A"
yields "B".
The relation
expressed
by "Quine{y,z}" is primitive recursive, and "Quine{y,z}"
represents
this relation in TNT.
Thus, if "B" is the arithmoquinification of "A" then
"Quine{[A]/x,[B]/y}" is a theorem, otherwise
"~Quine{[A]/x,[B]/y}" is a theorem.
The formula "Quine{y,z}" is the same as Hofstadter's "Arithmoquine{y,z}".
- "Proves-Quine{x,y}":
-
The formula "Proves-Quine{x,y}" is defined by
"Proves-Quine{x,y}" = "Ez: <Proves{x,z}^Quine{y,z}>".
Under the intended interpretation,
"Proves-Quine{[A1, ..., An]/x, [B]/y}" is true iff "A1", ..., "An" is
a proof of the arithmoquinification of "B".
The relation
expressed
by "Proves-Quine{x,y}" is primitive recursive, and "Proves-Quine{x,y}"
represents
this relation in TNT.
Thus, if "A1", ..., "An" is a proof of the arithmoquinification of
"B", then
"Proves-Quine{[A1, ..., An]/x, [B]/y}" is a theorem, otherwise
"~Proves-Quine{[A1, ..., An]/x, [B]/y}" is a theorem.
- "U{y}":
-
The formula "U{y}" is defined by
"U{y}" = "~Ex:Proves-Quine{x,y}".
Under the intended interpretation,
"U{[B]/y}" is true iff the arithmoquinification of "B" is not a
theorem.
The predicate
expressed
by "U{y}" is not primitive recursive, and is not
representable
in TNT.
The formula "U{y}" is what Hofstadter calls "G's uncle".
- "G":
-
The formula "G", which is called the Gödel sentence, is defined by
"G" = "U{[U{y}]/y}".
Under the intended interpretation, "G" is true iff "G" is not a
theorem.
- "Proves-G{x}":
-
The formula "G" is defined by
"Proves-G{x}" = "Proves-Quine{x,[U{y}]/y}".
Under the intended interpretation,
"Proves-G{[A1, ..., An]/x}" is true iff "A1", ..., "An" is a proof of
"G".
The predicate
expressed
by "Proves-G{x}" is primitive recursive, and "Proves-G{x}"
represents
this predicate in TNT.
Thus, if "A1", ..., "An" is a proof of "G" then
"Proves-G{[A1, ..., An]/x}" is a theorem, otherwise
"~Proves-G{[A1, ..., An]/x}" is a theorem.
- "Provable{y}":
-
The formula "Provable{z}" is defined by
"Provable{z}" = "Ex:Proves{x,z}".
Under the intended interpretation, "Provable{[B]/z}" is true iff "B" is
a theorem.
The predicate
expressed
by "Provable{z}" is not primitive recursive, and is not
representable
in TNT.
Using these formulas, we will now show that if TNT is consistent then "G"
is not a theorem, and if TNT is
We will first show that if "G" is a theorem then TNT is inconsistent.
First, note that "G" can be written in the form
Suppose that there is formula "P{x}" such that "P{<n>/x}" is a
theorem for every natural number n, and "~Ax:P{x}" is also a theorem.
Then TNT is omega-inconsistent.
Suppose that property p is expressible.
Then we can define the following formulas:
It is often useful to define an arbitrary ordering of VARS; we will
take this ordering to be
Note: Hofstadter states that a quantified formula is only well-formed
if the quantified variable is free in the formula being quantified
(see page 214); usually this restriction is not imposed.
See also comments under "Compounds" on page 214.