[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
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00061.html

concerning my contribution available at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00057.html


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 
point.

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
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00170.html

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 
necessary step.

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:
	http://www.kenkubota.de/files/Logical_Layers_in_R0_and_Isabelle.pdf

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 
level 1.
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 
level 3.)

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
	http://afp.sourceforge.net/browser_info/current/AFP/Incompleteness/Coding.html
maps from datatypes "tm" and "fm" to datatype "tm":
"class quot =
  fixes quot :: "'a => tm"  ("â_â")

instantiation tm :: quot
begin
  definition quot_tm :: "tm => tm"
    where "quot_tm t = quot_dbtm (trans_tm [] t)"

  instance ..
end

[...]

instantiation fm :: quot
begin
  definition quot_fm :: "fm => tm"
    where "quot_fm A = quot_dbfm (trans_fm [] A)"
  
  instance ..
end"

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 
composition,
	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
and
	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.


Kind regards,

Ken Kubota


References

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 
45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 
011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: 
http://dx.doi.org/10.4444/100.10

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).

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.