A Note on Spector’s Quantifier-Free Rule of Extensionality
Ulrich Kohlenbach · BRICS Report Series · 1999
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¨odel'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.