A Note on Spector's Quantifier-Free Rule of Extensionality
Ulrich Kohlenbach August 1999 |
Abstract: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 -axioms. Previously, only the failure of the stronger deduction theorem for deductions from (possibly open) assumptions (with parameters kept fixed) was known. Available as PostScript, PDF, DVI. |