Bulletin of Symbolic Logic 22 (1):121-144 (2016)

Andrzej Indrzejczak
University of Lodz
Hypersequent calculus, developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi. In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules. Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1017/bsl.2016.2
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,489
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
Display Logic.Nuel D. Belnap - 1982 - Journal of Philosophical Logic 11 (4):375-417.
Logics of Time and Computation.Robert Goldblatt - 1990 - Studia Logica 49 (2):284-286.
A Constructive Analysis of RM.Arnon Avron - 1987 - Journal of Symbolic Logic 52 (4):939 - 951.

View all 19 references / Add more references

Citations of this work BETA

Proof Theory for Functional Modal Logic.Shawn Standefer - 2018 - Studia Logica 106 (1):49-84.

Add more citations

Similar books and articles

Cut-Free Hypersequent Calculus for S4. 3.Andrzej Indrzejczak - 2012 - Bulletin of the Section of Logic 41 (1/2):89-104.
Complexity of Monodic Guarded Fragments Over Linear and Real Time.Ian Hodkinson - 2006 - Annals of Pure and Applied Logic 138 (1):94-125.
Free Will and Time: That "Stuck" Feeling.Brent D. Slife - 1994 - Journal of Theoretical and Philsophical Psychology 14 (1):1-12.
Linear Logic Automata.Max I. Kanovich - 1996 - Annals of Pure and Applied Logic 78 (1-3):147-188.
Some Considerations on Non-Linear Time Intervals.El?Bieta Hajnicz - 1995 - Journal of Logic, Language and Information 4 (4):335-357.
The Postmodern Perspective Of Time In Peter Ackroyd's Hawksmoor.Ana Sentov - 2009 - Facta Universitatis, Series: Linguistics and Literature 7 (1):123-134.
Linear-Time Temporal Logics with Presburger Constraints: An Overview ★.Stéphane Demri - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):311-347.


Added to PP index

Total views
22 ( #515,969 of 2,520,846 )

Recent downloads (6 months)
1 ( #405,457 of 2,520,846 )

How can I increase my downloads?


My notes