Draft description of (alleged) PRA implementation:
Syntax: The language has terms of two kinds, object terms and Function
terms.
Atomic object terms begin with lower-case letters.
true and false are object constants; there is a supply of free object
variables.
If x and y are object terms, then (x,y) is an object term.
Atomic Function terms begin with upper-case letters.
Cond and Id are Function constants; there is a supply of free Function
variables.
If F is a Function term and x is an object term, F(x) is an object term.
F(x,y) abbreviates F((x,y)).
If x is an object term, [x] is a Function term.
If F and G are Function terms, (F,G) and F(G) are Function terms.
Our logic is equational: assertions are equations between object
terms, in which substitutions for variables are permitted.
Abstraction axioms:
(A1): Id(x) = x
(A2): [y](x) = y
(A3): (F,G)(x) = (F(x),G(x))
(A4): F(G)(x) = F(G(x))
A1-4 allow the proof of a powerful (predicative) abstraction
metatheorem; the abstraction terms obtained are parallel in form to
the terms abstracted from.
Case expression axioms:
(C1): Cond((x,x),(y,z)) = y
(C2): Cond((true,false),(y,z)) = z
(C3): F(Cond((x,y),(u,v))) = Cond((x,y),(F(u),F(v)))
(C4): Cond((x,y),(F(x),z)) = Cond((x,y),(F(y),z))
The intended reading of Cond((x,y),(z,w)) is "if x = y then z else w".
C1 and C2 allow us to define the projection Functions Pi1 =
Cond([true,true],Id) and Pi2 = Cond([false,false],Id), which allows
abstraction with respect to multiple variables.
Axiom C3 is used to introduce and eliminate cases. The assertion z =
Cond((x,y),(z,z)) can be justified using constant functions and axiom
C3.
Axiom C4 is used to reason under hypotheses. Reasoning under negative
hypotheses as in Cond((x,y),(u,Cond((x,y),(v,w))) = Cond((x,y),(u,w))
is justifiable using these axioms.
Recursion and induction axioms:
If F and G are Function terms, is a Function term. If H is a
Function term, H!! is an object term. None of the Function terms in
these constructions may include the Hilbert construction introduced
with the next axiom.
(I1): (x) = Cond((x,(Pi1(x),Pi2(x))),
(G((Pi1(x)),(Pi2(x))),F(x)))
(I2): H(x) = Cond((H(H!!),
Cond((H!!,(Pi1(H!!),Pi2(H!!))),
(G(H(Pi1(H!!)),H(Pi2(H!!))),F(H!!)))),
((x),H(x)))
The test x = (Pi1(x),Pi2(x)) determines whether x is a pair or an
atom. All objects are built from atoms by pairing (we are working
with binary trees). (x) = F(x) if x is an atom, (x,y) =
G((x),(y)).
The object H!! is a counterexample to the defining conditions of
for the function H, if there is such a counterexample. The !!
operator can to a certain extent be used to define quantification (in
the same way that the Hilbert operator introduced below provides a
full implementation of quantification). Forbidding the Hilbert
operator from appearing in the constructions of this part keeps the
recursive functions constructive and the induction scheme open.
Hilbert operator axiom:
If F is a Function term, F! is a Function term.
(H): F(x,y) = Cond((true,F(F!(y),y)),(true,F(x,y)))
The intended meaning of F!(y) is "a counterexample to "for all x,
F(x,y) = true", if there is one (otherwise anything)". F! is usually
a nonconstructive function (it involves an element of choice); such
Functions are excluded from the definitions of recursive functions and
counterexamples to induction.
I have proved (unpublished, available on my Web site) that the system
EFT with axioms A1-4, C1-4, H is exactly equivalent to first-order
logic for infinite domains. I conjecture (and will undertake to
prove) that the full theory given here is equivalent to PRA. The
notation used here is somewhat different from that in the original EFT
paper.
I don't know whether axiom (H) is actually needed; it is needed if one
wants the full expressive power of first-order logic, but it probably
affords only a conservative extension. Expressing quantification
using induction (axiom (I2) and the !! construction instead of axiom
(H) and the ! construction) may be the correct course of action.
Axioms (I1) and (I2) introduce a kind of iteration construction; one
can, of course, define different kinds of recursive functions
constructors with the assistance of the pairing and abstraction
facilities available here. The axiom is more economical to state for
this form of recursion.
The form in which the theory is presented is determined by the style
of reasoning supported by my theorem prover Mark2 (which is
considerably improved over its precursor described in the EFT paper).
The theorem prover now provides variable binding constructions (and
also provides automated support for a style of reasoning not using
bound variables). The prover provides automated support for
substitutions justified by context in a case expression, as in axiom
C4. The documentation for the prover can supply more information (see
the section on "logical style").
There is a considerable amount of work to do to see that this is
equivalent to PRA. Part of this has been done in the paper on EFT
available on the Web site. Some remains to be done, but I'm fairly
sure that this is the right extension of EFT.
To use this system, one needs to prove a lot of preliminary theorems;
this axiom set is very economical! The theorem prover should provide
a good deal of support for reasoning in this theory; I will be
implementing this and doing experiments with it.
Reasons why I think this is a suitable "root logic": it has the right
subject matter (binary trees); it is extremely simple (and so ought to
be relatively easy to reason _about_); I think that I will find that
Mark2 supports computer-assisted reasoning in this system reasonably
well.
Reasons why it might NOT work out: it might be found to be _too_
economical; the style of reasoning might be found to be too eccentric.
I don't have extensive experience yet reasoning with this material
with the latest version of the theorem prover, so I only conjecture
that everything works as I expect it will.