Note on definitional reductions.
Jonathan P. Seldin · Notre Dame Journal of Formal Logic · 1968
(1) XDY& Φ(Al9 . . . ,Am)DZ==>XϋY where Y is formed from Y by replacing one occurrence of Φ{Ah . . . , Am) by Z. The older restriction, used in [CLg] and [DFS] is that Z be a basic ob. I will call the rule with this restriction Rd The other restriction, used in [FML], is that Φ(Ai, . . . , Am) DZ be one of the defining axioms. I will call the rule with this latter restriction Rd*. The equivalence of these two rules was apparently taken for granted in Curry's work. The purpose of this note is to verify this equivalence. It turns out that Rd* is slightly more general than Rd, but that the two are precisely equivalent for reductions to ultimate definienda. My basic notation is that of Curry in the papers referred to above. I will use '21' and f δ ' to stand for sequences of basic obs.