From lusk Wed May 25 09:16:02 1994 Received: from cli.com (cli.com [192.31.85.1]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with SMTP id JAA16074 for ; Wed, 25 May 1994 09:14:02 -0500 Received: from rita (rita.cli.com) by cli.com (4.1/SMI-4.1) id AA28417; Wed, 25 May 94 09:13:16 CDT From: boyer@cli.com (Robert S. Boyer) Received: by rita (4.1) id AA20022; Wed, 25 May 94 09:13:12 CDT Date: Wed, 25 May 94 09:13:12 CDT Message-Id: <9405251413.AA20022@rita> To: staples@cs.uq.oz.au Cc: qed@mcs.anl.gov Subject: Prolog as a metatheory John, I would like to see the details of your Prolog-based meta theory. I give below, again, Feferman's defintion of PRA, as a model of brevity. One important thing that PRA has is an induction principle. This is crucial for proving metatheorems, such as that any proof in classical first order arithmetic can be translated into a proof of an analogous constructive theorem by inserting double-negations. Proving such metatheorems in the meta (or root) logic of QED is crucial to sharing the labor of those who prefer to work in different logics. What sort of induction principle do you propose for your Prolog-based metatheory? I certainly like clausal form, and in general think that resolution (with unification) does a beautiful job of capturing the quantifier-free part of classical logic, which is also logical part of PRA. The absence of quantifiers in your proposal (as in PRA) is part of the reason that constructivists can buy into the use of classical propositional logic. However, I believe that another important reason that PRA is acceptable to the constructivists is that every function and predicate symbol is either (a) one of the constructors -- 0 and successor, (b) a recursively defined function symbol that when applied to numerals can be rewritten to a numeral, using definitions, or (c) the predicate =, which is decidable over numerals. One thing I don't yet understand is the semantics you propose for uninterpreted function symbols. I believe that constructivists will reject such a proposition as P(h(x)) v -P(h(x)) unless they know that both P and h are recursively decidable on all possible values of x. So what is the meaning of uninterpreted function symbols, such as h, in your Prolog-based meta theory? Am I permitted to think of uninterpreted function symbols as simply representing different colors for CONS, i.e., some sort of specially labeled N-tuples? What are the axioms for h? In particular, what does the induction principle say about h? I think that the intimate relationship between (a) the zero and successor function, (b) the scheme for primitive recursive definition, and (c) the induction principle is one of the reasons that PRA is acceptable to constructivsts -- questions such as the disjunction above do not arise in PRA because there are no uninterpreted h's. It seems to me likely that any practical metatheory will start with other primitives than 0 and successor. Feferman's FS0 takes 0 and cons, which gets one to a representation of terms without the necessity of using explosively large integers, as does Goedel. In my opinion, in addition to cons, some sort of pleasant representation for symbols is also highly desireable. (Perhaps this is all that you intend for uninterpreted function symbols.) Alas, once one starts adding in syntactic sugar, the complexity of a language description can grow very fast. The next thing you know, we'll be adding "backquote", which logicians seem to use in the statement of reflection principles. But it can take pages to define backquote, enough to drive away most prospective thoughtful readers. Bob P. S. To qualifiy my claim that constructivsts accept PRA, I should always mention that there are at least two people to whom PRA is not acceptable, Ed Nelson and Yessen-Volpin. I think they find some of the more computationally complex PRA functions, even exponentiation, rather dubious, since one cannot "in practice" rewrite variable-free terms involving such functions to numerals, for want of time and space in the known universe. But who knows, we may not need any functions outside of P-time in our meta theory. Even cubic-time algorithms can be pretty useless in practice, and if one wants to try to compute with a partial recursive function of no known complexity bound, one can always use a "cpu limit" approach to run it for a specific period of time, with a clocked P-time interpreter for von Neumann machines. ------------------------------------------------------------------------------- What is PRA? Below I quote from p. 7-8 of Solomon Feferman's paper "What rests on what? The proof-theoretical analysis of mathematics.", Invited lecture, 15th International Wittgenstein Symposium: Philosophy of Mathematics, held in Kirchberg/Wechsel, Austria, 16-23 August, 1992. This short text concludes with a definition of PRA. ------------------------------------------------------------------------------- 2.3 The language and basic axioms of first-order arithmetic. In order to describe the reductive results for several systems of arithmetic in the next section, we need some syntactic and logical preliminaries. The language of L0 is a 0 (or first-order) single-sorted formalism. It contains variables x, y, z, ..., the constant symbol 0, the successor symbol ' and symbols f0, f1, ... for each primitive recursive function, beginning with f0(x,y) for x+y, and f1(x,y) for x*y. Terms t, t1, t2, ... are built up from the variables and 0 by closing under ' and the fi. The atomic formulas are equations t1=t2 between terms. Formulas are built up from these by closing under the propositional operations (not, and, or, ->) and quantification (forall x, forsome x) with respect to any variable. A formula is said to be quantifier-free, or in the class QF, if it contains no quantifiers. ... Unless otherwise noted the underlying logic is that of the classical first-order predicate calculus with equality. The basic non-logical axioms Ax0 of arithmetic are: (1) x' /= 0 (2) x' = y' -> x = y (3) x+0 = x and x+y' = (x+y)' (4) x*0 = 0 and x*(y') = x*y + x, and so on for each further fi (using its primitive recursvie defining equations as axioms). To Ax0 may be added certain instances of the Induction Axiom scheme: IA phi(0) and ((forall x) (phi(x) -> phi(x'))) -> (forall x) (phi(x)) for each formula phi(x) (with possible additional free variables). PHI-IA is used to denote both this scheme restricted to phi in PHI {\em and} the system with axioms Ax0 plus PHI-IA. We use PA (Peano Arithmetic) to denote the system with axioms Ax0 and IA, where the full scheme is used. The language PRA (Primitive Recursive Arithmetic) is just the quantifier-free part of L0. In place of IA it uses an Induction Rule IR phi(0), phi(x) -> phi(x') ---------------------------- , for each phi in QF phi(x)