[FOM] Equational Reduction of Predicate Calculus
friedman at math.ohio-state.edu
Fri Jan 2 00:11:31 EST 2004
THEOREM. Let T be a recursively axiomatized set of sentences in first order
predicate calculus with equality, in a finite relational type consisting
entirely of constant and function symbols. There is a finitely axiomatized
set K of equations in many sorted first order predicate calculus with
equality, which is a conservative extension of T.
This is very classical looking. Who first proved this?
More information about the FOM