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

  • Ulrich Kohlenbach


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.
How to Cite
Kohlenbach, U. (1999). A Note on Spector’s Quantifier-Free Rule of Extensionality. BRICS Report Series, 6(20). https://doi.org/10.7146/brics.v6i20.20077