Skip to main content Skip to main navigation menu Skip to site footer
  • Register
  • Login
  • Language
    • English
    • Język Polski
  • Menu
  • Home
  • Current
  • Archives
  • Online First Articles
  • About
    • About the Journal
    • Submissions
    • Editorial Team
    • Advisory Board
    • Peer Review Process
    • Logic and Logical Philosophy Committee
    • Open Access Policy
    • Privacy Statement
    • Contact
  • Register
  • Login
  • Language:
  • English
  • Język Polski

Logic and Logical Philosophy

Tautology Elimination, Cut Elimination, and S5
  • Home
  • /
  • Tautology Elimination, Cut Elimination, and S5
  1. Home /
  2. Archives /
  3. Vol. 26 No. 4 (2017): December /
  4. Articles

Tautology Elimination, Cut Elimination, and S5

Authors

  • Andrzej Indrzejczak University of Łódź

DOI:

https://doi.org/10.12775/LLP.2017.005

Keywords

sequent calculus, tautology elimination, cut elimination, modal logic S5

Abstract

Tautology elimination rule was successfully applied in automated deduction and recently considered in the framework of sequent calculi where it is provably equivalent to cut rule. In this paper we focus on the advantages of proving admissibility of tautology elimination rule instead of cut for sequent calculi. It seems that one may find simpler proofs of admissibility for tautology elimination than for cut admissibility. Moreover, one may prove its admissibility for some calculi where constructive proofs of cut admissibility fail. As an illustration we present a cut-free sequent calculus for S5 based on tableau system of Fitting and prove admissibility of tautology elimination rule for it.

Author Biography

Andrzej Indrzejczak, University of Łódź

Department of Logic

References

Brighton, J., “Cut elimination for GLS using the terminability of its regress process”, Journal of Philosophical Logic 5, 2 (2016): 147–153. DOI: 10.1007/s10992-015-9368-4

Bednarska, K., and A. Indrzejczak, “Hypersequent calculi for S5: The methods of cut elimination”, Logic and Logical Philosophy 24, 3 (2015): 277–311. DOI: 10.12775/LLP.2015.018

Davis, M., and H. Putnam, “A computing procedure for quantification theory”, Journal of the Assoc. Comput. Mach. 7, 3 (1960): 201–215. DOI: 10.1145/321033.321034

Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Reidel, Dordrecht 1983. DOI: 10.1007/978-94-017-2794-5

Fitting, M., “Simple propositional S5 tableau system”, Annals of Pure and Applied Logic 96, 1–3 (1999): 101–115. DOI: 10.1016/S0168-0072(98)00034-7

Gallier, J.H., Logic for Computer Science, Harper and Row, New York 1986.

Gao, F., and G. Tourlakis, “A short and readable proof of cut elimination for two first-order modal logics”, Bulletin of the Section of Logic 44, 3–4 (2015): 131–148. DOI: 10.18778/0138-0680.44.3.4.03

Indrzejczak, A., “Simple decision procedure for S5 in standard cut-free sequent calculus”, Bulletin of the Section of Logic 45, 2 (2016): 125–140. DOI: 10.18778/0138-0680.45.2.05

Lyaletski, A.V., “A note on the cut rule”, in Abstracts of the International Conference “Maltsev Meeting”, vol. 137, Novosibirsk 2011.

Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge 2001. DOI: 10.1017/CBO9780511527340

Ohnishi, M., K. Matsumoto, “Gentzen method in modal calculi I”, Osaka Mathematical Journal 9 (1957): 113–130.

Logic and Logical Philosophy

Downloads

  • PDF

Published

2017-04-05

How to Cite

1.
INDRZEJCZAK, Andrzej. Tautology Elimination, Cut Elimination, and S5. Logic and Logical Philosophy [online]. 5 April 2017, T. 26, nr 4, s. 461–471. [accessed 1.4.2023]. DOI 10.12775/LLP.2017.005.
  • PN-ISO 690 (Polish)
  • ACM
  • ACS
  • APA
  • ABNT
  • Chicago
  • Harvard
  • IEEE
  • MLA
  • Turabian
  • Vancouver
Download Citation
  • Endnote/Zotero/Mendeley (RIS)
  • BibTeX

Issue

Vol. 26 No. 4 (2017): December

Section

Articles

Stats

Number of views and downloads: 311
Number of citations: 1

Crossref
Scopus
Google Scholar
Europe PMC

Search

Search

Browse

  • Browse Author Index
  • Issue archive

User

User

Current Issue

  • Atom logo
  • RSS2 logo
  • RSS1 logo

Information

  • For Readers
  • For Authors
  • For Librarians

Newsletter

Subscribe Unsubscribe

Language

  • English
  • Język Polski

Tags

Search using one of provided tags:

sequent calculus, tautology elimination, cut elimination, modal logic S5
Up

Akademicka Platforma Czasopism

Najlepsze czasopisma naukowe i akademickie w jednym miejscu

apcz.umk.pl

Partners

  • Akademia Ignatianum w Krakowie
  • Akademickie Towarzystwo Andragogiczne
  • Fundacja Copernicus na rzecz Rozwoju Badań Naukowych
  • Instytut Historii im. Tadeusza Manteuffla Polskiej Akademii Nauk
  • Instytut Kultur Śródziemnomorskich i Orientalnych PAN
  • Karmelitański Instytut Duchowości w Krakowie
  • Państwowa Akademia Nauk Stosowanych w Krośnie
  • Państwowa Akademia Nauk Stosowanych we Włocławku
  • Państwowa Wyższa Szkoła Zawodowa im. Stanisława Pigonia w Krośnie
  • Polskie Towarzystwo Ekonomiczne
  • Polskie Towarzystwo Ludoznawcze
  • Towarzystwo Miłośników Torunia
  • Towarzystwo Naukowe w Toruniu
  • Uniwersytet im. Adama Mickiewicza w Poznaniu
  • Uniwersytet Mikołaja Kopernika
  • Uniwersytet w Białymstoku
  • Uniwersytet Warszawski
  • Wojewódzka Biblioteka Publiczna - Książnica Kopernikańska
  • Wyższe Seminarium Duchowne w Pelplinie / Wydawnictwo Diecezjalne „Bernardinum" w Pelplinie

© 2021- Nicolaus Copernicus University Accessibility statement Shop