[FOM] Equational reduction of predicate calculus

Alasdair Urquhart urquhart at cs.toronto.edu
Fri Jan 2 12:17:41 EST 2004

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.

More information about the FOM mailing list