Sequent Calculi for Intuitionistic Linear Logic with Strong Negation

2002 ◽  
Vol 10 (6) ◽  
pp. 653-678 ◽  
Author(s):  
N. Kamide
2021 ◽  
pp. 115-141
Author(s):  
Christian G. Fermüller

Abstract Lorenzen has introduced his dialogical approach to the foundations of logic in the late 1950s to justify intuitionistic logic with respect to first principles about constructive reasoning. In the decades that have passed since, Lorenzen-style dialogue games turned out to be an inspiration for a more pluralistic approach to logical reasoning that covers a wide array of nonclassical logics. In particular, the close connection between (single-sided) sequent calculi and dialogue games is an invitation to look at substructural logics from a dialogical point of view. Focusing on intuitionistic linear logic, we illustrate that intuitions about resource-conscious reasoning are well served by translating sequent calculi into Lorenzen-style dialogue games. We suggest that these dialogue games may be understood as games of information extraction, where a sequent corresponds to the claim that a certain information package can be systematically extracted from a given bundle of such packages of logically structured information. As we will indicate, this opens the field for exploring new logical connectives arising by consideration of further forms of storing and structuring information.


2005 ◽  
Vol 13 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Maria Emilia Maietti ◽  
Paola Maneggia ◽  
Valeria de Paiva ◽  
Eike Ritter

2005 ◽  
Vol 70 (1) ◽  
pp. 84-98 ◽  
Author(s):  
C. J. van Alten

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.


Sign in / Sign up

Export Citation Format

Share Document