@article{Kohlenbach_1999, title={A Note on Spector’s Quantifier-Free Rule of Extensionality}, volume={6}, url={https://tidsskrift.dk/brics/article/view/20077}, DOI={10.7146/brics.v6i20.20077}, abstractNote={In this note we show that the so-called weakly extensional arithmetic<br />in all finite types, which is based on a quantifier-free rule of<br />extensionality due to C. Spector and which is of significance in the<br />context of G¨odel’s functional interpretation, does not satisfy the deduction<br />theorem for additional axioms. This holds already for PI^0_1-<br />axioms. Previously, only the failure of the stronger deduction theorem<br />for deductions from (possibly open) assumptions (with parameters<br />kept fixed) was known.}, number={20}, journal={BRICS Report Series}, author={Kohlenbach, Ulrich}, year={1999}, month={Jan.} }