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

DOI10.1090/S0273-0979-97-00715-5MaRDI QIDQ4337947zbMATH OpenFDO

Authors Stephen Semmes, Alessandra Carbone

Publication date 27 May 1997

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

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

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)

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.

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
• Combinatorial proofs for constructive modal logic
• scientific article; zbMATH DE number 2020175

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)