We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
A note on cut-elimination for classical propositional logic.
- Authors
Pulcini, Gabriele
- Abstract
In Schwichtenberg (Studies in logic and the foundations of mathematics, vol 90, Elsevier, pp 867–895, 1977), Schwichtenberg fine-tuned Tait's technique (Tait in The syntax and semantics of infinitary languages, Springer, pp 204–236, 1968) so as to provide a simplified version of Gentzen's original cut-elimination procedure for first-order classical logic (Gallier in Logic for computer science: foundations of automatic theorem proving, Courier Dover Publications, London, 2015). In this note we show that, limited to the case of classical propositional logic, the Tait–Schwichtenberg algorithm allows for a further simplification. The procedure offered here is implemented on Kleene's sequent system G4 (Kleene in Mathematical logic, Wiley, New York, 1967; Smullyan in First-order logic, Courier corporation, London, 1995). The specific formulation of the logical rules for G4 allows us to provide bounds on the height of cut-free proofs just in terms of the logical complexity of their end-sequent.
- Subjects
LONDON (England); NEW York (State); PROPOSITION (Logic); COMPUTER logic; MATHEMATICAL logic; FIRST-order logic; PHILOSOPHY of mathematics
- Publication
Archive for Mathematical Logic, 2022, Vol 61, Issue 3/4, p555
- ISSN
0933-5846
- Publication type
Article
- DOI
10.1007/s00153-021-00800-8