A proof of Gentzen's \textit{Hauptsatz} without multicut

DOI10.1007/S001530050170zbMath0968.03065OpenAlexW2014377715MaRDI QIDQ5928308

Jan von Plato

Publication date: 28 March 2001

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

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

zbMATH Keywords

cut eliminationinversibilitymulticuts

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items (11)

A connection between cut elimination and normalization ⋮ VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED ⋮ Gentzen's consistency proof without heightlines ⋮ Gentzen's Proof Systems: Byproducts in a Work of Genius ⋮ Proof-theoretic pluralism ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Sequent calculus in natural deduction style ⋮ A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION ⋮ Cut-elimination for weak Grzegorczyk logic Go ⋮ FROM STENIUS’ CONSISTENCY PROOF TO SCHÜTTE’S CUT ELIMINATION FOR ω-ARITHMETIC ⋮ Structural proof theory for first-order weak Kleene logics

This page was built for publication: A proof of Gentzen's \textit{Hauptsatz} without multicut