Open AccessA Note on Spector’s Quantifier-Free Rule of Extensionality
Author(s) -
Ulrich Kohlenbach
Publication year - 1999
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v6i20.20077
Subject(s) - extensionality , quantifier (linguistics) , axiom , mathematics , context (archaeology) , quantifier elimination , extensional definition , discrete mathematics , computer science , paleontology , tectonics , geometry , artificial intelligence , biology
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.