The undecidability of second order linear logic without exponentials

1996 ◽  
Vol 61 (2) ◽  
pp. 541-548 ◽  
Author(s):  
Yves Lafont
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Linear Logic ◽  
Classical Case ◽  
Second Order ◽  
Order Linear ◽  
Phase Semantics ◽  
Counter Machines ◽  
Intuitionistic Linear Logic

AbstractRecently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment of second order intuitionistic linear logic is undecidable, using an encoding of second order intuitionistic logic. Their argument applies to the multiplicative-additive fragment, but it does not work in the classical case, because second order classical logic is decidable. Here we show that the multiplicative-additive fragment of second order classical linear logic is also undecidable, using an encoding of two-counter machines originally due to Kanovich. The faithfulness of this encoding is proved by means of the phase semantics.

On the unification of classical, intuitionistic and affine logics

2018 ◽  
Vol 29 (8) ◽  
pp. 1177-1216
Author(s):  
CHUCK LIANG
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Kripke Semantics ◽  
Cut Elimination ◽  
Structural Rules ◽  
Phase Semantics ◽  
Intuitionistic Logics

This article presents a unified logic that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the λμ calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.

scholarly journals A phase semantics for polarized linear logic and second order conservativity

2010 ◽  
Vol 75 (1) ◽  
pp. 77-102 ◽  
Author(s):  
Masahiro Hamano ◽  
Ryo Takemura
Keyword(s):  
Topological Structure ◽  
Linear Logic ◽  
Second Order ◽  
Order Linear ◽  
First Order ◽  
Counter Model ◽  
Linear Fragment ◽  
Phase Semantics ◽  
Second Order Systems ◽  
Completeness Theorems

AbstractThis paper presents a polarized phase semantics, with respect to which the linear fragment of second order polarized linear logic of Laurent [15] is complete. This is done by adding a topological structure to Girard's phase semantics [9], The topological structure results naturally from the categorical construction developed by Hamano–Scott [12]. The polarity shifting operator ↓ (resp. ↑) is interpreted as an interior (resp. closure) operator in such a manner that positive (resp. negative) formulas correspond to open (resp. closed) facts. By accommodating the exponentials of linear logic, our model is extended to the polarized fragment of the second order linear logic. Strong forms of completeness theorems are given to yield cut-eliminations for the both second order systems. As an application of our semantics, the first order conservativity of linear logic is studied over its polarized fragment of Laurent [16]. Using a counter model construction, the extension of this conservativity is shown to fail into the second order, whose solution is posed as an open problem in [16]. After this negative result, a second order conservativity theorem is proved for an eta expanded fragment of the second order linear logic, which fragment retains a focalized sequent property of [3].

Decision Problems for Second-Order Linear Logic

1997 ◽  
pp. 127-143
Author(s):  
P. D. Lincoln ◽  
A. Scedrov ◽  
N. Shankar
Keyword(s):  
Linear Logic ◽  
Second Order ◽  
Decision Problems ◽  
Order Linear

On storage operators

1998 ◽  
Author(s):  
Karim Nour
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Input Data ◽  
Type System ◽  
Second Order ◽  
Data Type ◽  
Simple Type ◽  
Output Data ◽  
Major Drawback ◽  
Proof Rules

λ-calculus as such is not a computational model. A reduction strategy is needed. In this paper, we consider λ-calculus with the left reduction. This strategy has many advantages: it always terminates when applied to a normalizable λ-term and it seems more economic since we compute λ-term only when we need it. But the major drawback of this strategy is that a function must compute its argument every time it uses it. This is the reason why this strategy is not really used. In 1990 Krivine (1990b) introduced the notion of storage operators in order to avoid this problem and to simulate call-by-value when necessary. The AF2 type system is a way of interpreting the proof rules for second-order intuitionistic logic plus equational reasoning as construction rules for terms. Krivine (1990b) has shown that, by using Gödel translation from classical to intuitionistic logic (denoted byg), we can find in system AF2 a very simple type for storage operators. Historically the type was discovered before the notion of storage operator itself. Krivine (1990a) proved that as far as totality of functions is concerned second-order classical logic is conservative over second-order intuitionistic logic. To prove this, Krivine introduced the following notions: A[x] is an input (resp. output) data type if one can prove intuitionistically A[x] → Ag[x] (resp. Ag[x] → ⇁⇁A[x]). Then if A[x] is an input data type and B[x] is an output data type, then if one can prove A[x] → B[x] classically one can prove it intuitionistically. The notion of storage operator was discovered by investigating the property of all λ-terms of type Ng[x] → ⇁⇁N[x] where N[x] is the type of integers. Parigot (1992) and Krivine (1994) have extended the AF2 system to classical logic. The method of Krivine is very simple: it consists of adding a new constant, denoted by C, with the declaration С: ∀X{⇁⇁ X → X} which axiomatizes classical logic over intuitionistic logic. For the constant C, he adds a new reduction rule which is a particular case of a rule given by Felleisen (1987) for control operator.

scholarly journals Connecting Sequent Calculi with Lorenzen-Style Dialogue Games

2021 ◽  
pp. 115-141
Author(s):  
Christian G. Fermüller
Keyword(s):  
Intuitionistic Logic ◽  
Linear Logic ◽  
Substructural Logics ◽  
Point Of View ◽  
Sequent Calculi ◽  
Dialogue Games ◽  
Structured Information ◽  
Logical Connectives ◽  
Pluralistic Approach ◽  
Intuitionistic Linear Logic

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.

A new deconstructive logic: linear logic

1997 ◽  
Vol 62 (3) ◽  
pp. 755-807 ◽  
Author(s):  
Vincent Danos ◽  
Jean-Baptiste Joinet ◽  
Harold Schellinx
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Predicate Logic ◽  
Linear Logic ◽  
Second Order ◽  
Main Concern ◽  
Simple Pattern ◽  
Strong Normalization ◽  
Viable Systems ◽  
Proof Nets

AbstractThe main concern of this paper is the design of a noetherian and confluent normalization for LK2 (that is, classical second order predicate logic presented as a sequent calculus).The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of ‘programming-with-proofs’ ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making.A comparison of our method to that of embedding LK into LJ (intuitionistic sequent calculus) brings to the fore the latter's defects for these ‘deconstructive purposes’.

scholarly journals The Girard Translation Extended with Recursion

1995 ◽  
Vol 2 (13) ◽  
Author(s):  
Torben Braüner
Keyword(s):  
Intuitionistic Logic ◽  
Linear Logic ◽  
Full Version ◽  
Intuitionistic Linear Logic

<p>This paper extends Curry-Howard interpretations of Intuitionistic Logic (IL) and Intuitionistic Linear Logic (ILL) with rules for recursion. The resulting term languages, the rec-calculus and the linear rec-calculus respectively, are given sound<br />categorical interpretations. The embedding of proofs of IL into proofs of ILL given by the Girard Translation is extended with the rules for recursion, such that an embedding of terms of the rec-calculus into terms of the linear rec-calculus is induced via the extended Curry-Howard isomorphisms. This embedding is shown to be sound with respect to the categorical interpretations.</p><p><br />Full version of paper to appear in Proceedings of CSL '94, LNCS 933, 1995.

Sign in / Sign up

Export Citation Format

Share Document