Przejdź do sekcji głównej Przejdź do głównego menu Przejdź do stopki
  • Zarejestruj
  • Zaloguj
  • Język
    • English
    • Język Polski
  • Menu
  • Strona domowa
  • Aktualny numer
  • Archiwum
  • Prace online
  • O czasopiśmie
    • O czasopiśmie
    • Przesyłanie tekstów
    • Zespół redakcyjny
    • Rada redakcyjna
    • Proces recenzji
    • Komitet Logic and Logical Philosophy
    • Polityka Open Access
    • Polityka prywatności
    • Kontakt
  • Zarejestruj
  • Zaloguj
  • Język:
  • English
  • Język Polski

Logic and Logical Philosophy

Hypersequent Calculi for S5: The Methods of Cut Elimination
  • Strona domowa
  • /
  • Hypersequent Calculi for S5: The Methods of Cut Elimination
  1. Strona domowa /
  2. Archiwum /
  3. Tom 24 Nr 3 (2015): September /
  4. Artykuły

Hypersequent Calculi for S5: The Methods of Cut Elimination

Autor

  • Kaja Bednarska University of Łódź
  • Andrzej Indrzejczak University of Łódź

DOI:

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

Słowa kluczowe

cut elimination, modal logic, hypersequent calculi, proof theory

Abstrakt

S5 is one of the most important modal logic with nice syntactic, semantic and algebraic properties. In spite of that, a successful (i.e. cut-free) formalization of S5 on the ground of standard sequent calculus (SC) was problematic and led to the invention of numerous nonstandard, generalized forms of SC. One of the most interesting framework which was very often used for this aim is that of hypersequent calculi (HC). The paper is a survey of HC for S5 proposed by Pottinger, Avron, Restall, Poggiolesi, Lahav and Kurokawa. We are particularly interested in examining different methods which were used for proving the eliminability/admissibility of cut in these systems and present our own variant of a system which admits relatively simple proof of cut elimination.

Biogramy autorów

Kaja Bednarska - University of Łódź

Department of Logic

Andrzej Indrzejczak - University of Łódź

Department of Logic

Bibliografia

Avron, A., “A constructive analysis of RM”, Journal of Symbolic Logic, 52, 4 (1987): 939–951. DOI: 10.2307/2273828

Avron, A., “Hypersequents, logical consequence and intermediate logics for concurrency”, Annals of Mathematics and Artificial Intelligence, 4, 3–4 (1991): 225–248. DOI: 10.1007/BF01531058

Avron, A., “The method of hypersequents in the proof theory of propositional non-classical logic”, pages 1–32 in Logic: from Foundations to Applications, 1996.

Avron, A., “A simple proof of completeness and cut-elimination for propositional Gödel logic”, Journal of Logic and Computation, 21 (2011): 813–821.

Belnap, N.D., “Display logic”, Journal of Philosophical Logic, 11, 4 (1982): 375–417. DOI: 10.1007/BF00284976

Braüner, T., “A cut-free Gentzen formulation of the modal logic S5”, Logic Journal of the IGPL, 8, 5 (2000): 629–643. DOI: 10.1093/jigpal/8.5.629

Baaz, M., and A. Ciabattoni, “A Schütte-Tait style cut-elimination proof for first-order Gödel logic”, pages 24–38 in Automated Reasoning with Tableaux and Related Methods (Tableaux’02), vol. 2381 of LNAI, 2002.

Baaz, M., A. Ciabattoni, and C.G. Fermüller, “Hypersequent calculi for Gödel logics – a survey”, Journal of Logic and Computation, 13 (2003): 1–27.

Ciabattoni, A., G. Metcalfe, and F. Montagna, “Algebraic and prooftheoretic characterizations of truth stressers for MTL and its extensions”, Fuzzy Sets and Systems, 161 , 3 (2010): 369–389. DOI: 10.1016/j.fss.2009.09.001

Ciabattoni, A., R. Ramanayake, and H. Wansing, “Hypersequent and display calculi – a unified perspective”, Studia Logica, 102, 6 (2014): 1245–1294. DOI: 10.1007/s11225-014-9566-z

Curry, H.B., Foundations of Mathematical Logic, McGraw-Hill: New York, 1963.

Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Reidel: Dordrecht, 1983.

Girard, J. Y., Proof Theory and Logical Complexity, Bibliopolis: Napoli, 1987.

Indrzejczak, A., “Cut-free double sequent calculus for S5”, Logic Journal of the IGPL, 6, 3 (1998): 505–516. DOI: 10.1093/jigpal/6.3.505

Indrzejczak, A., “Cut-free hypersequent calculus for S4.3”, Bulletin of the Section of Logic, 41, 1/2 (2012): 89–104.

Indrzejczak, A., “Eliminability of cut in hypersequent calculi for some modal logics of linear frames”, Information Processing Letters, 115, 2 (2015): 75–81. DOI: 10.1016/j.ipl.2014.07.002

Kanger, S., “Provability in logic”, Stockholm Studies in Philosophy, 47 pp., series “Acta Universitatis Stockholmiensis”, Almqvist and Wiskell: Stockholm, 1957.

Kurokawa, H., “Hypersequent calculi for modal logics extending S4”, pages 51–68 in New Frontiers in Artificial Intelligence, series “Lecture Notes in Computer Science”, 2013. DOI: 10.1007/978-3-319-10061-6_4

Lahav, O., “From frame properties to hypersequent rules in modal logics”, pages 408–417 in 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013. DOI: 10.1109/LICS.2013.47

Metcalfe, G., N. Olivetti, and D. Gabbay, Proof Theory for Fuzzy Logics, Springer, 2008.

Mints, G., “Cut-free calculi of the S5 type”, pages 79–82 in Studies in Constructive Mathematics and Mathematical Logic, part 2, 1970. DOI: http://dx.doi.org/10.1007/978-1-4899-5327-8_16

Negri, S., “Proof analysis in modal logic”, Journal of Philosophical Logic, 34, 5–6 (2005): 507–544. DOI: 10.1007/s10992-005-2267-3

Negri, S., and J. von Plato, Proof Analysis a Contribution to Hilbert’s Last Problem, Cambridge, 2011.

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

Ohnishi, M., and K. Matsumoto, ‘Gentzen method in modal calculi II”, Osaka Mathematical Journal, 11 (1959): 115–120.

Poggiolesi, F., “A cut-free simple sequent calculus for modal logic S5”, Review of Symbolic Logic, 1, 1 (2008): 3–15. DOI: 10.1017/S1755020308080040

Poggiolesi, F., Gentzen Calculi for Modal Propositional Logic, Springer, 2011. DOI: 10.1007/978-90-481-9670-8

Pottinger, G., “Uniform cut-free formulations of T, S4 and S5 (abstract)”, Journal of Symbolic Logic, 48 (1983): 900. DOI: 10.2307/2273495

Restall, G., “Proofnets for S5: Sequents and circuits for modal logic”, pages 151–172 in Logic Colloquium 2005, series “Lecture Notes in Logic”, no. 28, Cambridge University Press, 2007. DOI: 10.1017/CBO9780511546464.012

Sato, M., “A study of Kripke-type models for some modal logics by Gentzen’s sequential method”, Publications of the Research Institute for Mathematical Sciences, Kyoto University, 13 (1977): 381–468.

Stouppa, P., “The design of modal proof theories: the case of S5”, Master Thesis, Dresden, 2004.

Stouppa, P., “A deep inference system for the modal logic S5”, Studia Logica, 85, 2 (2007): 199–214. DOI: 10.1007/s11225-007-9028-y

Takano, M., “Subformula property as a substitute for cut-elimination in modal propositional logics”, Mathematica Japonica, 37, 6 (1992): 1129–1145.

Wansing, H., Displaying Modal Logics, Kluwer Academic Publishers: Dordrecht, 1999. DOI: 10.1007/978-94-017-1280-4

Zeman, J. J., Modal Logic, Oxford University Press, Oxford, 1973.

Logic and Logical Philosophy

Pobrania

  • PDF (English)

Opublikowane

25.08.2015

Jak cytować

1.
BEDNARSKA, Kaja & INDRZEJCZAK, Andrzej. Hypersequent Calculi for S5: The Methods of Cut Elimination. Logic and Logical Philosophy [online]. 25 sierpień 2015, T. 24, nr 3, s. 277–311. [udostępniono 7.7.2025]. DOI 10.12775/LLP.2015.018.
  • PN-ISO 690 (Polski)
  • ACM
  • ACS
  • APA
  • ABNT
  • Chicago
  • Harvard
  • IEEE
  • MLA
  • Turabian
  • Vancouver
Pobierz cytowania
  • Endnote/Zotero/Mendeley (RIS)
  • BibTeX

Numer

Tom 24 Nr 3 (2015): September

Dział

Artykuły

Statystyki

Liczba wyświetleń i pobrań: 798
Liczba cytowań: 11

Crossref
Scopus
Google Scholar
Europe PMC

Wyszukiwanie

Wyszukiwanie

Przeglądaj

  • Indeks autorów
  • Lista archiwalnych numerów

Użytkownik

Użytkownik

Aktualny numer

  • Logo Atom
  • Logo RSS2
  • Logo RSS1

Informacje

  • dla czytelników
  • dla autorów
  • dla bibliotekarzy

Newsletter

Zapisz się Wypisz się

Język / Language

  • English
  • Język Polski

Tagi

Szukaj przy pomocy tagu:

cut elimination, modal logic, hypersequent calculi, proof theory
W górę

Akademicka Platforma Czasopism

Najlepsze czasopisma naukowe i akademickie w jednym miejscu

apcz.umk.pl

Partnerzy platformy czasopism

  • 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
  • Instytut Tomistyczny
  • Karmelitański Instytut Duchowości w Krakowie
  • Ministerstwo Kultury i Dziedzictwa Narodowego
  • 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
  • Polska Fundacja Przemysłu Kosmicznego
  • Polskie Towarzystwo Ekonomiczne
  • Polskie Towarzystwo Ludoznawcze
  • Towarzystwo Miłośników Torunia
  • Towarzystwo Naukowe w Toruniu
  • Uniwersytet im. Adama Mickiewicza w Poznaniu
  • Uniwersytet Komisji Edukacji Narodowej w Krakowie
  • 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- Uniwersytet Mikołaja Kopernika w Toruniu Deklaracja dostępności Sklep wydawnictwa