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

DOI10.1090/S0273-0979-97-00715-5zbMath0873.03049arXivmath/9607204MaRDI QIDQ4337947

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

cut eliminationsequent calculusinterpolation theoremlogical flow graphsHerbrand's theorempigeonhole principleJohn-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)

Related Items

The cost of a cycle is a square, Normalization of N-graphs via sub-N-graphs, Radical anti-realism, Wittgenstein and the length of proofs, Asymptotic cyclic expansion and bridge groups of formal proofs, Cycling in proofs and feasibility, Turning cycles into spirals, Streams and strings in formal proofs.