Reduction of finite and infinite derivations (Q1577482)

The author presents a general schema of easy normalizations proofs for finite systems \(S\) like first-order arithmetic or subsystems of analysis having good infinitary counterparts \(S_\infty\) and promotes a view of a derivation in a standard finite system with induction as a finite encoding of some infinitary derivations. The paper is essentially based on some of the author's previous works [see \textit{G. E. Mints}, J. Soviet Math. 10, 548-596 (1978; Zbl 0399.03044), translation from Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 49, 67-122 (1975; Zbl 0341.02020), reprinted in \textit{G. E. Mints}, Selected papers in proof theory, North-Holland and Bibliopolis, Amsterdam and Naples, 17-72 (1992; Zbl 0773.03038), and \textit{G. E. Mints}, J. Soviet Math. 20, 2322-2333 (1982; Zbl 0492.03021), translation from Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 88, 106-130 (1979; Zbl 0439.03042), reprinted in \textit{G. E. Mints}, Selected papers in proof theory, North-Holland and Bibliopolis, Amsterdam and Naples, 77-96 (1992; Zbl 0773.03038)]. The author considers a new system \(S_\infty^+\), with the same rules as \(S_\infty\), but different derivable objects: a derivation \(d\in S_\infty^+\) of a sequent \(\Gamma\) contains a finite derivation \(\Phi(d)\in S\) of \(\Gamma\). Sufficient conditions for \(S_\infty^+\) implying a weak normalization theorem for \(S\) are obtained, followed by three examples of application including variations on Peano arithmetic and subsystems of analysis.