Explaining the Gentzen-Takeuti reduction steps: A second-order system

DOI10.1007/s001530000064zbMath1007.03051OpenAlexW1986927116MaRDI QIDQ5944050

Wilfried Buchholz

Publication date: 2 April 2002

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

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

zbMATH Keywords

cut-eliminationcollapsingcomprehension axiomconsistency proofsfinitary derivationsGentzen-Takeuti reductionordinal diagrams

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35) Proof theory in general (including proof-theoretic semantics) (03F03) Recursive ordinals and ordinal notations (03F15)

Related Items (8)

An extension of the omega-rule ⋮ A Buchholz rule for modal fixed point logics ⋮ Effective cut-elimination for a fragment of modal mu-calculus ⋮ From Subsystems of Analysis to Subsystems of Set Theory ⋮ Gödel's Reformulation of Gentzen's First Consistency Proof For Arithmetic: The No-Counterexample Interpretation ⋮ MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics ⋮ A Buchholz derivation system for the ordinal analysis of KP + Π₃-reflection ⋮ Cut-Elimination for SBL

This page was built for publication: Explaining the Gentzen-Takeuti reduction steps: A second-order system