[FOM] Equational reduction of predicate calculus

[Alasdair Urquhart]

I don't know the answer to Harvey Friedman's query,
but there is of course a classical 1952 monograph by Kleene
(AMS Memoirs 10) showing that every recursively axiomatized
theory can be obtained as a restriction of a finitely axiomatized 
theory.  Kleene's construction is very clearly described in
the review by McNaughton (JSL XIX 62 -- available on-line on
JSTOR).  The trick is to formalize a description of a p.r.
function that enumerates the axioms.  

I suppose that you can generalize Kleene's construction
to get the result described by Harvey by Skolemizing 
everything in sight, but perhaps I am under-estimating
the difficulty of the proof.