[isabelle] Representation of meta-mathematics in natural deduction (including Isabelle) and Hilbert-style systems (Church and Andrews)



Dear Members of the Research Community,

Referring to publications by Alonzo Church, Peter B. Andrews and Lawrence C. 
Paulson, please allow me to comment on some remarks by David Cock, Lawrence C. 
Paulson, Markus Wenzel and Andrei Popescu, available at

	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-October/msg00019.html
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-October/msg00029.html
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-October/msg00030.html
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-September/msg00176.html
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-September/msg00187.html


The phenomenon of schematic variables in Isabelle, as addressed by David Cock, 
seems to coincide with the concept of syntactical variables in the works of 
Alonzo Church and Peter B. Andrews. The basic idea is that the same kind of 
proof can be carried out with certain or all possible substitutions for the 
schematic or syntactical variable, and due to its nature it must be a free 
"variable".

However, there also seems to be a difference in the way this idea is 
formalized, leading to different results.

In the works of Alonzo Church and Peter B. Andrews, syntactical variables 
always indicate a metatheorem of the meta-language: "In making metamathematical 
(syntactical) statements, we shall use bold capital letters as variables for 
well-formed formulas, and bold small letters as variables for variables [...]." 
[Church, 1940, p. 57] "We shall prove theorems in both the object language and 
the meta-language. Indeed, in the meta-language we shall prove theorems about 
the theorems of the object language. For emphasis, we may call a theorem of the 
meta-language a metatheorem." [Andrews, 2002, p. 11] "We shall now prove 
certain theorem schemata [...] of Q0." [Andrews, 2002, p. 215]

So the object language and the meta-language are always clearly separated, as 
the meta-language is "meta", in other words "above" the object language, and 
therefore, strictly speaking, outside of the mathematical language.

This is reflected by the fact that Andrews consequently distinguishes 
metatheorems from theorems of the object language by the use of bold letters 
for syntactical variables. (And, if I am not mistaken, only metatheorems employ 
informal words like "if" and "then" instead of logical symbols only [cf. 
Andrews, 2002, p. 224 (5224 = Modus Ponens)]; only metatheorems use the set of 
hypotheses [cf. ibid.]; and only metatheorems have restrictions, i.e., 
"provided that A is free for x in B" [Andrews, 2002, p. 224 (5226)].)

With his high accuracy, Andrews sets forth the path of Church's approach which 
is known for its "precise formulation of the syntax" [Paulson, 1989, p. 5].

It seems to me at the first glance that in Paulson's system Isabelle, in which 
a new kind of variable (schematic variables) is introduced, the separation of 
the object language and the meta-language is not as strict as in the works of 
Alonzo Church and Peter B. Andrews. There are three reasons for this impression.

First, it seems that metatheorems can be inferred directly in Isabelle and 
later instantiated for a concrete case by substitution, as indicated in the 
e-mail by David Cock. But inference should not work with metatheorems, since 
with purely mathematical means (namely, those of the object language) this is 
not possible. For example, in my (still unpublished) system R0 described at

	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00170.html

metatheorems are represented by files containing the proof templates, but for 
each individual case the proof has to be carried out again (technically 
implemented through file inclusion). Of course, there are theorems about 
general properties that can be instantiated for concrete cases. For example, I 
proved some property on groups in general and then transferred it to a concrete 
group. But this does not work with metatheorems (without artificially enhancing 
and, hence, violating the object language), because the mathematical language 
(the object language) simply does not provide the means for proving 
metatheorems or transferring (instantiating) them to theorems of the object 
language.

Second, the introduction of schematic variables only (without the introduction 
of names for the symbols of the object language in the meta-language) in 
Isabelle supposedly takes place in the same logical sphere (computational 
namespace) as the object language. In contrast, Church and Andrews emphasize 
that the names for the symbols of the object language in the meta-language are 
only the same for practical reasons, but logically belong to a different 
sphere: "Moreover we shall adopt the customary, self-explanatory, usage, 
according to which symbols belonging to the formal language serve in the syntax 
language (English) as names for themselves, and juxtaposition serves to denote 
juxtaposition." [Church, 1940, pp. 57 f.] "We shall use formulas of the object 
language as names for themselves in the meta-language." [Andrews, 2002, p. 11] 
Thus, carrying out a proof in the object language is something entirely 
different than expressing in the meta-language (i.e., by means of 
arithmetization of the object language) the fact that this proof can be carried 
out. Hence, through metatheorems, additional knowledge is obtained, but 
metatheorems cannot replace the theorems of the object language nor otherwise 
can meta-language substitute the mathematical language (the object language) 
itself.

Third, the strict distinction of the object language and the meta-language does 
not seem to be a criterion for the development of Isabelle, as the term 
"meta-logic" in the context of Isabelle is used for the _technical_ 
meta-language only, in which specific logics can be specified and implemented, 
but not in the sense of the _mathematical_ meta-language: "A calculus of logics 
is often called a logical framework; I prefer to speak of a meta-logic and its 
object-logics. Isabelle-86 required a precise meta-logic suited to its aims and 
methods. A fragment of higher-order logic (called M here for 'meta') now serves 
this purpose." [Paulson, 1988, p. 3]


The lack of a strict distinction between object language and meta-language 
seems inherent to natural deduction (and not only to Isabelle). Alonzo Church 
and Peter B. Andrews use an axiomatic (Hilbert-style) deductive system, whereas 
Lawrence C. Paulson's Isabelle is clearly a natural deduction system, since it 
allows the use of multiple deduction symbols (turnstiles) per line of a proof 
or per theorem. In Andrews' Hilbert-style system Q0, each line or each theorem 
has exactly one occurrence of the deduction symbol.

In both his 1988 and 1989 articles Lawrence C. Paulson explicitly refers to 
Peter B. Andrews' logic Q0: "Andrews [1] has written a book covering 
higher-order logic. Here is a brief sketch of a fragment called M, which will 
be our meta-logic." [Paulson, 1988, p. 4] "Andrews [1] presents a formulation 
based on equality." [Paulson, 1989, p. 14]

Nevertheless, in these articles no principle reasons are given for why Isabelle 
was implemented as a natural deduction system, but only a practical one: 
"Church's axiom system is now antiquated, largely dating back to Principia 
Mathematica. There are improved formulations but most use the Hilbert style. 
Natural deduction is far superior for automated proof." [Paulson, 1989, p. 3]

From the point of view of axiomatic (Hilbert-style) deductive systems, the 
theorems of the proofs of (historical) natural deduction were primarily 
metatheorems. For example, the classical rules and inferences given at

	http://plato.stanford.edu/archives/win2014/entries/proof-theory-development/#NatDedSeqCal
	http://plato.stanford.edu/archives/win2014/entries/reasoning-automated/#NatDed

are all metatheorems.

But if principle questions about the expressiveness of the mathematical 
language are concerned, they have to prevail over practical (technical) 
questions.


Maintaining the distinction between object language and meta-language, Goedel's 
First Incompleteness Theorem (and hence, the Second) does not work in Peter B. 
Andrews' logic Q0. Dealing with Goedel's First Incompleteness Theorem 
seriously, one cannot simply ignore the fact that this proof fails in one of 
the most important mathematical systems currently available to the public. As 
mentioned earlier at

	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00170.html

step 7101.4 has no syntactic justification [cf. Andrews, 2002, p. 314 (7101)], 
since "there is no rule of inference from a theorem to the existence of its 
proof in the object language." [Kubota, 2013, p. 9] Neither the basic rules of 
inference of Q0, R and R' [cf. Andrews, 2002, pp. 213 f.], nor any derived 
rules can be used to infer 7101.4.

In Paulson's proof, for this step (for which in Andrews' proof only some 
implicit rule is used) the theorem 'proved_iff_proved_PfP' - called (P) in my 
article - is required, which is the result of a long proof [cf. Kubota, 2015, 
pp. 8 f., 19]. I do not see any way of proving such a theorem in a 
Hilbert-style system.

Independently, James R. Meyer has raised the same concern: "[T]he result, as 
for Åwierczkowski's proof, is an illogical confusion of meta-language and the 
language of HF. [...] Paulson does not include any computer code that proves 
that this cannot result in an illogical confusion of meta-language and 
object[ ]language." [Meyer, 2015, p. 11]

If Professor Paulson decides to respond to this critique (possibly including 
those in section 3.8), I would be interested in the answer, too, as my 
communication with him was dominated by misunderstandings obviously caused by 
different interpretations of the term "meta-language", as outlined above, such 
that the main question remained unanswered: "3. Is the object language strictly 
separated from the meta-language [...], and how is this done?" [Kubota, first 
e-mail to Lawrence C. Paulson, May 22, 2015.] I had already previously written 
(referring to the proofs of Andrews and Rautenberg): "It should be noted that 
the confusion of language levels in this proof is not specific to the work of 
Peter B. Andrews or higher-order logic or type theory, but also appears in 
other â set-theoretic â presentations of the proof of GÃdel's Incompleteness 
Theorem." [Kubota, 2013, p. 10]

The philosophical background is that both Goedel's First Incompleteness Theorem 
("I am not provable") as well as Russell's paradox ("the set of all sets that 
are not members of themselves") have the two constitutive properties of 
antinomies, self-reference and negation. The self-reference in these cases 
cannot be construed without the violation of the formal language such as the 
confusion of object language and meta-language or disregarding the types.


Furthermore, I would like to comment on implementation issues.

Markus Wenzel wrote: "My impression is that the 'Consistency Club' is presently 
empty: none of the major ITP [Interactive Theorem Proving] systems are 
absolutely well-defined and correctly implemented in every respect. Note that 
HOL Light is often quoted [a]s being really small and formally well-understood, 
but it resides in the unsafe environment of the OCaml top[ ]level: users need 
to refrain from playing dirty tricks in ML."

Andrei Popescu noted: "The logic kernel consists of the inference rules and the 
definitional mechanisms, regardless of where they are located in the 
implementation. A small logic kernel is an implementation-independent virtue of 
Isabelle/HOL as well as of all the Gordon-HOL systems."

A technical meta-logic as in the case of Isabelle or technical meta-languages 
like ML have the advantage of offering the easy implementation and comparison 
of several logics. But this advantage is relevant for the experimental stage 
only. As for the final implementation of the particular preferred logic, I 
would advise against using some kind of meta-logic or meta-language, as 
additional features may weaken the rigor of (or even create an inconsistency 
in) the logical kernel, but would suggest restricting oneself to the _direct_ 
encoding of the logic in order to preserve logical rigor or necessity. This 
implies the use of a purely imperative computer programming language without an 
implicit type system for the mathematical objects to be represented (i.e., C++).

The logical kernel should be as small as possible in order to guarantee logical 
rigor, and should be strictly separated from other software layers like user 
interface, proof tactics etc. In my draft I used John Harrison's HOL Light with 
its small logic kernel as point of reference: "In summary, if 'HOL Light is 
[...] a clean and simplified version of Mike Gordon's original HOL system' 
[Harrison, 2009, p. 60], then R0 is even cleaner and simpler than HOL Light and 
follows consequently the path of maximising logical rigor by reductionism." 
[Kubota, 2015a, p. 15]

Also, in order to preserve logical correctness, including the clear distinction 
of the object language and the (mathematical) meta-language, a Hilbert-style 
system should be used.

All three considerations were implemented by encoding a further development of 
Peter B. Andrews' logic Q0, my own logic R0, which allows for type variables 
and binding of type variables with lambda, directly (without a technical 
meta-logic) into an extremely small logical kernel: "In the R0 implementation, 
the concept of a simple minimum core logic is also applied to the technical 
implementation, and the program containing the logical core itself does not 
exceed 2,500 lines of code (even including the routines for formatting and 
displaying the formulas, and administration overhead)." [Kubota, 2015a, p. 15]

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 (2013). On Some Doubts Concerning the Formal Correctness of GÃdel's 
Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 978-3-943334-04-3. 
DOI: 10.4444/100.101. See: http://dx.doi.org/10.4444/100.101

Kubota, Ken (2015). GÃdel Revisited. Some More Doubts Concerning the Formal 
Correctness of GÃdel's Incompleteness Theorem. Berlin: Owl of Minerva Press. 
ISBN 978-3-943334-06-7. DOI: 10.4444/100.102. See: 
http://dx.doi.org/10.4444/100.102

Kubota, Ken (2015a). 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

Meyer, James R. (2015), "A Fundamental Flaw in An Incompleteness Proof by 
StanisÅaw Åwierczkowski" (v2 30 Apr 2015). Available online at 
http://www.jamesrmeyer.com/pdfs/ff_swierczkowski.pdf (November 28, 2015).

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 
(November 28, 2015).

Paulson, Lawrence C. (1989), "A Formulation of the Simple Theory of Types (for 
Isabelle)". Available online at 
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (November 28, 2015).

____________________

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.