Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination

DOI10.1090/S0273-0979-97-00715-5zbMATH Open0873.03049arXivmath/9607204MaRDI QIDQ4337947FDOQ4337947

Authors: Stephen Semmes, Alessandra Carbone 

Publication date: 27 May 1997

Published in: Bulletin of the American Mathematical Society (Search for Journal in Brave)

Abstract: This paper is intended to provide an introduction to cut elimination which is accessible to a broad mathematical audience. Gentzen's cut elimination theorem is not as well known as it deserves to be, and it is tied to a lot of interesting mathematical structure. In particular we try to indicate some dynamical and combinatorial aspects of cut elimination, as well as its connections to complexity theory. We discuss two concrete examples where one can see the structure of short proofs with cuts, one concerning feasible numbers and the other concerning "bounded mean oscillation" from real analysis.

Full work available at URL: https://arxiv.org/abs/math/9607204

Recommendations

• Interpolants, cut elimination and flow graphs for the propositional calculus
• scientific article; zbMATH DE number 7307076
• Proofs without syntax
• Streams and strings in formal proofs.
• scientific article; zbMATH DE number 7204450
• Combinatorial flows as bicolored atomic flows
• Proof theory
• Duplication of directed graphs and exponential blow up of proofs
• scientific article; zbMATH DE number 7668089
• scientific article; zbMATH DE number 2020175

zbMATH Keywords

Herbrand's theoremcut eliminationsequent calculusinterpolation theorempigeonhole principlelogical flow graphsJohn-Nirenberg theoremcombinatorial aspect of proof theorygeometry and dynamism in formal proofsnesting of quantifiers

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

Cited In (9)

• Logical structures and genus of proofs
• Turning cycles into spirals
• Radical anti-realism, Wittgenstein and the length of proofs
• Normalization of N-graphs via sub-N-graphs
• Streams and strings in formal proofs.
• Cycling in proofs and feasibility
• The cost of a cycle is a square
• Asymptotic cyclic expansion and bridge groups of formal proofs
• Interpolants, cut elimination and flow graphs for the propositional calculus

This page was built for publication: Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination

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