In this note we show that the so-called weakly extensional arithmetic in all finite types, which is based on a quantifier-free rule of extensionality due to C. Spector and which is of significance in the context of Gödel’s functional interpretation, does not satisfy the deduction theorem for additional axioms. This holds already for PI_0^1-axioms. Previously, only the failure of the stronger deduction theorem for deductions from (possibly open) assumptions (with parameters kept fixed) was known.
Archive for Mathematical Logic, 2001, Vol 40, Issue 2, p. 89-92
Finite type arithmetic; Functionals of finitetype; Extensionality; Deduction theorem