Reduction of finite and infinite derivations
type: Item
instance of: scholarly article
title: Reduction of finite and infinite derivations
zbMATH Open document ID: 0964.03057
DOI: 10.1016/S0168-0072(00)00011-7
published in: Annals of Pure and Applied Logic
publication date: 2001-07-09T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 1501505
zbMATH Keywords: normalization
zbMATH Keywords: cut elimination
zbMATH Keywords: first-order arithmetic
zbMATH Keywords: analysis
author: G. E. Mints
reviewed by: Branislav Boričić
MaRDI profile type: Publication
cites work: The lambda calculus, its syntax and semantics
cites work: Notation systems for infinitary derivations
cites work: Q4364500
cites work: Q3922646
cites work: Untersuchungen über das logische Schliessen. I
cites work: Q5812175
cites work: A survey of proof theory
cites work: Q5633976
cites work: Finite investigations of transfinite derivations
cites work: A new reduction sequence for arithmetic
cites work: A normal form for logical derivations implying one for arithmetic derivations
cites work: Q3999386
cites work: Proof-theoretic analysis of KPM
cites work: Q4143279
cites work: Intensional interpretations of functionals of finite type I
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Q4944926
full work available at URL: s0168-0072(00)00011-7
OpenAlex ID: W1969898883
description: scientific article; zbMATH DE number 1501505