[FOM] Equational Reduction of Predicate Calculus/Correction

[Harvey Friedman]

On 1/2/04 12:11 AM, "Harvey Friedman" <friedman at math.ohio-state.edu> wrote:

> 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?
> 

Correction:

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 finite set K of many
sorted equations such that K + "the first new function symbol has exactly
two values" is a conservative extension of T.

Harvey Friedman