Email Gateway (Aug 22 2022 at 12:00): Email Gateway (Aug 22 2022 at 12:00):From: Ken Kubota <mail@kenkubota.de>
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 unan
[message truncated]
Email Gateway (Aug 22 2022 at 12:01):From: Gottfried Barrow <igbi@gmx.com>
Greetings,
Adhering to good military protocol, I state that I don't fraternize with
the troops, of whom I command none, so I fraternize with no one, and
prefer monologue to dialog.
On 12/7/2015 10:35 AM, Ken Kubota wrote:
Dear Members of the Research Community,
I am a community-of-one, a mere observer who can type.
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
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.
Central to your email is your emphasis on the traditional phrases of
logic, "object language" and "meta-language". The problem I see with
that is that though you use the phrases to try and frame the discussion
about Isabelle, the phrases aren't used in the distribution
documentation, which is a major representation of how the primaries want
to frame the discussion.
Definitions and axioms are everything. You shouldn't be arguing
subtleties if there's no common agreement on the meaning of central
words and phrases.
In Logic and Computation, by Paulson, published 1987, Paulson was still
sticking with tradition, and wrote:
To clear up the confusion we must distinguish the meta language from
the object
language. The formal language of terms and formulae is the object
language. We
make statements about the object language in the meta language.
In 1988, only a year later, he switched to "meta-logic" and
"object-logic", as shown in the document you quote from, which I show
again below.
I've always been under the impression that Paulson did that to give
himself new or relatively unused terminology, to define specifically
what he was doing, to separate his stuff from the crowd's stuff. In
fact, if you search on "meta-logic" and "object-logic", the two compound
words don't show up much, unlike "object language" and "metalanguage".
I'm actually a bit confused. I'm inclined to believe that Larry Paulson
is who introduced their use into the language of logic, or at least,
he's who made their use "popular". I could ask him about the history of
the words, but he's a member of the set of everyone, and not to be
fraternized with.
Back to the documentation. If the authors, in the documentation, don't
use the words "object language" and "meta-language", and they do use
"meta-logic" and "object-logic", doesn't that tell us there's a
distinction they're trying to make?
That your points may be valid for some kind of general critique, that
may be true, but you can't attack a claim that a person hasn't made. You
want to talk about "object language" and "meta-language", when I only
hear them talking about "meta-logic" and "object-logic".
I think they are at fault at something. It's that they describe
Isabelle/HOL in terms of older logics, when, in my opinion, though it
draws from far and wide, it is its own standard; it defines itself, in a
very concrete way. There is something very specific to talk about.
Because they describe it in terms of other logics, to give people an
idea of what it is, people then expect it to be what they want it to be,
which usually is what the people are familiar with.
I did a search for "language", in PDF and DJVU verions of this book,
"Isabelle - A Generic Theorem Prover":
https://www.springer.com/us/book/9783540582441
https://isabelle.in.tum.de/download_past.html
http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2002.tar.gz
http://isabelle.in.tum.de/website-Isabelle2008/index.html
That book is a big part of what's in the current documentation. It was
basically intact, though split up, until at least 2008, in the docs
ref.pdf, intro.pdf, logics.pdf, and logic-ZF.pdf.
I didn't see one use of "object language" and "meta-language" in those
documents. I could have missed something.
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
You say, "Third, the strict distinction of the object language and the meta-language does not seem to be a criterion for the development of Isabelle..."
Maybe so, or maybe not, or maybe it's a lot easier to just talk about"meta-logic" and "object-logic", since they're precisely defined by Isabelle/Pure, along with the primary object-logic, Isabelle/HOL.
The beauty of proof assistants is that, unlike a logic like traditional
ZFC, at build time, the heap for Isabelle/HOL is precisely and exactly
defined. When I'm told that Isabelle/Pure is the meta-logic, I know
exactly what "meta-logic" is. In fact, my understanding of "meta-logic"
has no bearing on what the meta-logic of Isabelle/Pure is. Per binary
file, called the heap, it's locked in, assuming no randomness in the
physics of it all.
Compare that to abstract thoughts of the mind, where the outcome is
dependent on understanding.
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 athttps://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00170.html
I'm not out to critique anything that I don't understand. I'll interpret
this sentence broadly: "one cannot simply ignore the fact that this
proof fails in one of the most important mathematical systems currently
available to the public".
I think, actually, most everything gets ignored, in the grand scheme of
things. Larry Paulson put a lot of work into the ZF logic, but then it's
not used. Google introduced Dart to try and replace Javascript, but it
hasn't. They tried to displace Facebook with something-or-another. They
didn't. They're big, but not so big as to not get ignored in many of
their new ventures.
What people care about with Isabelle is this: Isabelle/HOL. It's the
result of a collective effort by many people, a product of 30 years or
so, with millions of dollars having been poured into it. Tobias Nipkow,
the wizard of mysterious low-level, under appreciated, under-the-hood
magic, teamed up with Larry Paulson and switched the emphasis to
Isabelle/HOL, which is based on the work of Mike Gordon. The large group
at TUM gave it the huge boost it needed to get to the point it is now.
Nobody cares about a raw logic. Nobody cares about raw much-of-anything.
If we work real hard, and give people a polished, or semi-polished
product, then they might care about something we have to give away, or
they may not.
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++).
You're looking at things wrong. If the rigor of the logic of
Isabelle/HOL is weakened, and it's possibly inconsistent, then what is
that? It's an opportunity for someone like you to get some bragging rights.
What did we see recently? A major accumulation of bragging rights by 3
people, though I'm not completely clear on how the bragging rights
deserve to be divvied out. There's the Czech. Will he just get a Ph.D?
No. He also gets the summa cum laude of bragging rights, for showing a
logic is inconsistent.
Scary stuff, inconsistent logics. "Falso, you stay from me! You scary
scary dude! You scare me, worse than a talking Barbie doll!!"
Really, what would be of more value? A generalized logic that stands the
test of time, such as Isabelle/Pure and Isabelle/HOL, or a very narrow
logic, such as what you advise?
How are people supposed to test the generalized logic, over many years,
if the safer route is taken. And an inconsistent logic is not a crisis
anyway. An inconsistent logic that can't be fixed with "don't do that"
is
[message truncated]
Last updated: Nov 21 2024 at 12:39 UTC