[FOM] Equational Reduction of Predicate Calculus/Correction
Harvey Friedman
friedman at math.ohio-state.edu
Fri Jan 2 03:00:50 EST 2004
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
More information about the FOM
mailing list