A Note on Spector's Quantifier-Free Rule of Extensionality

Ulrich Kohlenbach

August 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ödel's functional interpretation, does not satisfy the deduction theorem for additional axioms. This holds already for tex2html_wrap_inline21-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.


Last modified: 2003-06-08 by webmaster.