scholarly journals S5-Style Non-Standard Modalities in a Hypersequent Framework

2021 ◽  
pp. 1-30
Author(s):  
Yaroslav Petrukhin
Keyword(s):  
Cut Elimination ◽  
Hypersequent Calculi ◽  
Soundness And Completeness ◽  
Completeness Theorems

The aim of the paper is to present some non-standard modalities (such as non-contingency, contingency, essence and accident) based on S5-models in a framework of cut-free hypersequent calculi. We also study negated modalities, i.e. negated necessity and negated possibility, which produce paraconsistent and paracomplete negations respectively. As a basis for our calculi, we use Restall's cut-free hypersequent calculus for S5. We modify its rules for the above-mentioned modalities and prove strong soundness and completeness theorems by a Hintikka-style argument. As a consequence, we obtain a cut admissibility theorem. Finally, we present a constructive syntactic proof of cut elimination theorem.

scholarly journals Bunched Hypersequent Calculi for Distributive Substructural Logics

10.29007/ngp3 ◽  
2018 ◽  
Author(s):  
Agata Ciabattoni ◽  
Revantha Ramanayake
Keyword(s):  
Large Class ◽  
General Rule ◽  
Expressive Power ◽  
Substructural Logics ◽  
Cut Elimination ◽  
Lambek Calculus ◽  
Hypersequent Calculi

We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. A general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions is then proved. We adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.

scholarly journals Cut Elimination Theorem for Non-Commutative Hypersequent Calculus

2017 ◽  
Vol 46 (1/2) ◽  
Author(s):  
Andrzej Indrzejczak
Keyword(s):  
Temporal Logic ◽  
Cut Elimination ◽  
Temporal Logics ◽  
Hypersequent Calculi ◽  
Flow Of Time

Hypersequent calculi (HC) can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.

scholarly journals Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity

2020 ◽  
Author(s):  
Tiziano Dalmonte ◽  
Björn Lellmann ◽  
Nicola Olivetti ◽  
Elaine Pimentel
Keyword(s):  
Search Strategy ◽  
Cut Elimination ◽  
Relational Semantics ◽  
Optimal Complexity ◽  
Proof Search ◽  
Polynomial Size ◽  
Hypersequent Calculi

Abstract We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms ${T}$, ${P}$ and ${D}$ and for every $n \geq 1$, rule ${RD}_n^+$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.

scholarly journals Cut free sequent calculus for logic S5n(ED)

2010 ◽  
Vol 51 ◽  
Author(s):  
Haroldas Giedra
Keyword(s):  
Sequent Calculus ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Soundness And Completeness

Hilbert style, Gentzen style sequent and Kanger style sequent calculi for logic S5n(ED) are considered in this paper. Gentzen style sequent calculus is constructed and its equivalence with Hilbert style system is proved, getting soundness and  completeness of Gentzen style system. Kanger style indexed sequent calculus is defined for cut elimination.

scholarly journals Multisequent Gentzen Deduction Systems For B2 2-Valued First-Order Logic

2018 ◽  
Vol 7 (1) ◽  
pp. 53
Author(s):  
Wei Li ◽  
Yuefei Sui
Keyword(s):  
Boolean Algebra ◽  
Order Logic ◽  
First Order Logic ◽  
Deduction System ◽  
Truth Values ◽  
First Order ◽  
Soundness And Completeness ◽  
Completeness Theorems

For the four-element Boolean algebra B22, a multisequent Г|Δ|∑|∏ is a generalization of sequent Г→Δ in traditional B22 valued first-order logic. By defining the truth-values of quantified formulas, a Gentzen deduction system G22 for B22-valued first-order logic will be built and its soundness and completeness theorems will be proved.

scholarly journals Ternary Relational Semantics for the Variants of BN4 and E4 which Contain Routley and Meyer's Logic B

2021 ◽  
Author(s):  
Sandra M. López
Keyword(s):  
Relational Semantics ◽  
Basic Logic ◽  
Relevant Logics ◽  
The Family ◽  
Soundness And Completeness ◽  
Completeness Theorems

Six hopefully interesting variants of the logics BN4 and E4 – which can be considered as the 4-valued logics of the relevant conditional and (relevant) entailment, respectively – were previously developed in the literature. All these systems are related to the family of relevant logics and contain Routley and Meyer's basic logic B, which is well-known to be specifically associated with the ternary relational semantics. The aim of this paper is to develop reduced general Routley-Meyer semantics for them. Strong soundness and completeness theorems are proved for each one of the logics.

TRANSITIVE PRIMAL INFON LOGIC

2013 ◽  
Vol 6 (2) ◽  
pp. 281-304 ◽  
Author(s):  
CARLOS COTRINI ◽  
YURI GUREVICH
Keyword(s):  
Access Control ◽  
Linear Time ◽  
Kripke Models ◽  
Control Applications ◽  
Traditional Logic ◽  
Soundness And Completeness ◽  
Image Position ◽  
Small Models ◽  
Completeness Theorems ◽  
Subformula Property

AbstractPrimal infon logic was introduced in 2009 in connection with access control. In addition to traditional logic constructs, it contains unary connectives p said indispensable in the intended access control applications. Propositional primal infon logic is decidable in linear time, yet suffices for many common access control scenarios. The most obvious limitation on its expressivity is the failure of the transitivity law for implication: $x \to y$ and $y \to z$ do not necessarily yield $x \to z$. Here we introduce and investigate equiexpressive “transitive” extensions TPIL and TPIL* of propositional primal infon logic as well as their quote-free fragments TPIL0 and TPIL0* respectively. We prove the subformula property for TPIL0* and a similar property for TPIL*; we define Kripke models for the four logics and prove the corresponding soundness-and-completeness theorems; we show that, in all these logics, satisfiable formulas have small models; but our main result is a quadratic-time derivation algorithm for TPIL*.

Sign in / Sign up

Export Citation Format

Share Document