Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] The violation of type restrictions by the Goed...

Email Gateway (Aug 22 2022 at 12:25):

From: Ken Kubota <mail@kenkubota.de>
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 mathema
[message truncated]

Last updated: Apr 24 2024 at 16:18 UTC