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

Forfattere

  • Ulrich Kohlenbach

DOI:

https://doi.org/10.7146/brics.v6i20.20077

Resumé

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.

Downloads

Publiceret

1999-01-20

Citation/Eksport

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

Nummer

Nr. 20 (1999): RS-20 A Note on Spector’s Quantifier-Free Rule of Extensionality

Sektion

Artikler

Licens

Authors who publish with this journal agree to the following terms:

    1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.

    1. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.

  1. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).