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


Abstract
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)
ISBN(s)
DOI 10.1080/11663081.2018.1525208
Options
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: 39,566
Through your library

References found in this work BETA

Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
Introduction to Metamathematics.Stephen Cole Kleene - 1968 - Journal of Symbolic Logic 33 (2):290-291.
Natural 3-Valued Logics—Characterization and Proof Theory.Arnon Avron - 1991 - Journal of Symbolic Logic 56 (1):276-294.

View all 15 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.George Boolos & Richard G. Heck - 1998 - In Matthias Schirn (ed.), Bulletin of Symbolic Logic. Clarendon Press. pp. 407-28.

Analytics

Added to PP index
2018-10-12

Total views
9 ( #695,116 of 2,325,499 )

Recent downloads (6 months)
8 ( #173,021 of 2,325,499 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature