Search

We show that all extensions of the (non-associative) Gentzen system for distributive full Lambek calculus by simple structural rules have the cut elimination property. Also, extensions by such rules that do not increase complexity have the finite model property, hence many subvarieties of the variety of distributive residuated lattices have decidable equational theories. For some other extensions, we prove the finite embeddability property, which implies the decidability of the universal theory, and we show that our results also apply to generalized bunched implication algebras. Our analysis is conducted in the general setting of residuated frames.

This paper extends the theory of situated inference from Mares (Relevant logic: a philosophical interpretation. Cambridge University Press, Cambrdge, 2004) to treat two weak relevant logics, B and DJ. These logics are interesting because they can be used as bases for consistent naive theories, such as naive set theory. The concepts of a situation and of information that are employed by the theory of situated inference are used to justify various aspects of these logics and to give an interpretation of the notion of set that is represented in the naive set theories that are based on them.

ince the pioneering work of Birkhoff and von Neumann, quantum logic has been interpreted as the logic of (closed) subspaces of a Hilbert space. There is a progression from the usual Boolean logic of subsets to the "quantum logic" of subspaces of a general vector space--which is then specialized to the closed subspaces of a Hilbert space. But there is a "dual" progression. The set notion of a partition (or quotient set or equivalence relation) is dual (in a category-theoretic sense) to the notion of a subset. Hence the Boolean logic of subsets has a dual logic of partitions. Then the dual progression is from that logic of set partitions to the quantum logic of direct-sum decompositions (i.e., the vector space version of a set partition) of a general vector space--which can then be specialized to the direct-sum decompositions of a Hilbert space. This allows the quantum logic of direct-sum decompositions to express measurement by any self-adjoint operators. The quantum logic of direct-sum decompositions is dual to the usual quantum logic of subspaces in the same sense that the logic of partitions is dual to the usual Boolean logic of subsets.

This paper deals with the standard completeness of involutive non-associative, non-commutative, substructural fuzzy logics and their axiomatic extensions. First, fuzzy systems based on involutively residuated mianorms (binary monotonic identity aggregation operations on the real unit interval [ 0 , 1 ] ), their corresponding algebraic structures, and their algebraic completeness results are discussed. Next, completeness with respect to algebras whose lattice reduct is [ 0 , 1 ] , known as standard completeness, is established for these systems via a construction in the style of Jenei–Montagna. These standard completeness results resolve a problem left open by Cintula, Horcik, and Noguera in the recent Handbook of Mathematical Fuzzy Logic and Review of Symbolic Logic. Finally, we briefly consider the similarities and differences between constructions of the author and Wang's Jenei–Montagna-style.

The Belnap–Dunn logic (also known as First Degree Entailment, or FDE) is a well-known and well-studied four-valued logic, but until recently little has been known about its extensions, i.e. stronger logics in the same language, called super-Belnap logics here. We give an overview of several results on these logics which have been proved in recent works by Přenosil and Rivieccio. We present Hilbert-style axiomatizations, describe reduced matrix models, and give a description of the lattice of super-Belnap logics and its connections with graph theory. We adopt the point of view of Abstract Algebraic Logic, exploring applications of the general theory of algebraization of logics to the super-Belnap family. In this respect we establish a number of new results, including a description of the algebraic counterparts, Leibniz filters, and strong versions of super-Belnap logics, as well as the classification of these logics within the Leibniz and Frege hierarchies.

Graph normal form, GNF, [1], was used in [2, 3] for analyzing paradoxes in propositional discourses, with the semantics—equivalent to the classical one—defined by kernels of digraphs. The paper presents infinitary, resolution-based reasoning with GNF theories, which is refutationally complete for the classical semantics. Used for direct (not refutational) deduction it is not explosive and allows to identify in an inconsistent discourse, a maximal consistent subdiscourse with its classical consequences. Semikernels, generalizing kernels, provide the semantic interpretation.

When studying sequent calculi, proof theorists often have to prove properties about the systems, whether it is to show that they are “well-behaved”, amenable to automated proof search, complete with respect to another system, consistent, among other reasons. These proofs usually involve many very similar cases, which leads to authors rarely writing them in full detail, only pointing to one or two more complicated cases. Moreover, the amount of details makes them more error-prone for humans. Computers, on the other hand, are very good at handling details and repetitiveness. In this work we have formalized textbook proofs of the meta-theory of sequent calculi for linear logic in Abella. Using the infrastructure developed, the proofs can be easily adapted to other substructural logics. We implemented rules as clauses in an intuitive and straightforward way, similar to logic programming, using operations on multisets for the explicit contexts. Although the proofs are quite big, their writing took no more than a few weeks once the correct definitions were found. This is an evidence that machine-checked proofs of properties of sequent calculi can be obtained using a natural encoding on most proof assistants available nowadays.

We give a simple sequent calculus presentation of R.B. Angell’s logic of analytic containment, recently championed by Kit Fine as a plausible logic of partial content.

This paper explores a notion of “the strong version” of a sentential logic S, initially defined in terms of the notion of a Leibniz filter, and shown to coincide with the logic determined by the matrices of S whose filter is the least S-filter in the algebra of the matrix. The paper makes a general study of this notion, which appears to unify under an abstract framework the relationships between many pairs of logics in the literature. The paradigmatic examples are the local and the global consequences associated with a normal modal logic, and the logics preserving degrees of truth and preserving truth associated with certain substructural and many-valued logics. For protoalgebraic logics the results in the paper coincide with those obtained by two of the authors in 2001, so the main novelty of the approach is its suitability for all kinds of logics. The paper also studies three kinds of definability of the Leibniz filters, and their consequences for the determination of the strong version. In a second part of the paper several case studies are developed, comprising positive modal logic, Dunn–Belnap’s four-valued logic, the large family of substructural logics, and some relevance logics.

Paraconsistent quantum logic, a hybrid of minimal quantum logic and paraconsistent four-valued logic, is introduced as Gentzen-type sequent calculi, and the cut-elimination theorems for these calculi are proved. This logic is shown to be decidable through the use of these calculi. A first-order extension of this logic is also shown to be decidable. The relationship between minimal quantum logic and paraconsistent four-valued logic is clarified, and a survey of existing Gentzen-type sequent calculi for these logics and their close relatives is addressed.

We continue our program of establishing connections between proof-theoretic and order-algebraic properties in the setting of substructural logics and residuated lattices. Extending our previous work that connects a strong form of cut-admissibility in sequent calculi with closure under MacNeille completions of corresponding varieties, we now consider hypersequent calculi and more general completions; these capture logics/varieties that were not covered by the previous approach and that are characterized by Hilbert axioms (algebraic equations) residing in the level P 3 of the substructural hierarchy. We provide algebraic foundations for substructural hypersequent calculi and an algorithm to transform P 3 axioms/equations into equivalent structural hypersequent rules. Using residuated hyperframes we link strong analyticity in the resulting calculi with a new algebraic completion, which we call hyper-MacNeille.

We introduce a substructural modal logic of utility that can be used to reason aboutoptimality with respect to properties of states. Our notion of state is quite general, and is able to represent resource allocation problems in distributed systems. The underlying logic is a variant of the modal logic of bunched implications, and based on resource semantics, which is closely related to concurrent separation logic. We consider a labelled transition semantics and establish conditions under which Hennessy—Milner soundness and completeness hold. By considering notions of cost, strategy and utility, we are able to formulate characterizations of Pareto optimality, best responses, and Nash equilibrium within resource semantics. We also show that our logic is able to serve as a logic for a fully featured process algebra and explain the interaction between utility and the structure of processes.

Tensorial logic is a primitive logic of tensor and negation which refines linear logic by relaxing the hypothesis that linear negation is involutive. Thanks to this mild modification, tensorial logic provides a type-theoretic account of game semantics where innocent strategies are portrayed as temporal refinements of traditional proof-nets in linear logic. In this paper, we study the algebraic and combinatorial structure of negation in a non-commutative variant of tensorial logic. The analysis is based on a 2-categorical account of dialogue categories, which unifies tensorial logic with linear logic, and discloses a primitive symmetry between proofs and anti-proofs. The micrological analysis of tensorial negation reveals that it can be decomposed into a series of more elementary components: an adjunction L ⊣ R between the left and right negation functors L and R; a pair of linear distributivity laws κ and κ which refines the linear distributivity law between ⊗ and ⅋ in linear logic, and generates the Opponent and Proponent views of innocent strategies between dialogue games; a pair of axiom and cut combinators adapted from linear logic; an involutive change of frame ( − ) ⁎ reversing the point of view of Prover and of Denier on the logical dispute, and reversing the polarity of moves in the dialogue game associated to the tensorial formula.

We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of architectures as generic coordination schemes involving a configuration of interactions between typed components; and 2) configuration logics for the specification of architecture styles as sets of interaction configurations. The presented results build on previous work on architecture modeling in BIP. We show how propositional interaction logic can be extended into a corresponding configuration logic by adding new operators on sets of interaction configurations. In addition to the usual set-theoretic operators, configuration logic is equipped with a coalescing operator + to express combination of configuration sets. We provide a complete axiomatization of propositional configuration logic as well as decision procedures for checking that an architecture satisfies given logical specifications. To allow genericity of specifications, we study first-order and second-order extensions of the propositional configuration logic. First-order logic formulas involve quantification over component variables. Second-order logic formulas involve additional quantification over sets of components. We provide several examples illustrating the application of the results to the characterization of various architecture styles. We also provide an experimental evaluation using the Maude rewriting system to implement the decision procedure for the propositional flavor of the logic.

In this paper we introduce arbitrary arrow update logic (AAUL). The logic AAUL takes arrow update logic, a dynamic epistemic logic where the accessibility relations of agents are updated rather than the set of possible worlds, and adds a quantifier over such arrow updates.We investigate the relative expressivity of AAUL compared to other logics, most notably arbitrary public announcement logic (APAL). Additionally, we show that the model checking problem for AAUL is PSPACE-complete. Finally, we introduce a proof system for AAUL, and prove it to be sound and complete. (C) 2016 Elsevier B.V. All rights reserved.

One of the most fruitful applications of substructural logics stems from their capacity to deal with self-referential paradoxes, especially truth-theoretic paradoxes. Both the structural rules of contraction and the rule of cut play a crucial role in typical paradoxical arguments. In this paper I address a number of difficulties affecting noncontractive approaches to paradox that have been discussed in the recent literature. The situation was roughly this: if you decide to go substructural, the nontransitive approach to truth offers a lot of benefits that are not available in the noncontractive account. I sketch a noncontractive theory of truth that has these benefits. In particular, it has both a proof- and a model-theoretic presentation, it can be extended to a first-order language, and it retains every classically valid inference.

The paper investigates fuzzy tolerance relations with membership function valued in a noncommutative residuated lattice. Such tolerance relations appear in the context of the theory of formal concepts. The paper shows that given a fuzzy tolerance relation, it is possible to identify a system of attributes and an object-to-attribute relationship, so that the objects are similar to the extent they have common attributes. For this purpose the tolerance classes can be taken as attributes. The paper presents the general description of the structure of fuzzy tolerance classes.

Our method for density elimination is generalized to the non-commutative substructural logic GpsUL * . Then, the standard completeness of HpsUL * follows as a lemma by virtue of previous work by Metcalfe and Montagna. This result shows that HpsUL * is the logic of pseudo-uninorms and their residua and answered the question posed by Prof. Metcalfe, Olivetti, Gabbay and Tsinakis.

A logic for inconsistent mathematics must be strong enough to support reasoning in proofs, while weak enough to avoid paradoxes. We present a substructural logic intended to meet the needs of a working dialetheic mathematician—specifically, by adding a de Morgan negation to light linear logic, and extending the logic with a relevant conditional. The logic satisfies a deduction theorem. Soundness and completeness is established, showing in particular that contraction is invalidated. This opens the way for a robust naive set theory; we conclude by showing how the set theory provides a foundation for induction.

We prove completeness and decidability of a version of Propositional Dynamic Logic where the underlying non-modal propositional logic is a substructural logic in the vicinity of the Full Distributive Non-associative Lambek Calculus. Extensions of the result to stronger substructural logics are briefly discussed.

We prove that the problem of tabularity over Johansson’s minimal logic J is decidable. Describing all pretabular extensions of the minimal logic, we find that there are seven of them and show that they are all recognizable over J. We find axiomatizations and semantic characterizations of all seven pretabular logics.

Closure is the idea that what is true about a theory of truth should be true (and therefore expressible) in it. Commitment to closure under truth motivates non-classical logic; commitment to closure under validity leads to substructural logic (nontransitive or noncontractive). These moves can be thought of as responses to revenge problems. With a focus on truth in mathematics, I will consider whether a noncontractive approach faces a similar revenge problem with respect to closure under provability, and argue that if a noncontractive theory is to be genuinely closed, then it must be free of all contraction, even in the metatheory.

This paper addresses standard completeness for non-associative, non-commutative, substructural fuzzy logics and their axiomatic extensions. First, fuzzy systems, which are based on mianorms (binary monotonic identity aggregation operations on the real unit interval [ 0 , 1 ] ), their corresponding algebraic structures, and algebraic completeness results are discussed. Next, completeness with respect to algebras whose lattice reduct is [ 0 , 1 ] , so-called standard completeness, is established for these systems using construction in the style of Jenei–Montagna. Finally, some axiomatic extensions of the non-associative, non-commutative core fuzzy logics having axioms corresponding to the structural rule(s) of exchange and/or associativity are considered.

MTL is a Monoidal t-norm based logic introduced by Esteva and Godo by omitting divisibility axiom from H´ajek's Basic logic (BL). Many logics can be obtained by adding axioms to MTL logic. Logic system WBL is obtained by adding weak divisibility axiom to logic system MTL. Logic system WMV is obtained by adding involution axiom to logic system WBL. WBL-algebra corresponding to logic system WBL and WMV-algebra to logic system WMV are defined respectively. It is proved that the both of logic system Luk and logic system Nilpotent minimum (NM) are the schematic extensions of logic system WMV. Weak Wajsberg algebra and the simplified form of logic system WMV are obtained.

We set out the implication fragment of Frege’s Grundgesetze, clarifying the implication rules and showing that this system extends Absolute Implication, or the implication fragment of Intuitionist logic. We set out a sequent calculus which naturally captures Frege’s implication proofs, and draw particular attention to the Cut-like features of his Hypothetical Syllogism rule.

In [25] Priest developed the da Costa logic (daC); this is a paraconsistent logic which is also a co-intuitionistic logic that contains the logic C ω . Due to its interesting properties it has been studied by Castiglioni, Ertola and Ferguson, and some remarkable results about it and its extensions are shown in [8] , [11] . In the present article we continue the study of daC, we prove that a restricted Hilbert system for daC, named DC, satisfies certain properties that help us show that this logic is not a maximal paraconsistent system. We also study an extension of daC called P H 1 and we give different characterizations of it. Finally we compare daC and P H 1 with several paraconsistent logics.

A star-free relational semantics for relevant logic is presented together with a sound and complete sequent proof theory (display calculus). It is an extension of the dualist approach to negation regarded as modality, according to which de Morgan negation in relevant logic is better understood as the confusion of two negative modalities. The present work shows a way to define them in terms of implication and a new connective, co-implication, which is modeled by respective ternary relations. The defined negations are confused by a special constraint on ternary relation, called the generalized star postulate, which implies definability of the Routley star in the frame. The resultant logic is shown to be equivalent to the well-known relevant logic R. Thus it can be seen as a reconstruction of R in the dualist framework.

FL ew -algebras form the algebraic semantics of the full Lambek calculus with exchange and weakening. We investigate two relations, called satisfiability and positive satisfiability, between FL ew -terms and FL ew -algebras. For each FL ew -algebra, the sets of its satisfiable and positively satisfiable terms can be viewed as fragments of its existential theory; we identify and investigate the complements as fragments of its universal theory. We offer characterizations of those algebras that (positively) satisfy just those terms that are satisfiable in the two-element Boolean algebra providing its semantics to classical propositional logic. In case of positive satisfiability, these algebras are just the nontrivial weakly contractive FL ew -algebras. In case of satisfiability, we give a characterization by means of another property of the algebra, the existence of a two-element congruence. Further, we argue that (positive) satisfiability problems in FL ew -algebras are computationally hard. Some previous results in the area of term satisfiability in MV-algebras or BL-algebras are thus brought to a common footing with known facts on satisfiability in Heyting algebras.

We 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.