A note on Spector's quantifier-free rule of extensionality (Q5931215): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 00:40, 5 March 2024
scientific article; zbMATH DE number 1590717
Language | Label | Description | Also known as |
---|---|---|---|
English | A note on Spector's quantifier-free rule of extensionality |
scientific article; zbMATH DE number 1590717 |
Statements
A note on Spector's quantifier-free rule of extensionality (English)
0 references
12 March 2002
0 references
Extensionality is a tricky business in the system of the Dialectica interpretation (= functional type theory). The author presents one more aspect of this situation, in this paper. Let \(\text{WE-HA}^{\omega}\) be Heyting arithmetic in all finite types with weak extensionality. (Extensionality is expressed, not by axioms, but by the rule: from \(A\to s=t\) infer \(A\to r[s]=r[t]\), where \(A\) is quantifier-free and terms \(s,t\) and \(r\) have appropriate types. This is the approach used by Spector.) The author constructs a \(\Pi^0_1\)-sentence \(A\) and a quantifier-free \(B\) such that \(A\vdash B\) in \(\text{WE-HA}^{\omega}\) but \(\nvdash A\to B\) even if classical logic is used. [Failure of the deduction theorem.] Actually, \(A\) is the consistency statement of Peano arithmetic, \(\forall x(t_{\text{PA}}x=0)\), and \(B\) is \(a(t_{\text{PA}})=a(\lambda x\cdot 0)\). Were \(\vdash A\to B\), the consistency of PA is derived.
0 references
Dialectica interpretation
0 references
functional type theory
0 references
Heyting arithmetic
0 references
extensionality
0 references
deduction theorem
0 references