arXiv · 2403.09119
Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss
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.
Explore related subjects
Keep this discovery
Daniil Kozhemiachenko. 2024-03-14. Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss. https://doi.org/10.1080/11663081.2018.1525208
Cite the original work for its findings. Save a collection to share your selection of sources.