Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Buss

ABSTRACTIn 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 Łukasiewicz logics. To this end, we provide proof systems and which augment Avron's Frege system HŁuk 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 GŁuk for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1080/11663081.2018.1525208
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 48,784
Through your library

References found in this work BETA

Basic Proof Theory.A. S. Troelstra - 2000 - Cambridge University Press.
Mathematical Logic.Joseph R. Shoenfield - 1967 - Reading, Mass., Addison-Wesley Pub. Co..
Proof Theory.Gaisi Takeuti - 1987 - Elsevier.
Basic Proof Theory.Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280-280.

View all 27 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Propositional Consistency Proofs.Samuel R. Buss - 1991 - Annals of Pure and Applied Logic 52 (1-2):3-29.
Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
A Bounded Arithmetic AID for Frege Systems.Toshiyasu Arai - 2000 - Annals of Pure and Applied Logic 103 (1-3):155-199.
Quantum Deduction Rules.Pavel Pudlák - 2009 - Annals of Pure and Applied Logic 157 (1):16-29.
Frege on Indirect Proof.Ivan Welty - 2011 - History and Philosophy of Logic 32 (3):283-290.
Extension Without Cut.Lutz Straßburger - 2012 - Annals of Pure and Applied Logic 163 (12):1995-2007.
Die Grundlagen der Arithmetik, §§ 82-3. [REVIEW]William Demopoulos - 1998 - Bulletin of Symbolic Logic 6 (4):407-28.


Added to PP index

Total views
16 ( #574,750 of 2,309,236 )

Recent downloads (6 months)
4 ( #268,614 of 2,309,236 )

How can I increase my downloads?


My notes

Sign in to use this feature