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 Available as PostScript, PDF, DVI. |