[isabelle] The violation of type restrictions by the Goedel numbering (or encoding) function
Dear Ramana Kumar and List Members,
Thank you for your comment at
concerning my contribution available at
I would also like to thank other members for their comments, which have been
noted. As Ramana Kumar directly addresses the crucial question, I would like to
concentrate on and answer it in section 2 further below.
1. The presentations of the proof by Andrews and Rautenberg
Syntactically, of course, in Paulson's claimed theorem 'proved_iff_proved_PfP'
> a <-> > PfP "a"
the right-hand side (PfP "a") is an object-language statement. We agree on this
I refer to the meaning ("semantically"), since I am basically trying to
summarize the (incorrect) presentations of the proof by Andrews and Rautenberg,
in which neither the claimed lemma 'proved_iff_proved_PfP' nor an equivalent
lemma is proven, but is used as a rule implicitly or explicitly justified by
its meaning; for example, in Andrews' presentation from the statement of the
left-hand side (a) the statement of the right-hand side (PfP "a") is inferred
while giving an informal argument only ("since the wff Proof represents the
numerical relation Proof" [Andrews, 2002, p. 314 (7101)]), thus violating
Andrews' own strict formal (syntactic) standards. Therefore, I previously wrote
that "step 7101.4 has no syntactic justification" at
The purpose of this passage about Andrews and Rautenberg is to show that the
presentations of the proof by both of them fail, as they do not prove the
claimed lemma 'proved_iff_proved_PfP' at all, although this would be a
So in order to verify whether Goedel's First Incompleteness Theorem can be
formally obtained, I suggest focusing on and proceeding to Paulson's
presentation discussed below.
2. The presentation of the proof by Paulson
Not only the right-hand side (PfP "a"), but also the left-hand side (a) is an
object-language statement, which in Q0 always have type 'o' (Boolean truth
values). Moreover, if the proposition 'a' has type 'o' (omicron), it cannot
have a second type "tm" (for term) unless this is identical with 'o', since in
Q0 all mathematical objects, including propositions (object-language
statements), have exactly and only one type. It is not possible in Q0 to assign
a second type to a mathematical object.
Furthermore, the type "tm" (for term) in Isabelle is intended for the notation,
which in Q0 is not part of the object language itself. The purpose of types in
Q0 is to categorize mathematical objects, but not their names. Obviously types
in Isabelle are used for non-mathematical purposes also.
If you believe that the type "tm" (for term) is definable within Q0, you could
a) negatively refute my argument that any Goedel encoding function violates
type restrictions, or
b) positively present the definition of type "tm" (for term) within Q0 on the
basis of the primitive types 'o' (omicron, for truth values) and 'i' (iota, for
individuals) only [cf. Andrews, 2002, p. 210, and Church, 1940, p. 56], as, for
example, similar to nat = (o(oi)).
In Q0, there are two kinds of definitions:
1. The first kind of definition are _metamathematical_ definitions in order to
set up the formal language, for example
- the definition of (the concept of) type symbols [cf. Andrews, 2002, p. 210] or
- the definition of (the concept of) wffs (well-formed formulae) [cf. Andrews,
2002, p. 211].
Definitions of this sort are very often "defined inductively" [Andrews, 2002,
pp. 210, 211], fostering metamathematical reasoning (i.e., via arithmetization)
about the properties of the object language. Unlike the other kind of
definition described below, they also often ramify into several possibilities,
which in the literature appear as a list "(a) [...] / (b) [...] / (c) [...]"
[Andrews, 2002, pp. 210, 211], and in the software implementation by Paulson as
a list separated by the propositional connective for the logical relation "or",
represented by the vertical bar (single pipe) '|'.
2. The second kind of definition are _mathematical_ definitions, which do
nothing more than add a shorthand (a label) to a more complex wff (well-formed
formula) in order to increase readability. Typical examples are
- the definitions of the propositional connectives and the universal and
existential quantifiers [cf. Andrews, 2002, p. 212],
- the definitions of subset, power set, union, etc. [cf. Andrews, 2002, p. 231],
- the definition of the uniqueness quantifier [cf. Andrews, 2002, p. 233], and
- the definitions of zero, the successor function, and the set of natural
numbers [cf. Andrews, 2002, p. 260].
All these definitions explicitly use the formulation "stands for" [Andrews,
2002, pp. 212, 231, 233, 260] in order to express that they are only shorthands
which can be replaced by the original wff. The single exception also implies
substitution: "Let [nat] be the type symbol (o(oi))." [Andrews, 2002, p. 260]
So if we discuss the definability of "tm" within Q0, the first kind of
definition is out of question, since it would modify Q0, and therefore go
beyond Q0 instead of remaining within.
The difference between these two kinds of definition can be demonstrated best
by looking at the different logical levels and comparing their implementation
in R0 [cf. Kubota, 2015] and Isabelle:
Logical level R0 implementation Isabelle
1. definition of the formal language C++ classes (*.cc) theories (*.thy)
2. theorems and wff definitions proofs (*.r0) theories (*.thy)
3. (Hilbert-style) metatheorems proof templates (*.r0t) theories (*.thy)
A PDF sheet is available online at:
Since Isabelle uses natural deduction, Hilbert-style (informal) metatheorems
become symbolically representable and part of the formal language itself,
although within the formal language, theorems and metatheorems are still
distinguished (with "Meta-logic" [Nipkow, 2015, p. 11] operators having a lower
precedence than the "Logic" [Nipkow, 2015, p. 11] operators). So in Isabelle,
both Hilbert-style theorems (level 2) and Hilbert-style metatheorems (level 3)
are merged into the same sphere (Isabelle theory files).
Further, unlike the R0 implementation, which uses the concept of _direct
encoding_, Isabelle provides a "logical framework; I prefer to speak of a
meta-logic" [Paulson, 1988, p. 3]. Thus, even the definition of the formal
language (the object language, defined in level 1), which is hard-coded in the
C++ source code of the R0 implementation, in Isabelle is specified in the
Isabelle theory files.
In summary, all three logical levels in Isabelle are merged into the same
sphere (Isabelle theory files), which provides advantages for the practical
purpose of automation, but also creates the danger of confusion of these
different levels in the implementation.
The first kind of definition (_metamathematical_ definitions) such as the
definition of the concept of type symbols or of the concept of wffs belongs to
The second kind of definition (_mathematical_ definitions) such as the
definition of propositional connectives belongs to level 2.
(Note that the terms "metamathematical" or "meta-language" are, depending on
the context, sometimes used for notions of level 1, sometimes for notions of
For example, the definition of propositional connectives in R0 is outsourced
into *.r0 proof files (level 2), but the (general) definition of the concept of
type symbols and the concept of wffs as such in R0 is implemented in the C++
source code (level 1), as they modify (set up) the formal language and could
not be specified at a later time (i.e., in levels 2 or 3).
(Note that in the dependent type theory R0, types are also mathematical objects
- wffs -, and definable in level 2.)
But the definition of type "tm" (for term) is exactly this kind of
_metamathematical_ definition (level 1). According to Paulson at
http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 5),
"[t]he following datatype defines the syntax of terms in the HF theory:
nominal_datatype tm = Zero | Var name | Eats tm tm
The type name (of variable names) has been created using the nominal framework."
So both "tm" and "fm" (cf. ibid.) are actually - in terms of computer science -
datatypes ("nominal_datatype"), and - in terms of mathematics -
metamathematical notions or notions of the meta-language that describe
("define[ ] the syntax of") the formal language (the object language) itself.
Paulson's implementation of the Goedel encoding function as specified at
maps from datatypes "tm" and "fm" to datatype "tm":
"class quot =
fixes quot :: "'a => tm" ("â_â")
instantiation tm :: quot
definition quot_tm :: "tm => tm"
where "quot_tm t = quot_dbtm (trans_tm  t)"
instantiation fm :: quot
definition quot_fm :: "fm => tm"
where "quot_fm A = quot_dbfm (trans_fm  A)"
In the application of a Goedel numbering function (or Goedel encoding function)
'G' to an argument 'a' as in
Ga = n
according to the restrictions on lambda application (case (b) in the definition
of wffs [cf. Andrews, 2002, p. 211]), 'G' must be a function with a valid
mathematical input (domain) type and a valid mathematical output (codomain)
type, and the input (domain) type must match the type of 'a' (which must be a
concrete mathematical type symbol of level 2).
But "tm", "fm" and "dbtm" are clearly metamathematical notions (level 1) and
not concrete mathematical type symbols (level 2) as defined in [Andrews, 2002,
p. 210], as for example an object of datatype "tm" can be a variable name
(meaning the name of the variable, i.e., the label, not the variable as a
mathematical entity itself), and, for example, this kind of datatype is used
for metamathematical reasoning based on the inner structure of terms or
formulas (which is normally not directly accessible by means of the object
language) as in lemma 'quot_Zero', lemma 'quot_Var', etc., after the definition
of function 'quot_dbtm' at
http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 16)
The names of variables (unlike the variables themselves) are not mathematical
objects, and therefore they cannot have a mathematical type such as nat =
(o(oi)). Treating metamathematical notions (level 1) as concrete mathematical
types (level 2) in construing wffs violates the type restrictions.
Consequently, the Goedel encoding function presented by Paulson is not a wff,
and 'proved_iff_proved_PfP' is not a theorem/metatheorem. One may use
arithmetization in order to gain insights about properties of the formal
language (the object language), but treating metamathematical notions as
mathematical types is an illegitimate shortcut mixing syntactical inference of
the formal language and metamathematical reasoning. The object language and the
meta-language are not strictly separated in the presentation discussed, which
would be necessary in order to guarantee logical correctness.
One cannot construe a well-formed formula by treating datatype "tm" (for term;
level 1) as a mathematical type (level 2), and this fact is reflected by the
non-definability of the Goedel encoding function presented by Paulson (or of
the datatype "tm") within Q0 or R0.
In other words, the rules for the construction of mathematical wffs
(well-formed formulae), which also preserve the type restrictions, are not
correctly implemented in Isabelle, or at least in Paulson's presentation of
Goedel's First Incompleteness Theorem using Isabelle.
Let me illustrate my general argument on the non-definability of a Goedel
numbering function (or a Goedel encoding function) with an example, and for
simplification we shall use a Goedel numbering function (instead of Paulson's
Goedel encoding function) without limiting the validity of the argument.
Let n be the Goedel number for the proposition 'a', such that
"a" = n
Using classical lambda-notation with a prefix function 'G' instead of the
quotation marks (" ") for the Goedel numbering function, we would obtain
Ga = n
Since propositions in Q0 have type 'o', and natural numbers have type 'nat'
(with nat = (o(oi)) = (i -> o) -> o; natural numbers as "equivalence classes of
sets of individuals" [Andrews, 2002, p. 260]), and since all mathematical
objects in Q0 (including propositions and natural numbers) have a single type
only, we would have a Goedel numbering function 'G'
function G :: "o -> nat"
or fully expanded, using partly Church's and Andrews' notation (ab) for type
function G :: "o -> (o(oi))"
or fully expanded, using Isabelle's notation (b -> a) for type composition only,
function G :: "o -> ((i -> o) -> o)"
But since the input (domain) type would be type 'o' (Boolean truth values), the
only possible values for arguments for 'G' could be T (true) and F (false),
hence there would be only two different Goedel numbers:
GT = g1 (definition of g1)
GF = g2 (definition of g2)
As a trivial example, we shall use the proposition 'T & T' and its Goedel
number t, such that from
Ga = n
a = (T & T)
n = t
we would obtain
G(T & T) = t
Since (T & T) = T, we would obtain
G(T & T) = GT
G(T & T) = g1
t = g1
Both propositions 'T' and 'T & T' would have the same Goedel number g1:
G(T & T) = GT = g1
However, this contradicts the concept of Goedel numbering (or Goedel encoding),
since its purpose is to encode propositions with the means of the object
language only in order to reason about them within the object language, but
with only two Goedel numbers (g1 = GT and g2 = GF) this is not possible.
So the concept of the Goedel encoding function generally violates the type
restrictions on construing mathematical wffs, as with the type of truth values
as input (domain) type there would be only two different Goedel numbers.
Note that Andrews' definition of the Goedel numbering function, of course, also
must fail. Both the definitions of Goedel numbers for type symbols [cf.
Andrews, 2002, p. 303] as well as for primitive symbols [cf. Andrews, 2002, p.
304] do not use the formulation "stands for", but "assign" [Andrews, 2002, pp.
303, 304] natural numbers, which does not match the second kind of definitions
mentioned above, although this would be the only possibility of introducing
Goedel numbers without modifying and hence violating the formal language. These
two definitions and step 7101.4 [cf. Andrews, 2002, p. 314 (7101)] are the only
occurrences in this book currently known where Andrews does not meet his own
strict syntactic standards.
Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type
Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London:
Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4.
Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In:
Journal of Symbolic Logic 5, pp. 56-68.
Kubota, Ken (2015), On the Theory of Mathematical Forms (Draft of May 18,
2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5
011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See:
Nipkow, Tobias (2015), "What's in Main" (May 25, 2015). Available online at
https://isabelle.in.tum.de/dist/Isabelle2015/doc/main.pdf (January 1, 2016).
Paulson, Lawrence C. (1988), "The Foundation of a Generic Theorem Prover".
Available online at http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf
(January 1, 2016).
This archive was generated by a fusion of
Pipermail (Mailman edition) and