A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel–McKinsey–Tarski embedding

2013 ◽  
Vol 26 (1) ◽  
pp. 169-187 ◽  
Author(s):  
Roy Dyckhoff ◽  
Sara Negri
Keyword(s):  
Grzegorczyk Logic ◽  
Sequent System

scholarly journals One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity

2020 ◽  
Author(s):  
Paweł Płaczek
Keyword(s):  
Analogous Result ◽  
Cut Elimination ◽  
Sequent Systems ◽  
Natural Symmetry ◽  
Sequent System

Bilinear Logic of Lambek [10] amounts to Noncommutative MALL of Abrusci [1]. Lambek [10] proves the cut–elimination theorem for a onesided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek [10], we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTIME complexity of the multiplicative fragment of NBL.

scholarly journals Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity

2017 ◽  
Vol 46 (1/2) ◽  
Author(s):  
Wojciech Buszkowski
Keyword(s):  
Cut Elimination ◽  
Lambek Calculus ◽  
Double Negation ◽  
Sequent Systems ◽  
Sequent System

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.

A note on the system GRW with the intensional contraction rule

2020 ◽  
Author(s):  
Mirjana Ilić ◽  
Branislav Boričić
Keyword(s):  
Sequent Calculus ◽  
Relevant Logic ◽  
Structural Rule ◽  
The Right ◽  
Sequent System

Abstract In Ilić and Boričić (2014, Log. J. IGPL, 22, 673–695), the right-handed cut-free sequent calculus $GRW$ for the contraction-less relevant logic $RW$ is defined. In this paper, we show that the enlargement of the system $GRW$ with the structural rule of intensional contraction (WI) presents the sequent system for the principal relevant logic $R$ but the rule of cut cannot be eliminated in $GRW+$(WI).

Cut-elimination for Weak Grzegorczyk Logic Go

Studia Logica ◽  
2012 ◽  
Vol 102 (1) ◽  
pp. 1-27 ◽  
Author(s):  
Rajeev Goré ◽  
Revantha Ramanayake
Keyword(s):  
Cut Elimination ◽  
Grzegorczyk Logic

A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language

2011 ◽  
Vol 76 (2) ◽  
pp. 673-699 ◽  
Author(s):  
Michael Gabbay
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Functional Programming ◽  
Order Logic ◽  
First Order Logic ◽  
Cut Elimination ◽  
Logic Programming Language ◽  
First Order ◽  
Functional Programming Language ◽  
Sequent System

AbstractWe build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic.We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

The subformula property of natural deduction derivations and analytic cuts

2020 ◽  
Author(s):  
Mirjana Borisavljević
Keyword(s):  
Natural Deduction ◽  
Deduction System ◽  
Natural Deduction System ◽  
Sequent System ◽  
Subformula Property

Abstract In derivations of a sequent system, $\mathcal{L}\mathcal{J}$, and a natural deduction system, $\mathcal{N}\mathcal{J}$, the trails of formulae and the subformula property based on these trails will be defined. The derivations of $\mathcal{N}\mathcal{J}$ and $\mathcal{L}\mathcal{J}$ will be connected by the map $g$, and it will be proved the following: an $\mathcal{N}\mathcal{J}$-derivation is normal $\Longleftrightarrow $ it has the subformula property based on trails $\Longleftrightarrow $ its $g$-image in $\mathcal{L}\mathcal{J}$ is without maximum cuts $\Longrightarrow $ that $g$-image has the subformula property based on trails. In $\mathcal{L}\mathcal{J}$-derivations, another type of cuts, sub-cuts, will be introduced, and it will be proved the following: all cuts of an $\mathcal{L}\mathcal{J}$-derivation are sub-cuts $\Longleftrightarrow $ it has the subformula property based on trails.

scholarly journals On the Minimal Non-Fregean Grzegorczyk Logic

Studia Logica ◽  
2015 ◽  
Vol 104 (2) ◽  
pp. 209-234 ◽  
Author(s):  
Joanna Golińska-Pilarek
Keyword(s):  
Grzegorczyk Logic

scholarly journals Free lattices proof-theoretically

2020 ◽  
Vol 17 (2) ◽  
pp. 110
Author(s):  
Tomasz Kowalski
Keyword(s):  
Proof Systems ◽  
Sequent System

A sequent system is used to give alternative proofs of two well known properties of free lattices: Whitman’s condition and semidistributivity. It demonstrates usefulness of such proof systems outside logic.

Sign in / Sign up

Export Citation Format

Share Document