Current browse context:
math.LO
Change to browse by:
References & Citations
Mathematics > Logic
Title: Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss
(Submitted on 14 Mar 2024)
Abstract: In this paper, we present a~generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued \L{}ukasiewicz logics. To this end, we provide proof systems that augment Avron's Frege system for \L{}ukasiewicz three-valued logic with nested and general versions of the disjunction elimination rule, respectively. For these systems we provide upper bounds on speed-ups w.r.t.\ both the number of steps in proofs and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus for 3-valued \L{}ukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued \L{}ukasiewicz logics.
Submission history
From: Daniil Kozhemiachenko [view email][v1] Thu, 14 Mar 2024 06:01:26 GMT (19kb)
Link back to: arXiv, form interface, contact.