A term calculus for Intuitionistic Linear Logic

AbstractThe logics considered here are the propositional Linear Logic and propositional Intuitionistic Linear Logic extended by a knotted structural rule: . It is proved that the class of algebraic models for such a logic has the finite embeddability property, meaning that every finite partial subalgebra of an algebra in the class can be embedded into a finite full algebra in the class. It follows that each such logic has the finite model property with respect to its algebraic semantics and hence that the logic is decidable.

Download Full-text

Reconciling Lambek’s restriction, cut-elimination and substitution in the presence of exponential modalities

Journal of Logic and Computation ◽

10.1093/logcom/exaa010 ◽

2020 ◽

Vol 30 (1) ◽

pp. 239-256 ◽

Cited By ~ 2

Author(s):

Max Kanovich ◽

Stepan Kuznetsov ◽

Andre Scedrov

Keyword(s):

Linear Logic ◽

Cut Elimination ◽

Lambek Calculus ◽

Full Extent ◽

Intuitionistic Linear Logic

Abstract The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. Interestingly enough, we show that for any system equipped with a reasonable exponential modality the following holds: if the system enjoys cut elimination and substitution to the full extent, then the system necessarily violates Lambek’s restriction. Nevertheless, we show that two of the three conditions can be implemented. Namely, we design a system with Lambek’s restriction and cut elimination and another system with Lambek’s restriction and substitution. For both calculi, we prove that they are undecidable, even if we take only one of the two divisions provided by the Lambek calculus. The system with cut elimination and substitution and without Lambek’s restriction is folklore and known to be undecidable.

Download Full-text

Girard translation and logical predicates

Journal of Functional Programming ◽

10.1017/s0956796899003615 ◽

2000 ◽

Vol 10 (1) ◽

pp. 77-89 ◽

Cited By ~ 4

Author(s):

MASAHITO HASEGAWA

Keyword(s):

Short Proof ◽

Linear Logic ◽

Lambda Calculus ◽

Independent Interest ◽

Proof Technique ◽

Typed Lambda Calculus ◽

Intuitionistic Linear Logic

We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete. The proof makes use of a notion of logical predicates for intuitionistic linear logic. While the main result is of independent interest, this paper can be read as a tutorial on this proof technique for reasoning about relations between type theories.

Download Full-text