Notation systems for infinitary derivations

\(\omega \) -arithmetic cut-elimination operator infinite derivations inversion operator notation system Peano arithmetic reduction operator transfinite induction

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Review text

The author calls his paper modestly a supplement to presentations of \textit{J.-Y. Girard} [Proof theory and logical complexity. Vol. I (1987; Zbl 0635.03052)], \textit{G. E. Mints} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 49, 67-122 (1975; Zbl 0341.02020)], and \textit{H. Schwichtenberg} [``Proof theory: some applications of cut-elemination, Handbook of mathematical logic, 867-895 (1977; Zbl 0443.03001)]. Actually he provides an elegant method of finitarily describing infinite derivations of \(\omega\)-arithmetic \({\mathbb{Z}}^{\infty}\) without numerical coding. Instead he uses finite terms as notations for infinite derivations. The system of these terms is generated starting from constants for finite derivations by function symbols \(I_{k,A}\), \(R_ C\), and E, which correspond to the operations \({\mathcal I}_{k,A}\), \({\mathcal R}_ C\), and \({\mathcal E}\) on \({\mathbb{Z}}^{\infty}\), the set of well-founded infinite derivations of \(\omega\)-arithmetic. \({\mathcal E}: {\mathbb{Z}}^{\infty}\to {\mathbb{Z}}^{\infty}\) is to be the cut-elimination operator, \({\mathcal R}_ C: {\mathbb{Z}}^{\infty}\times {\mathbb{Z}}^{\infty}\to {\mathbb{Z}}^{\infty}\) the reduction operator, which associates to each derivation containing a cut with cut formula C a derivation with a simpler cut formula in the corresponding cut. \({\mathcal I}_{k,A}\) is the inversion operator, which substitutes each occurrence of A in the derivations by some A[k], which is simpler than A. The method is applied to gain two known results of proof theory: Let \({\mathbb{Z}}+TI_{\prec \upharpoonright}\) be the system of Peano arithmetic together with the schema of transfinite induction up to any proper segment of the given primitive recursive well-ordering \(\prec\). Then it is shown: (I) If \(R\in \Sigma^ 0_ 1\) and \({\mathbb{Z}}+TI_{\prec \upharpoonright}\vdash \forall x\exists yR(x,y)\), then there are primitive recursive functions g and o from \({\mathbb{N}}^ 2\) to \({\mathbb{N}}\) such that \[ \min \{m| \quad R(n,m)\}=g(n,\quad \min \{k| \quad o(n,k+1)\nless o(n,k)\})\text{ for all } n\in {\mathbb{N}}. \] (II) PRA\(\vdash PRW O(\prec)\Rightarrow\Pi^ 0_ 2\)-Reflection (\({\mathbb{Z}}+TI_{\prec \upharpoonright}).\) At the end of the paper the notation system for well-founded derivations is extended to a concept of derivations which have not necessarily well- founded tree structure. The cut-elimination operator \({\mathcal E}\) is extended to an operator \({\mathcal E}'\) which operates on generalized derivations such that local correctness with respect to the derivation rules is preserved and \({\mathcal E}'\) is continuous. Thus an alternative description of the continuous cut-elimination operator of Mints [loc. cit.] is provided.

Recommendations

Cites work

Cited in

(38)

This page was built for publication: Notation systems for infinitary derivations

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