ABSTRACT
Consider a prenex sentence v , and let g(v) be the number of quantifiers V in v . If g(v) = 0 then trivially NH(v) = v . Assume now that g (v )> 0 and that, for formulas u with g(u) < g (v ) , I have constructed algorithms transfor ming derivations of
C 0, E 1? EHU = 4 NH(u), C x
into derivations of
C 0, E i u , Cq
where Ejj11 is the set o f equality axioms for the Herbrand functions in NH(u) and Ej is a set of other equality axiom s, including those for the functions symbols in u .
