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)