*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] The violation of type restrictions by the Goedel numbering (or encoding) function*From*: Ken Kubota <mail at kenkubota.de>*Date*: Mon, 4 Jan 2016 18:00:13 +0100

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

- Previous by Date: Re: [isabelle] Isabelle2016-RC0 - default output buffers
- Next by Date: Re: [isabelle] Isabelle2016-RC0 - default output buffers
- Previous by Thread: Re: [isabelle] Isabelle2016-RC0 - does not exit on Linux
- Next by Thread: [isabelle] Deep embedding of natural deduction?
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list