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

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¨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.