Classical logic, storage operators and second-order lambda-calculus (Q1326769)

Storage operators, introduced by the author [Arch. Math. Logic 30, 241- 267 (1990; Zbl 0712.03009)], are a device to simulate call-by-value in a lambda-calculus with head-reduction. In this paper this concept is used to characterize the lambda-terms encoding integers in classical logic. Let \(\text{Nat} [x]\) be the formula expressing in second-order lambda- calculus (also with first-order variables and quantifiers) the data type of natural numbers. An important consequence of the normalization theorem is that if \(\vdash M: \text{Nat} [x]\), then \(M\) is beta-equivalent to \(\underline{n}\), the Church numeral for \(n\). When one extends the calculus with axioms (i.e., when the typing context is extended with typed constants \(c_ i: \sigma_ i\)), this in general is no longer true. The paper considers the especially relevant extension obtained with the axiom \({\mathbf c}\): \(\forall X(\neg\neg X\to X)\). This system, in view of Gödel's double-negation translation, axiomatizes classical logic. \textit{M. Parigot} [Lect. Notes Comput Sci. 592, 361-380 (1991)] has shown that closed elements of type NAT in this extended system can be characterized in terms of storage operators: If \({\mathbf c} \vdash M: \text{Nat} [n]\) and if \(T\) is a storage operator for integers, then, for any variable \(f\), \(TfM\) reduces by head reduction to \(fN\), with \(N\) beta- equivalent to \(\underline {n}\), depending only on \(n\) (and not on \(M\)). The nontrivial proof uses a realizability argument. All the preliminaries, including those on storage operators and the proof of Parigot's result, are clearly explained in the first part (pp. 53-70) of the paper. The result, besides its direct technical interest, is of potential relevance also for the ongoing research on the extraction of programs from classical proofs.