scientific article; zbMATH DE number 1420833

Publication date 22 October 2000

cut elimination first order arithmetic ordinal analysis realizability interpretation witnessing theorem

Cut-elimination and normal-form theorems (03F05) Functionals in proof theory (03F10) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50)

Review text

The aim of the paper is (i) to define a realizability interpretation for classical Peano arithmetic PA; (ii) to prove several E-theorems, in the sense of \textit{G. E. Mints} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 40, 110-118 (1974; Zbl 0368.02034); translation in J. Sov. Math. 8, 323-329 (1977; Zbl 0404.03044)], i.e., to show that different methods for extracting witnessing information from proofs yield the same result. As to the content, section 3 describes the realizability interpretation for PA and its main applications. Roughly, the underlying informal idea can be summarized as follows. Assume that we are looking for a witness of an existential theorem \(\exists x A\) (\(A\) quantifier free). The task is recasted as a general functional problem: if we are given a proof of a finite set \(\Gamma\) of formulas in \(\text{PA} +\forall x \neg A\), try to find a witness for \(A\) from witnesses to the falsity of every formula of \(\Gamma\). The idea is formally implemented by the author in three steps: (1) first of all, fix an existential formula \(\exists x A\) and systematically associate to every formula \(\varphi\) a type \(\text{Type}_{\varphi}\), a realizing term \(f\) in \(\text{PR}_{\omega}\) (= the system of primitive recursive functionals of finite type) of the same type as \(\text{Type}_{\varphi}\), as well as a refuting term; (2) assign to each derivation \(d\) of \(\Gamma\) in PA+\(\forall x \neg A\) a functional term \(F_d\), whose free variables include the free variables of the end-sequent \(\Gamma\) of \(d\), those of \(\exists x A\) and the free variables corresponding to the realizers of the negations of the formula in \(\Gamma\) (this is done by induction on \(d\) and it requires a special lemma ensuring closure under cut of the realizing procedure, in the sense that we can realize \(A\) from refutations of \(\varphi\) and \(\neg \varphi\)); (3) on the assumption that the negations of the formulas in \(\Gamma\) are realized, show that \(F_d\) satisfies \(A\) (or constructively witnesses \(A\)). That this is indeed the case is shown by the main result (Theorem 1): If PA proves an existential formula \(\exists x A\), then a \(\text{PR}_{\omega}\)-term can be produced that witnesses the formula (whence the well-known result on the provably recursive functions of PA). Section 4 discusses a variant of double negation translation for the Tait language. The \(M\)-translation \(A^M\) of \(A\) (\(A\) in the Tait language) is related to its double negation translation \(A^N\) as follows: if the sequent \(\{\varphi_1, \dots,\varphi_k\}\) is provable in PA, then the sequent \( \{ (\varphi_1)^{M}, \dots, ( \varphi_k)^{M} \} \Rightarrow \bot \) is provable in arithmetic with minimal logic. Composing \(M\)-translation, the Friedman-Dragalin (FD)-translation and Kreisel's modified realizability yields another method for extracting witnessing information for classical existential theorems and it turns out (Theorem 5) that the witnessing results coincide with those of classical realizability. Section 5 describes a set of proof reductions for a slightly extended version PA\(^+\) of PA. The crucial property of the induced reduction relation is its compatibility with term reduction: if a derivation \(d\) reduces to a derivation \(d'\), then the associated realizing terms \(F_d\) and \(F_d'\) convert to the same term. PA\(^+\) mainly consists of PA with inversion rule for conjunction and universal quantifiers. The basic reductions of a derivation \(d\) to a derivation \(d'\) are defined according to the last rule of \(d\) and comprise five groups (among them, reductions on principal and non-principal cuts, which essentially correspond to reductions applied in the usual infinitary and finitary cut elimination), elimination of unnecessary variables, principal inversions (e.g., elimination of induction), and non-principal inversions (if the last rule is an inversion applied to a formula not principal in the preceding inference). Iterated application of the reduction rules yields normal proofs (indeed cut free ones) when applied to existential theorems of PA (Lemma 7, Corollary). Again the new witnessing procedure provides the same results of the classical realizability interpretation (Theorem 6). Section 6 deals with cut elimination and ordinal analysis. A variant of Gentzen ordinal assignment for proofs in PA\(^+\) is defined and it is shown that the reductions lower the ordinals of derivations; as a corollary, one obtains a (weak) normalization procedure, and a cut elimination for proofs of existential statements (as normal proofs are cut free). This can be used to get the usual results relating PA and \(\varepsilon_0\) (ordinal classifications of provable functions, bounds on provable primitive recursive wellorderings, 1-consistency of PA). There also follows another E-theorem: If \(d\) is a derivation of an existential statement in PA, the value extracted from \(d\) via classical realizability coincides with the value extracted from \(d\) via ordinal analysis. It is possible to get refinements (fragments of arithmetic) and strong normalization, under suitable restrictions. Section 7 describes a method (inspired by Mints; notion of enrichment) to extract sequences of finitary reductions from an infinitary cut elimination procedure. Again the witnessing information extracted from proofs of existential theorems using infinitary methods coincides with the one using classical realizability. In the final section it is noted that the \(M\)-translation is not efficient on fragments as double negation translation for fragments of arithmetic. It is also remarked that, although classical realizability, finitary cut elimination, infinitary cut elimination all produce the same witnessing information, the results depend on the choice of the cut elimination procedures (reduction rules) and the particular translation of PA to HA. So it would be important to better understand how the witnessing techniques depend on variations in cut elimination. The paper interestingly displays the main methods for constructive interpretation of arithmetic at work: primitive recursive functionals of finite types, various translations of classical theories into constructive theories, realizability, finitary cut elimination and infinitary cut elimination. Thus the paper is especially worthwhile as a contribution towards an integration of proof-theoretic methods and their comparison. For the entire collection see [Zbl 0932.00038].

Recommendations

Cited in

(14)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4944901)