We introduce an extended intuitionistic linear logic with strong negation and modality. The logic presented is a modal extension of Wansing's extended linear logic with strong negation. First, we propose three types of cut-free sequent calculi for this new logic. The first one is named a subformula calculus, which yields the subformula property. The second one is termed a dual calculus, which has positive and negative sequents. The third (...) one is called a triple-context calculus, which is regarded as a natural extension or generalization of Hodas and Miller's dual-context calculus appearing in a linear logic programming language. Second, we present a concurrent process calculus based on the logic. This calculus is an extension of Okada's process calculus. Third, we introduce a Kripke type semantics for a fragment of the logic, and show the completeness theorems with respect to the semantics. Finally, we mention a logic programming language based on the triple-context calculus. (shrink)

We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.

A new logic, quantized intuitionistic linear logic, is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's involutive quantales. Some cut-free sequent calculi with a new property quantization principle and some complete semantics such as an involutive quantale model and a quantale model are obtained for QILL. The relationship between QILL and Wansing's extended intuitionistic linear logic with strong negation is also observed using such syntactical (...) and semantical frameworks. (shrink)

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL ew of the substructural logic FL ew . In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL ew (namely, a certain variety of FL ew -algebras) are term equivalent. This answers a (...) longstanding question of Nelson [30]. Extensive use is made of the automated theorem-prover Prover9 in order to establish the result. The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL ew are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL ew. (shrink)

Wansing’s extended intuitionistic linear logic with strong negation, called WILL, is regarded as a resource-conscious refinment of Nelson’s constructive logics with strong negation. In this paper, (1) the completeness theorem with respect to phase semantics is proved for WILL using a method that simultaneously derives the cut-elimination theorem, (2) a simple correspondence between the class of Petri nets with inhibitor arcs and a fragment of WILL is obtained using a Kripke (...) semantics, (3) a cut-free sequent calculus for WILL, called twist calculus, is presented, (4) a strongly normalizable typed λ-calculus is obtained for a fragment of WILL, and (5) new applications of WILL in medical diagnosis and electric circuit theory are proposed. Strong negation in WILL is found to be expressible as a resource-conscious refutability, and is shown to correspond to inhibitor arcs in Petri net theory. (shrink)

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL ew of the substructural logic FL ew. The main result of Part I of this series [41] shows that the equivalent variety semantics of N and the equivalent variety semantics of NFL ew are term equivalent. In this paper, the term equivalence result of Part I [41] is lifted (...) to the setting of deductive systems to establish the definitional equivalence of the logics N and NFL ew. It follows from the definitional equivalence of these systems that constructive logic with strong negation is a substructural logic. (shrink)

This paper is a reaction to the following remark by grzegorczyk: "the compound sentences are not a product of experiment. they arise from reasoning. this concerns also negations; we see that the lemon is yellow, we do not see that it is not blue." generally, in science the truth is ascertained as indirectly as falsehood. an example: a litmus-paper is used to verify the sentence "the solution is acid." this approach gives rise to a (very intuitionistic indeed) conservative extension of (...) the heyting logic satisfying natural duality laws. (shrink)

Motivated by the definition of semi-Nelson algebras, a propositional calculus called semi-intuitionistic logic with strong negation is introduced and proved to be complete with respect to that class of algebras. An axiomatic extension is proved to have as algebraic semantics the class of Nelson algebras.

This paper deals with, prepositional calculi with strong negation (N-logics) in which the Craig interpolation theorem holds. N-logics are defined to be axiomatic strengthenings of the intuitionistic calculus enriched with a unary connective called strong negation. There exists continuum of N-logics, but the Craig interpolation theorem holds only in 14 of them.

We introduce Kripke models for propositional substructural logics with strong negation, and show the completeness theorems for these logics using an extended Ishihara's canonical model construction method. The framework presented can deal with a broad range of substructural logics with strong negation, including a modified version of Nelson's logic N$^-$, Wansing's logic COSPL, and extended versions of Visser's basic propositional logic, positive relevant logics, Corsi's logics and M\'endez's logics.

In this paper, we introduce a Hilbert style axiomatic calculus for intutionistic logic with strong negation. This calculus is a preservative extension of intuitionistic logic, but it can express that some falsity are constructive. We show that the introduction of strong negation allows us to define a square of opposition based on quantification on possible worlds.

We study axiomatic extensions of the propositional constructive logic with strong negation having the disjunction property in terms of corresponding to them varieties of Nelson algebras. Any such varietyV is characterized by the property: (PQWC) ifA,B V, thenA×B is a homomorphic image of some well-connected algebra ofV.We prove:• each varietyV of Nelson algebras with PQWC lies in the fibre –1(W) for some varietyW of Heyting algebras having PQWC, • for any varietyW of Heyting algebras (...) class='Hi'>with PQWC the least and the greatest varieties in –1(W) have PQWC, • there exist varietiesW of Heyting algebras having PQWC such that –1(W) contains infinitely many varieties (of Nelson algebras) with PQWC. (shrink)

The aim of the paper is to show that topoi are useful in the categorial analysis of the constructive logic with strong negation. In any topos ϵ we can distinguish an object Λ and its truth-arrows such that sets ϵ have a Nelson algebra structure. The object Λ is defined by the categorial counterpart of the algebraic FIDEL-VAKARELOV construction. Then it is possible to define the universal quantifier morphism which permits us to make the first order (...) predicate calculus. The completeness theorem is proved using the Kripke-type semantic defined by THOMASON. (shrink)

A sufficient condition for an extension of positive logic with strong negation to be characterized by a class of finite trees is given.

Just as intuitionistic proofs can be modeled by functions, linear logic proofs, being symmetric in the inputs and outputs, can be modeled by relations . However generic relations do not establish any functional dependence between the arguments, and therefore it is questionable whether they can be thought as reasonable generalizations of functions. On the other hand, in some situations one can speak in some precise sense about an implicit functional dependence defined by a relation. It turns out that (...) it is possible to model linear logic with implicit functions rather than general relations, an adequate language for such a semantics being differential calculus. This results in a non-degenerate model enjoying quite strong completeness properties. (shrink)

Let denote a first‐order logic in a language that contains infinitely many constant symbols and also containing intuitionistic logic. By, we mean the associated logic axiomatized by the double negation of the universal closure of the axioms of plus. We shall show that if is strongly complete for a class of Kripke models, then is strongly complete for the class of Kripke models that are ultimately in.

The Craig interpolation theorem is shown for an extended LJ with strong negation. A new simple proof of this theorem is obtained. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

Strong negation is a well-known alternative to the standard negation in intuitionistic logic. It is defined virtually by giving falsity conditions to each of the connectives. Among these, the falsity condition for implication appears to unnecessarily deviate from the standard negation. In this paper, we introduce a slight modification to strong negation, and observe its comparative advantages over the original notion. In addition, we consider the paraconsistent variants of our modification, and study their (...) relationship with non-constructive principles and connexivity. (shrink)

A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a (...) variety of proposed sequent calculi including CLS (a conservative extension of CL) and CLScw (a conservative extension of some bilattice logics, LK and S4). Completeness theorems are given for these calculi with respect to phase semantics, for SLK (a conservative extension and fragment of LK and CLScw, respectively) with respect to a classical-like semantics, and for SS4 (a conservative extension and fragment of S4 and CLScw, respectively) with respect to a Kripke-type semantics. The proposed framework allows for an embedding of the proposed calculi into LK, S4 and CL. (shrink)

Let MK3 I and MK3 II be Kleene's strong 3-valued matrix with only one and two designated values, respectively. Next, let MK3 G be defined exactly as MK3 I, except th...

A low linear order with no computable copy constructed by C. Jockusch and R. Soare has Hausdorff rank equal to $2$. In this regard, the question arises, how simple can be a low linear order with no computable copy from the point of view of the linear order type? The main result of this work is an example of a low strong $\eta $ -representation with no computable copy that is the simplest possible (...) example. (shrink)

Various four- and three-valued modal propositional logics are studied. The basic systems are modal extensions BK and BS4 of Belnap and Dunn's four-valued logic of firstdegree entailment. Three-valued extensions of BK and BS4 are considered as well. These logics are introduced semantically by means of relational models with two distinct evaluation relations, one for verification and the other for falsification. Axiom systems are defined and shown to be sound and complete with respect to the relational semantics and (...) with respect to twist structures over modal algebras. Sound and complete tableau calculi are presented as well. Moreover, a number of constructive non-modal logics with strong negation are faithfully embedded into BS4, into its three-valued extension B3S4, or into temporal BS4, BtS4. These logics include David Nelson's three-valued logic N3, the four-valued logic N4 bottom, the connexive logic C, and several extensions of bi-intuitionistic logic by strong negation. (shrink)

We study the sequent system mentioned in the author's work as CyInFL with ‘intuitionistic’ sequents. We explore the connection between this system and symmetric constructive logic of Zaslavsky and develop an algebraic semantics for both of them. In contrast to the previous work, we prove the strong completeness theorem for CyInFL with ‘intuitionistic’ sequents and all of its basic variants, including variants with contraction. We also show how the defined classes of structures are related to (...) cyclic involutive FL‐algebras and Nelson FLew‐algebras. In particular, we prove the definitional equivalence of symmetric constructive FLewc‐algebras (algebraic models of symmetric constructive logic) and Nelson FLew‐algebras (algebras introduced by Spinks and Veroff, as the termwise equivalent definition of Nelson algebras). Because of the strong completeness theorem that covers all basic variants of CyInFL with ‘intuitionistic’ sequents, we rename this sequent system to symmetric constructive full Lambek calculus (). We verify the decidability of this system and its basic variants, as we did in the case of their distributive cousins. As a consequence we obtain that the corresponding theories of (distributive and nondistributive) symmetric constructive FL‐algebras are decidable. (shrink)

ABSTRACT A new algebraic construction -called rotation- is introduced in this paper which from any left-continuous triangular norm which has no zero divisors produces a left-continuous but not continuous triangular norm with strong induced negation. An infinite number of new families of such triangular norms can be constructed in this way which provides a huge spectrum of choice for e.g. logical and set theoretical connectives in non-classical logic and in fuzzy theory. On the other hand, the (...) introduced construction brings us closer to the understanding the structure of these connectives and the corresponding logics. From the application point of view, results of this paper can be especially useful in the field of non-classical logic, fuzzy sets, and fuzzy preference modeling. (shrink)

This paper is the continuation of [11] where the rotation construction of left-continuous triangular norms was presented. Here the class of triangular subnorms and a second construction, called rotation-annihilation, are introduced: Let T1 be a left-continuous triangular norm. If T1 has no zero divisors then let T2 be a left-continuous rotation invariant t-subnorm. If T1 has zero divisors then let T2 be a left-continuous rotation invariant triangular norm. From each such pair the rotation-annihilation construction produces a left-continuous triangular norm (...) class='Hi'>with strong induced negation. An infinite number of new families of such triangular norms can be constructed in this way, and this further extends our spectrum of choice for the proper triangular norm e.g. in probabilistic metric spaces, or for logical and set theoretical connectives in non-classical logic, or e.g. in fuzzy sets theory and its applications. On the other hand, the introduced construction brings us closer to the understanding of the structure of these operations. (shrink)

We present a Kripke model for Girard's Linear Logic (without exponentials) in a conservative fashion where the logical functors beyond the basic lattice operations may be added one by one without recourse to such things as negation. You can either have some logical functors or not as you choose. Commutatively and associatively are isolated in such a way that the base Kripke model is a model for noncommutative, nonassociative Linear Logic. We also extend the (...) class='Hi'>logic by adding a coimplication operator, similar to Curry's subtraction operator, which is resituated with Linear Logic's contensor product. And we can add contraction to get nondistributive Relevance Logic. The model rests heavily on Urquhart's representation of nondistributive lattices and also on Dunn's Gaggle Theory. Indeed, the paper may be viewed as an investigation into nondistributive Gaggle Theory restricted to binary operations. The valuations on the Kripke model are three valued: true, false, and indifferent. The lattice representation theorem of Urquhart has the nice feature of yielding Priestley's representation theorem for distributive lattices if the original lattice happens to be distributive. Hence the representation is consistent with Stone's representation of distributive and Boolean lattices, and our semantics is consistent with the Lemmon-Scott representation of modal algebras and the Routley-Meyer semantics for Relevance Logic. (shrink)

The main concern of this paper is the design of a noetherian and confluent normalization for LK 2. 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, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic ; it is painless: since we reduce strong normalization and confluence to the same properties for (...) linear logic using appropriate embeddings ; 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 brings to the fore the latter's defects for these `deconstructive purposes'. (shrink)

The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.This paper introduces a typed functional language Λ! and a categorical (...) model for it.The terms of Λ! encode a version of natural deduction for Intuitionistic Linear Logic such that linear and non linear assumptions are managed multiplicatively and additively, respectively. Correspondingly, the terms of Λ! are built out of two disjoint sets of variables. Moreover, the λ-abstractions of Λ! bind variables and patterns. The use of two different kinds of variables and the patterns allow a very compact definition of the one-step operational semantics of Λ!, unlike all other extensions of Curry-Howard Isomorphism to Intuitionistic Linear Logic. The language Λ! is Church-Rosser and enjoys both Strong Normalizability and Subject Reduction.The categorical model induces operational equivalences like, for example, a set of extensional equivalences.The paper presents also an untyped version of Λ! and a type assignment for it, using formulas of Linear Logic as types. The type assignment inherits from Λ! all the good computational properties and enjoys also the Principal-Type Property. (shrink)

The paper deals with two versions of the fragment with unit, tensor, linear implication and storage operator of intuitionistic linear logic. The first version, ILL, appears in a paper by Benton, Bierman, Hyland and de Paiva; the second one, ILL+, is described in this paper. ILL has a contraction rule and an introduction rule !I for the exponential; in ILL+, instead of a contraction rule, multiple occurrences of labels for assumptions are permitted under certain conditions; (...) moreover, there is a different introduction rule for the exponential, !I+, which is closer in spirit to the necessitation rule for the normalizable version of S4 discussed by Prawitz in his monograph “Natural Deduction”.It is relatively easy to adapt Prawitz's treatment of natural deduction for intuitionistic logic to ILL+; in particular one can formulate a notion of strong validity permitting a proof of strong normalization.The conversion rules for ILL explicitly mentioned in the paper by Benton et al. do not suffice for normal forms with subformula property, but we can show that this can be remedied by addition of a special permutation conversion plus some “satellite” permutation conversions.Some discussion of the categorical models which might correspond to ILL+ is given. (shrink)

Linear Logic is a versatile framework with diverse applications in computer science and mathematics. One intriguing fragment of Linear Logic is Multiplicative-Additive Linear Logic (MALL), which forms the exponential-free component of the larger framework. Modifying MALL, researchers have explored weaker logics such as Noncommutative MALL (Bilinear Logic, BL) and Cyclic MALL (CyMALL) to investigate variations in commutativity. In this paper, we focus on Cyclic Nonassociative Bilinear Logic (CyNBL), a variant that combines (...) noncommutativity and nonassociativity. We introduce a sequent system for CyNBL, which includes an auxiliary system for incorporating nonlogical axioms. Notably, we establish the cut elimination property for CyNBL. Moreover, we establish the strong conservativeness of CyNBL over Full Nonassociative Lambek Calculus (FNL) without additive constants. The paper highlights that all proofs are constructed using syntactic methods, ensuring their constructive nature. We provide insights into constructing cut-free proofs and establishing a logical relationship between CyNBL and FNL. (shrink)

We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and (...) the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass, et al. (shrink)

The starting point of the present study is the interpretation of intuitionistic linear logic in Petri nets proposed by U. Engberg and G. Winskel. We show that several categories of order algebras provide equivalent interpretations of this logic, and identify the category of the so called strongly coherent quantales arising in these interpretations. The equivalence of the interpretations is intimately related to the categorical facts that the aforementioned categories are connected with each other via adjunctions, and (...) the compositions of the connecting functors with co-domain the category of strongly coherent quantales are dense. In particular, each quantale canonically induces a Petri net, and this association gives rise to an adjunction between the category of quantales and a category whose objects are all Petri nets. (shrink)

This 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]. (shrink)