A note on Spector's quantifier-free rule of extensionality (Q5931215)

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.