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.