On cut elimination in the presence of perice rule

DOI10.1007/BF02017499zbMath0639.03059MaRDI QIDQ3781102

L. N. Gordeev

Publication date: 1987

Published in: Archiv für Mathematische Logik und Grundlagenforschung (Search for Journal in Brave)

Full work available at URL: https://eudml.org/doc/138059

zbMATH Keywords

cut eliminationsequent calculusproof theoryprimitive recursive arithmeticPeirce ruleLJP

Mathematics Subject Classification ID

Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items (9)

Proof compressions with circuit-structured substitutions ⋮ Bounds for cut elimination in intuitionistic propositional logic ⋮ Peirce's Rule in a Full Natural Deduction System ⋮ A new normalization strategy for the implicational fragment of classical propositional logic ⋮ 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08 ⋮ How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning ⋮ On Constructive Fragments of Classical Logic ⋮ An alternative normalization of the implicative fragment of classical logic ⋮ Peirce's rule in natural deduction.

Cites Work

• Finite investigations of transfinite derivations
• Unnamed Item
• Unnamed Item

This page was built for publication: On cut elimination in the presence of perice rule