Finite investigations of transfinite derivations

DOI10.1007/BF01091743zbMath0399.03044OpenAlexW2071823993MaRDI QIDQ1254248

Grigori Mints

Publication date: 1978

Published in: Journal of Soviet Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01091743

zbMATH Keywords

FunctionalProof TheoryCut EleminationHeyting ArithmeticImpredicative AnalysisPrimitive Recursive ArithmeticSecond Order ArithmeticTransfinite Derivations

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Complexity of proofs (03F20)

Related Items

A NOTE ON FRAGMENTS OF UNIFORM REFLECTION IN SECOND ORDER ARITHMETIC ⋮ Elementary descent recursion and proof theory ⋮ Proof compressions with circuit-structured substitutions ⋮ A termination proof for epsilon substitution using partial derivations ⋮ On cut elimination in the presence of perice rule ⋮ On the computational complexity of cut-reduction ⋮ Proof-theoretical analysis: Weak systems of functions and classes ⋮ Three faces of natural deduction ⋮ A NOTE ON PREDICATIVE ORDINAL ANALYSIS I: ITERATED COMPREHENSION AND TRANSFINITE INDUCTION ⋮ Cut elimination for a simple formulation of epsilon calculus ⋮ Continuous normalization for the lambda-calculus and Gödel's T ⋮ Generalizations of the one-dimensional version of the Kruskal-Friedman theorems ⋮ \(\Pi_1^1\)-comprehension as a well-ordering principle ⋮ Notation systems for infinitary derivations ⋮ Tiered Arithmetics ⋮ A Characterisation of Definable NP Search Problems in Peano Arithmetic ⋮ Reduction of finite and infinite derivations ⋮ Completeness of the primitive recursive \(\omega \)-rule ⋮ A term calculus for (co-)recursive definitions on streamlike data structures ⋮ Finite notations for infinite terms

Cites Work

• A survey of proof theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item