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.

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v6i20.20077
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library