Admissibility of structural rules for extensions of contraction-free sequent calculi

2001 ◽  
Vol 9 (4) ◽  
pp. 541-548 ◽  
Author(s):  
R Dyckhoff
Keyword(s):  
Sequent Calculi ◽  
Structural Rules

scholarly journals Dynamic sequent calculus for the logic of Epistemic Actions and Knowledge

10.29007/mwpp ◽  
2018 ◽  
Author(s):  
Giuseppe Greco ◽  
Alexander Kurz ◽  
Alessandra Palmigiano
Keyword(s):  
Sequent Calculus ◽  
Relational Semantics ◽  
Sequent Calculi ◽  
Structural Rules ◽  
Epistemic Actions ◽  
Dynamic Logics ◽  
Display Calculi

We develop a family of display-style, cut-free sequent calculi for dynamic epistemic logics on both an intuitionistic and a classical base. Like the standard display calculi, these calculi are modular: just by modifying the structural rules according to Dosen’s principle, these calculi are generalizable both to different Dynamic Logics (Epistemic, Deontic, etc.) and to different propositional bases (Linear, Relevant, etc.). Moreover, the rules they feature agree with the standard relational semantics for dynamic epistemic logics.

Towards an algorithmic construction of cut-elimination procedures

2008 ◽  
Vol 18 (1) ◽  
pp. 81-105 ◽  
Author(s):  
AGATA CIABATTONI ◽  
ALEXANDER LEITSCH
Keyword(s):  
Substructural Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Structural Rules ◽  
Algorithmic Construction ◽  
Logical Rules

We investigate cut elimination in propositional substructural logics. The problem is to decide whether a given calculus admits (reductive) cut elimination. We show that for commutative single-conclusion sequent calculi containing generalised knotted structural rules and arbitrary logical rules the problem can be decided by resolution-based methods. A general cut-elimination proof for these calculi is also provided.

LINEAR TIME IN HYPERSEQUENT FRAMEWORK

2016 ◽  
Vol 22 (1) ◽  
pp. 121-144 ◽  
Author(s):  
ANDRZEJ INDRZEJCZAK
Keyword(s):  
Proof Theory ◽  
Linear Time ◽  
Expressive Power ◽  
Sequent Calculi ◽  
Temporal Logics ◽  
Structural Rules ◽  
Proof Systems ◽  
Nonclassical Logics ◽  
Time Flow ◽  
Basic Calculus

AbstractHypersequent calculus (HC), 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 (SC). 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 (multi)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 (three for future-necessity and three dual rules for past-necessity). 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.

Proof Theory of the Cut Rule

2018 ◽  
Author(s):  
J. R. B. Cockett ◽  
R. A. G. Seely
Keyword(s):  
Proof Theory ◽  
Graphical Representation ◽  
Basic Component ◽  
Graphical Representations ◽  
Mathematical Language ◽  
Basic Logic ◽  
Cut Rule ◽  
Structural Rules ◽  
The One ◽  
Categorical Semantics

This chapter describes the categorical proof theory of the cut rule, a very basic component of any sequent-style presentation of a logic, assuming a minimum of structural rules and connectives, in fact, starting with none. It is shown how logical features can be added to this basic logic in a modular fashion, at each stage showing the appropriate corresponding categorical semantics of the proof theory, starting with multicategories, and moving to linearly distributive categories and *-autonomous categories. A key tool is the use of graphical representations of proofs (“proof circuits”) to represent formal derivations in these logics. This is a powerful symbolism, which on the one hand is a formal mathematical language, but crucially, at the same time, has an intuitive graphical representation.

scholarly journals On the correspondence between nested calculi and semantic systems for intuitionistic logics

2020 ◽  
Author(s):  
Tim Lyon
Keyword(s):  
Intuitionistic Logic ◽  
Structural Rules ◽  
First Order ◽  
Constant Domains ◽  
The Relationship ◽  
Intuitionistic Logics

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.

Sequent Calculi for Global Modal Consequence Relations

Studia Logica ◽  
2018 ◽  
Vol 107 (4) ◽  
pp. 613-637
Author(s):  
Minghui Ma ◽  
Jinsheng Chen
Keyword(s):  
Consequence Relations ◽  
Sequent Calculi
Sign in / Sign up

Export Citation Format

Share Document