Masini, A., 2-Sequent calculus: a proof theory of modalities, Annals of Pure and Applied Logic 58 229–246. In this work we propose an extension of the Getzen sequent calculus in order to deal with modalities. We extend the notion of a sequent obtaining what we call a 2-sequent. For the obtained calculus we prove a cut elimination theorem.

We introduce a two‐dimensional metric (interval) temporal logic whose internal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness and a semantic partial cut elimination theorem down to formulas of a certain type.

We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation.

Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an ω–type schema of inference that naturally interpret the propositional and the predicate until–free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set of (...) extralogical axioms). For each system we provide a syntactic proof of cut elimination and a proof of completeness. (shrink)

We present a sequent calculus for the modal logic S4, and building on some relevant features of this system we show how S4 can easily be translated into full propositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.

1. It is a fact that developing a good proof theory for modal logics is a difficult task. The problem is not in having deductive systems. In fact, all the main modal logics enjoy an axiomatic prese...

We investigate the consequences of removing the infinitary axiom and rules from a previously defined proof system for a fragment of propositional metric temporal logic over dense time.

We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for \(\Box\) and \(\Diamond\). Starting points for this research are 2-sequents and indexed-based calculi (...) (sequents and tableaux). By extending and modifying existing proposals, we show how to achieve a syntactical proof of the cut-elimination theorem that is as close as possible to the one for first-order classical logic. In doing this, we implicitly show how small is the proof-theoretical distance between classical logic and the systems under consideration. (shrink)

We introduce a natural deduction system for the until-free subsystem of the branching time logic Although we work with labelled formulas, our system differs conceptually from the usual labelled deduction systems because we have no relational formulas. Moreover, no deduction rule embodies semantic features such as properties of accessibility relation or similar algebraic properties. We provide a suitable semantics for our system and prove that it is sound and weakly complete with respect to such semantics.

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in (...) contrast, we make explicit this duality of until by introducing a new temporal operator ∇ that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and ẃ. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system N(LTL∇) for a linear-time logic LTL∇ endowed with the new history operator. We show that LTL∇ is equivalent to the linear temporal logic LTL with until, which follows by formalizing back and forth translations between the two logics. We also define an indirect translation from LTL∇ into LTL via temporal logics with past operators; such a result provides an upper bound to the problem of satisfiability for LTL∇ formulas. (shrink)

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in (...) contrast, we make explicit this duality of until by introducing a new temporal operator ∇ that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and ẃ. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system N(LTL∇) for a linear-time logic LTL∇ endowed with the new history operator. We show that LTL∇ is equivalent to the linear temporal logic LTL with until, which follows by formalizing back and forth translations between the two logics. We also define an indirect translation from LTL∇ into LTL via temporal logics with past operators; such a result provides an upper bound to the problem of satisfiability for LTL∇ formulas. (shrink)