[FOM] Equational reduction of predicate calculus
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