scholarly journals FULL LAMBEK CALCULUS WITH CONTRACTION IS UNDECIDABLE

2016 ◽  
Vol 81 (2) ◽  
pp. 524-540 ◽  
Author(s):  
KAREL CHVALOVSKÝ ◽  
ROSTISLAV HORČÍK
Keyword(s):  
Lambek Calculus ◽  
Structural Rule

AbstractWe prove that the set of formulae provable in the full Lambek calculus with the structural rule of contraction is undecidable. In fact, we show that the positive fragment of this logic is undecidable.

Interpolation in fragments of classical linear logic

1994 ◽  
Vol 59 (2) ◽  
pp. 419-444 ◽  
Author(s):  
Dirk Roorda
Keyword(s):  
Intuitionistic Logic ◽  
Linear Logic ◽  
Quantum Graphs ◽  
Lambek Calculus ◽  
Structural Rule ◽  
Proof Nets

AbstractWe study interpolation for elementary fragments of classical linear logic. Unlike in intuitionistic logic (see [Renardel de Lavalette, 1989]) there are fragments in linear logic for which interpolation does not hold. We prove interpolation for a lot of fragments and refute it for the multiplicative fragment (→, +), using proof nets and quantum graphs. We give a separate proof for the fragment with implication and product, but without the structural rule of permutation. This is nearly the Lambek calculus. There is an appendix explaining what quantum graphs are and how they relate to proof nets.

Structural Rule of N-Coordinated Single Atomic Catalysts for Electrochemical CO2 Reduction

2022 ◽  
Author(s):  
Zhenxin Lou ◽  
Wenjing Li ◽  
Haiyang Yuan ◽  
Yu Hou ◽  
Huagui Yang ◽  
...  
Keyword(s):  
Co2 Reduction ◽  
Single Atom ◽  
Structural Rule ◽  
Metal Centers ◽  
Nitrogen Doped ◽  
Electrochemical Co2 Reduction

Metal single-atom catalysts (SACs) on nitrogen-doped carbons exhibit an attractive prospect in catalysis. However, how to quickly collocate various metal centers with diversified N-coordination topologic structures to maximize the catalytic...

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.

UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS

2014 ◽  
Vol 7 (3) ◽  
pp. 455-483 ◽  
Author(s):  
MAJID ALIZADEH ◽  
FARZANEH DERAKHSHAN ◽  
HIROAKIRA ONO
Keyword(s):  
Propositional Logic ◽  
Predicate Logic ◽  
Interpolation Property ◽  
Substructural Logics ◽  
Substructural Logic ◽  
Sequent Calculi ◽  
Structural Rule ◽  
Modal Propositional Logic ◽  
Uniform Interpolation ◽  
Classical Predicate

AbstractUniform interpolation property of a given logic is a stronger form of Craig’s interpolation property where both pre-interpolant and post-interpolant always exist uniformly for any provable implication in the logic. It is known that there exist logics, e.g., modal propositional logic S4, which have Craig’s interpolation property but do not have uniform interpolation property. The situation is even worse for predicate logics, as classical predicate logic does not have uniform interpolation property as pointed out by L. Henkin.In this paper, uniform interpolation property of basic substructural logics is studied by applying the proof-theoretic method introduced by A. Pitts (Pitts, 1992). It is shown that uniform interpolation property holds even for their predicate extensions, as long as they can be formalized by sequent calculi without contraction rules. For instance, uniform interpolation property of full Lambek predicate calculus, i.e., the substructural logic without any structural rule, and of both linear and affine predicate logics without exponentials are proved.

scholarly journals Undecidability of the Lambek Calculus with a Relevant Modality

2016 ◽  
pp. 240-256 ◽  
Author(s):  
Max Kanovich ◽  
Stepan Kuznetsov ◽  
Andre Scedrov
Keyword(s):  
Lambek Calculus
Sign in / Sign up

Export Citation Format

Share Document