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

Ulrich Kohlenbach | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research