**Mail folder:**QED**Next message:**beeson@cats.UCSC.EDU: "Re: Root Logics"**Previous message:**John Harrison: "Bourbaki's construction of the reals"**Reply:**beeson@cats.UCSC.EDU: "Re: Root Logics"**Reply:**Tobias.Nipkow@informatik.tu-muenchen.de: "Root Logics"

Date: Thu, 22 Apr 93 16:13:21 BST Message-id: <11595.9304221513@whalsay.dcs.ed.ac.uk> From: Randy Pollack <rap@dcs.ed.ac.uk> To: qed@mcs.anl.gov Cc: rap@dcs.ed.ac.uk Subject: Root Logics Sender: qed-owner Precedence: bulk

I want to say something about the Root Logic, but will motivate this by replying to Michael Beeson's recent comment: > I suggest the following organization of the QED effort: > 1. Machine Math language design and specification. > 2. Formalization of a sizeable body of mathematics in Machine Math. > 3. Specification of low-order logic(s) as target language(s). > 4. Construction of Machine Math compiler(s) into the target language(s). > 5. Construction of proof-checkers for the target languages. > 6. Construction of database software to manipulate a large body of > mathematics in Machine Math form. I take a different view: The Root Logic must be agreed upon first, along with some notion of "modularization" for the Root Logic, such as little theories or whatever. In fact, these are the only things that have to be agreed upon. Once the Root Logic is decided on, everyone can go and write proof tools for whatever language and logic they like, using whatever proof search technology they like, as long as the proofs can be translated into the Root Logic and its theory mechanism. Everyone can use the high-level language and logic of his/her choice, within the restriction that its proofs can be translated to proofs in the Root Logic with its theories. It is even possible that some existing proof tools might be modified to translate their internal justifications into explicit proofs in the Root Logic. Of course the correctness of derivations in the Root Logic must be efficiently checkable without any fancy proof search; all proof search is done by whatever front-end is used. Thus I am assuming that the Root Logic has a reasonably efficient notation for completely explicit proofs. (See my comment on tactics below.) This suggestion is not an argument against an agreed upon high-level logic, but that is a much harder problem than to agree on a Root Logic, and it is not necessary to solve this harder problem. Also, different kinds of mathematics may be more amenable to different specialized proof tools. This brings up a point related to Javier's recent comment (these messages are coming faster than I can write!): The mathematics QED should attempt to cover, is I think, the fundamental issue we should be discussing now. From a marketing point, this I think makes a lot of sense. Using an automobile manufacturer's analogy, let's design and produce a car for the market, not find a market for a car we designed and produced without consideration of the market. Yes, we should be discussing what mathematics QED will cover, and we may well design specialized proof tools for these various "markets" as I've suggested above. However, we should not design the Root Logic, in which all the different developments of parts of mathematics are put together with some particular market in mind. The Root Logic is the one thing that, once agreed upon, is very difficult to change. It should be of sufficient expressiveness to handle unexpected problems. On the Root Logic Bob Boyer writes The key point, I think that classicist David Hilbert would say, is that WE CAN ALL AGREE to present and discuss essentially all important logics and theories in a `finitistic' format, such as PRA admits. David McAllester writes Although I am sympathetic to the idea that we can all accept primitive recursive arithmetic (PRA) I am little troubled by using it as the foundation of QED. Consider the mean value theorem (MVT) of calculus. I agree that this thoerem can be encoded as "P is a proof in ZFC of ZFC-MVT" where ZFC-MVT is some formal statement of the mean value theorem in the langauge of set theory. I am concerned about the difficulty of using this entry in the QED library. It seems "encrypted". Larry Paulson writes Mathematics done in simple base logics is not encrypted at all. Isabelle supports the illusion that you are working directly in the formalized logic, be it ZF, HOL, Constructive Type Theory or what have you. AUTOMATH type theories also support a natural proof style. This topic of representing logics in other logics is not (yet) a cleaned-up and codified field of mathematics, so different words are used for the same thing, and the same words for different things. Let me distinguish three approaches for representing logics, although they may be combined in different ways, and I'm probably leaving some out altogether. PRA In PRA, we use the natural numbers, one canonical inductively defined class, to encode PR definable classes of well-founded trees, e.g. the syntax and derivation trees of some object logic. This is really encryption, as McAllester said, and clearly depends on the power of computation over the canonical class. FS0 In Feferman's FS0, we have can directly construct classes of finitely branching well-founded trees, and use these classes directly to represent isomorphically trees of syntax and derivations of some object logic. This is a lot less like encryption, a lot more natural than in PRA. These two ways of representing a logic are similar in that they employ the power of the meta-logic to represent and compute over inductively defined classes; the terms and derivations of the object logic are objects of the meta-logic. One might, for example, quantify over derivations (well, not in PRA, but in L0), and do induction over derivations to prove admissible rules of the object logic. This is the point Feferman is making in [1] when he says (sect. 21) "Examples of elementary meta-logical theorems about Prov(S) which can be proved in FS0 ... are the Deduction Theorem and the Finiteness Theorem." Logical Frameworks The third approach for representing logics is different, and can be used in meta-logics with no inductively defined classes, and no power to construct them. It is used in Automath, and more recently by Martin-L\"of and also the Edinburgh Logical Framework (LF) [2]. The idea is to use the inductive structure of the meta-theory itself to represent the inductive structure of the object theory. I'm being vague because I don't know how to explain this other than by example: see [2],[3], or [4]. LF is a first-order logic; its consistency is provable in PA, and it represents exactly the same functions as simply typed lambda calculus (much less than PR), yet it can faithfully represent a great many powerful object-logics. This method is also used in some higher-order meta-logics. For example some versions of Automath had some second-order power. Isabelle, as mentioned by Larry Paulson in this mailing list, uses this method of representing logics. When Larry says "Isabelle supports the illusion that you are working directly in the formalized logic" he means using this form of representation. Isabelle is higher-order (but without dependent types), but for representing logics in this way it really needs little more than first order. Lambda-prolog also uses this third approach. (The question of how strong does the meta-logic have to be to use this third approach has been somewhat quantified by Amy Felty in a series of papers.) Some Comparisons This third approach sounds pretty good. Larry says he can "support the illusion that you are working directly in the formalized logic", and I've just made a point that it can be carried out in very weak meta-logics. What's the problem? I see two major issues: how many logics can be represented in this way, and how easy are the representations to use. (Both of these points are hinted at by Feferman in [1].) How Many Object-Logics are Representable The representations in this third style use the connectives of the meta-logic to represent meta-connectives of the object logic. For example, the implication of the meta-theory is used for "consequence" (the horizontal line in rules) of the object logic (see [2]). Is it possible to "faithfully and adequately" represent every object logic in this way? (Clearly "every object logic" is too vague to be meaningful.) This is addressed in [4] for LF, and is a technical question; even the definition of "faithful and adequate" is not clear. It is even more problematic for stronger meta-logics than LF; for example if functions are definable by Primitive Recursion then the function type A->B, which is used to code syntactic abstraction (i.e. a B-thing with one A-thing hole) contains more than just syntactic abstractions. The correctness of representations in the first two approaches mentioned above is more straightfoward: one just builds copies of the object-logic's informal term, formula and derivation trees. Similarly, more object-logics are representable with the first two approaches: we just build the derivation trees. Notice, however, that for FS0 it is still possible to find naturally occurring formal systems that are not representable: FS0 only represents finitely branching trees, not the so-called "generalised inductive definitions", including infinitely branching well-founded trees. (See [5] for an example of a use of generalised inductive definitions in formalizing everyday mathematics. By the way, does anyone know of a philosophical school that accepts inductive definitions but rejects generalized inductive definitions where the infinite branching is given by a finite rule?) How Easy is it to Use the Representations In the third approach, the terms, formulas, and derivations of the object logic are not objects of the meta-logic. For one thing, you cannot do induction over them, so the meta-theory of the object logic is not provable. (How much meta-theory you can do may depend on how much extra power the meta-logic has. In Isabelle's representation of first-order logic, is the Deduction Theorem provable? It is certainly not provable in the LF presentation of FOL.) In such a representation the Deduction Theorem is only representable as a tactic; i.e a program in some meta-language of the framework that actually transforms represented derivations of A |- B (these are terms of the framework) into derivations of |- A->B (also terms of the framework). Correctness of this tactic cannot even be stated in the framework. (Of course, we don't have to state or prove correctness of a tactic to use it, but actually running tactics blows up the size of proof trees!) In FS0, the Deduction theorem for a representation of FOL is just a theorem of FS0. This is how mathematics is actually done! Which Root Logic? It may sound like I am putting foward FS0, but I am only using FS0 as an example of a certain style. I am arguing against the LF/Isabelle/Automath style of representation. I am arguing for a Root Logic that can express inductively defined classes. How strong is the Root Logic? How complex are the inductively defined classes it can express? I have argued that FS0 is slightly deficient in only having finitely branching trees. (Feferman suggests this can be easily fixed.) I only happen to know these are very useful from experience [5]. The QED project needs to collect this kind of experience in order to make reasonable decisions on the Root Logic. Another weak but expressive logic, very different in character from FS0 is the Martin-L\"of logical framework, presented somewhat informally in [6]. It has generalized inductive definitions, and is acceptable to most constructivists. [1] "Finitary inductively presented logics", S. Feferman, Logic Colloquium '88, Ferro, Bonotto, Valenti and Zanardo (eds.), Elsevier, North-Holland, 1989., pp. 191-220. [2] "A Framework for Defining Logics", Harper, Honsell and Plotkin, JACM, Jan. 1993. [3] "Using Typed Lambda Calculus to Implement Formal Systems on a Machine", Avron, Honsell, Mason and Pollack, JAR 9:309-354, 1992. [4] "Representing Logics in Type Theory" Philippa Gardner, PhD thesis, Computer Science Dept., University of Edinburgh, July 1992. [5] "Pure Type Systems Formalized", McKinna and Pollack, TLCA'93 (Utrecht), LNCS 664, March 1993. Also available by anonymous ftp from ftp.ed.ac.uk; cd to export/lego and get README. [6] "Programming in Martin-L\"of's Type Theory", Nordstr\"om, Petersson and Smith, Oxford University Press, 1990.