*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Representation of meta-mathematics in natural deduction (including Isabelle) and Hilbert-style systems (Church and Andrews)*From*: Gottfried Barrow <igbi at gmx.com>*Date*: Wed, 09 Dec 2015 12:10:43 -0600*In-reply-to*: <9EC8620D-E106-4989-943E-A6FBC3034411@kenkubota.de>*References*: <9EC8620D-E106-4989-943E-A6FBC3034411@kenkubota.de>*User-agent*: Mozilla/5.0 (Windows NT 6.2; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Greetings,

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.

make statements about the object language in the meta language.

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

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.

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

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

Regards, GB

**References**:

- Previous by Date: Re: [isabelle] Failing afp-2015 build
- Next by Date: [isabelle] Unification bound exceeded on "show"
- Previous by Thread: [isabelle] Representation of meta-mathematics in natural deduction (including Isabelle) and Hilbert-style systems (Church and Andrews)
- Next by Thread: [isabelle] typedef with sorts
- Cl-isabelle-users December 2015 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