Displaying similar documents to “Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus”

The Method of Socratic Proofs Meets Correspondence Analysis

Dorota Leszczyńska-Jasion, Yaroslav Petrukhin, Vasilyi Shangin (2019)

Bulletin of the Section of Logic

Similarity:

The goal of this paper is to propose correspondence analysis as a technique for generating the so-called erotetic (i.e. pertaining to the logic of questions) calculi which constitute the method of Socratic proofs by Andrzej Wiśniewski. As we explain in the paper, in order to successfully design an erotetic calculus one needs invertible sequent-calculus-style rules. For this reason, the proposed correspondence analysis resulting in invertible rules can constitute a new foundation for...

Empirical Negation, Co-Negation and the Contraposition Rule II: Proof-Theoretical Investigations

Satoru Niki (2020)

Bulletin of the Section of Logic

Similarity:

We continue the investigation of the first paper where we studied logics with various negations including empirical negation and co-negation. We established how such logics can be treated uniformly with R. Sylvan's CCω as the basis. In this paper we use this result to obtain cut-free labelled sequent calculi for the logics.

New Modification of the Subformula Property for a Modal Logic

Mitio Takano (2020)

Bulletin of the Section of Logic

Similarity:

A modified subformula property for the modal logic KD with the additionalaxiom □ ◊(A ∨ B) ⊃ □ ◊ A ∨ □ ◊B is shown. A new modification of the notion of subformula is proposed for this purpose. This modification forms a natural extension of our former one on which modified subformula property for the modal logics K5, K5D and S4.2 has been shown ([2] and [4]). The finite model property as well as decidability for the logic follows from this.

A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs

George Tourlakis (2016)

Bulletin of the Section of Logic

Similarity:

Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable....

Functional Completeness in CPL via Correspondence Analysis

Dorota Leszczyńska-Jasion, Yaroslav Petrukhin, Vasilyi Shangin, Marcin Jukiewicz (2019)

Bulletin of the Section of Logic

Similarity:

Kooi and Tamminga's correspondence analysis is a technique for designing proof systems, mostly, natural deduction and sequent systems. In this paper it is used to generate sequent calculi with invertible rules, whose only branching rule is the rule of cut. The calculi pertain to classical propositional logic and any of its fragments that may be obtained from adding a set (sets) of rules characterizing a two-argument Boolean function(s) to the negation fragment of classical propositional...

An Alternative Natural Deduction for the Intuitionistic Propositional Logic

Mirjana Ilić (2016)

Bulletin of the Section of Logic

Similarity:

A natural deduction system NI, for the full propositional intuitionistic logic, is proposed. The operational rules of NI are obtained by the translation from Gentzen’s calculus LJ and the normalization is proved, via translations from sequent calculus derivations to natural deduction derivations and back.

A Modified Subformula Property for the Modal Logic S4.2

Mitio Takano (2019)

Bulletin of the Section of Logic

Similarity:

The modal logic S4.2 is S4 with the additional axiom ◊□A ⊃ □◊A. In this article, the sequent calculus GS4.2 for this logic is presented, and by imposing an appropriate restriction on the application of the cut-rule, it is shown that, every GS4.2-provable sequent S has a GS4.2-proof such that every formula occurring in it is either a subformula of some formula in S, or the formula □¬□B or ¬□B, where □B occurs in the scope of some occurrence of □ in some formula of S. These are just the...

Super-strict Implications

Guido Gherardi, Eugenio Orlandelli (2021)

Bulletin of the Section of Logic

Similarity:

This paper introduces the logics of super-strict implications, where a super-strict implication is a strengthening of C.I. Lewis' strict implication that avoids not only the paradoxes of material implication but also those of strict implication. The semantics of super-strict implications is obtained by strengthening the (normal) relational semantics for strict implication. We consider all logics of super-strict implications that are based on relational frames for modal logics in the...

Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity

Wojciech Buszkowski (2017)

Bulletin of the Section of Logic

Similarity:

In [5] we study Nonassociative Lambek Calculus (NL) augmented with De Morgan negation, satisfying the double negation and contraposition laws. This logic, introduced by de Grooté and Lamarche [10], is called Classical Non-Associative Lambek Calculus (CNL). Here we study a weaker logic InNL, i.e. NL with two involutive negations. We present a one-sided sequent system for InNL, admitting cut elimination. We also prove that InNL is PTIME.

Semantical Proof of Subformula Property for the Modal Logics K4.3, KD4.3, and S4.3

Daishi Yazaki (2019)

Bulletin of the Section of Logic

Similarity:

The main purpose of this paper is to give alternative proofs of syntactical and semantical properties, i.e. the subformula property and the nite model property, of the sequent calculi for the modal logics K4.3, KD4.3, and S4.3. The application of the inference rules is said to be acceptable, if all the formulas in the upper sequents are subformula of the formulas in lower sequent. For some modal logics, Takano analyzed the relationships between the acceptable inference rules and semantical...

Axiomatization of a Basic Logic of Logical Bilattices

Mitio Takano (2016)

Bulletin of the Section of Logic

Similarity:

A sequential axiomatization is given for the 16-valued logic that has been proposed by Shramko-Wansing (J Philos Logic 34:121–153, 2005) as a candidate for the basic logic of logical bilattices.

Modal Boolean Connexive Logics: Semantics and Tableau Approach

Tomasz Jarmużek, Jacek Malinowski (2019)

Bulletin of the Section of Logic

Similarity:

In this paper we investigate Boolean connexive logics in a language with modal operators: □, ◊. In such logics, negation, conjunction, and disjunction behave in a classical, Boolean way. Only implication is non-classical. We construct these logics by mixing relating semantics with possible worlds. This way, we obtain connexive counterparts of basic normal modal logics. However, most of their traditional axioms formulated in terms of modalities and implication do not hold anymore without...

An Investigation into Intuitionistic Logic with Identity

Szymon Chlebowski, Dorota Leszczyńska-Jasion (2019)

Bulletin of the Section of Logic

Similarity:

We define Kripke semantics for propositional intuitionistic logic with Suszko’s identity (ISCI). We propose sequent calculus for ISCI along with cut-elimination theorem. We sketch a constructive interpretation of Suszko’s propositional identity connective.

Empirical Negation, Co-negation and Contraposition Rule I: Semantical Investigations

Satoru Niki (2020)

Bulletin of the Section of Logic

Similarity:

We investigate the relationship between M. De's empirical negation in Kripke and Beth Semantics. It turns out empirical negation, as well as co-negation, corresponds to different logics under different semantics. We then establish the relationship between logics related to these negations under unified syntax and semantics based on R. Sylvan's CCω.

Rule-Generation Theorem and its Applications

Andrzej Indrzejczak (2018)

Bulletin of the Section of Logic

Similarity:

In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some...

From Intuitionism to Brouwer's Modal Logic

Zofia Kostrzycka (2020)

Bulletin of the Section of Logic

Similarity:

We try to translate the intuitionistic propositional logic INT into Brouwer's modal logic KTB. Our translation is motivated by intuitions behind Brouwer's axiom p →☐◊p The main idea is to interpret intuitionistic implication as modal strict implication, whereas variables and other positive sentences remain as they are. The proposed translation preserves fragments of the Rieger-Nishimura lattice which is the Lindenbaum algebra of monadic formulas in INT. Unfortunately, INT is not embedded...

Intuitionistic logic considered as an extension of classical logic : some critical remarks

Javier Legris, Jorge A. Molina (2001)

Philosophia Scientiae

Similarity:

In this paper we analyze the consideration of intuitionistic logic as an extension of classical logic. This — at first sight surprising — point of view has been sustained explicitly by Jan Łukasiewicz on the basis of a mapping of classical propositional logic into intuitionistic propositional logic by Kurt Gödel in 1933. Simultaneously with Gödel, Gerhard Gentzen had proposed another mapping of Peano´s arithmetic into Heyting´s arithmetic. We shall discuss these mappings in connection...