Search

We present a logic of evidence that reduces agents' epistemic idealisations by combining classical propositional logic with substructural modal logic for formulas in the scope of epistemic modalities. To this aim, we provide a neighborhood semantics of evidence, which provides a modal extension of Fine's semantics for relevant propositional logic. Possible worlds semantics for classical propositional logic is then obtained by defining the set of possible worlds as a special subset of information states in Fine's semantics. Finally, we prove that evidence is a hyperintensional and non-prime notion in our logic, and provide a sound and complete axiomatisation of our evidence logic. [ABSTRACT FROM AUTHOR]

A representation theorem is proved for De Morgan monoids that are (i) semilinear, i.e., subdirect products of totally ordered algebras, and (ii) negatively generated, i.e., generated by lower bounds of the neutral element. Using this theorem, we prove that the De Morgan monoids satisfying (i) and (ii) form a variety—in fact, a locally finite variety. We then prove that epimorphisms are surjective in every variety of negatively generated semilinear De Morgan monoids. In the process, epimorphism-surjectivity is established for several other classes as well, including the variety of all semilinear idempotent commutative residuated lattices and all varieties of negatively generated semilinear Dunn monoids. The results settle natural questions about Beth-style definability for a range of substructural logics. [ABSTRACT FROM AUTHOR]

Some think that logic concerns the "laws of truth"; others that logic concerns the "laws of thought." This paper presents a way to reconcile both views by building a bridge between truth-maker theory, à la Fine, and normative bilateralism, à la Restall and Ripley. The paper suggests a novel way of understanding consequence in truth-maker theory and shows that this allows us to identify a common structure shared by truth-maker theory and normative bilateralism. We can thus transfer ideas from normative bilateralism to truth-maker theory, such as non-transitive solutions to paradox, and vice versa, such as notions of factual equivalence and containment. [ABSTRACT FROM AUTHOR]

In a recent paper, Barrio, Pailos and Szmuc (BPS) show that there are logics that have exactly the validities of classical logic up to arbitrarily high levels of inference. They suggest that a logic therefore must be identified by its valid inferences at every inferential level. However, Scambler shows that there are logics with all the validities of classical logic at every inferential level, but with no antivalidities at any inferential level. Scambler concludes that in order to identify a logic, we at least need to look at the validities and the antivalidities of every inferential level. In this paper, I argue that this is still not enough to identify a logic. I apply BPS's techniques in a super/sub-valuationist setting to construct a logic that has exactly the validities and antivalidities of classical logic at every inferential level. I argue that the resulting logic is nevertheless distinct from classical logic. [ABSTRACT FROM AUTHOR]

The paper presents a truth-maker semantics for Strict/Tolerant Logic (ST), which is the currently most popular logic among advocates of the non-transitive approach to paradoxes. Besides being interesting in itself, the truth-maker presentation of ST offers a new perspective on the recently discovered hierarchy of meta-inferences that, according to some, generalizes the idea behind ST. While fascinating from a mathematical perspective, there is no agreement on the philosophical significance of this hierarchy. I aim to show that there is no clear philosophical significance of meta-inferences above the first level. [ABSTRACT FROM AUTHOR]

This paper is a step toward showing what is achievable using non-classical metatheory—particularly, a substructural paraconsistent framework. What standard results, or analogues thereof, from the classical metatheory of first order logic(s) can be obtained? We reconstruct some of the originals proofs for Completeness, Löwenheim-Skolem and Compactness theorems in the context of a substructural logic with the naive comprehension schema. The main result is that paraconsistent metatheory can 're-capture' versions of standard theorems, given suitable restrictions and background assumptions; but the shift to non-classical logic may recast the meanings of these apparently 'absolute' theorems. [ABSTRACT FROM AUTHOR]

The Mares-Goldblatt semantics for quantified relevant logics have been developed for first-order extensions of R, and a range of other relevant logics and modal extensions thereof. All such work has taken place in the the ternary relation semantic framework, most famously developed by Sylvan (née Routley) and Meyer. In this paper, the Mares-Goldblatt technique for the interpretation of quantifiers is adapted to the more general neighbourhood semantic framework, developed by Sylvan, Meyer, and, more recently, Goble. This more algebraic semantics allows one to characterise a still wider range of logics, and provides the grist for some new results. To showcase this, we show, using some non-augmented models, that some quantified relevant logics are not conservatively extended by connectives the addition of which do conservatively extend the associated propositional logics, namely fusion and the dual implication. We close by proposing some further uses to which the neighbourhood Mares-Goldblatt semantics may be put. [ABSTRACT FROM AUTHOR]

Priest argued in Fusion and Confusion (Priest in Topoi 34(1):55–61, 2015a) for a new concept of logical consequence over the relevant logic B, one where premises my be "confused" together. This paper develops Priest's idea. Whereas Priest uses a substructural proof calculus, this paper provides a Hilbert proof calculus for it. Using this it is shown that Priest's consequence relation is weaker than the standard Hilbert consequence relation for B, but strictly stronger than Anderson and Belnap's original relevant notion of consequence. Unlike the latter, however, Priest's consequence relation does not satisfy a variant of the variable sharing property. This paper shows that how it can be modified so as to do so. Priest's consequence relation turns out to be surprisingly weak in some respects. The prospects of strengthening it is raised and discussed in a broader philosophical context. [ABSTRACT FROM AUTHOR]

The Lambek calculus with the unit can be defined as the atomic theory (algebraic logic) of the class of residuated monoids. This calculus, being a theory of a broader class of algebras than Heyting ones, is weaker than intuitionistic logic. Namely, it lacks structural rules: permutation, contraction, and weakening. We consider two extensions of the Lambek calculus with modalities—the exponential, under which all structural rules are permitted, and the relevant modality, under which only permutation and contraction rules are allowed. The Lambek calculus with a relevant modality is used in mathematical linguistics. Both calculi are algorithmically undecidable. We consider their fragments in which the modality is allowed to be applied to just formulas of Horn depth not greater than 1. We prove that these fragments are decidable and belong to the NP class. To show this, in the case of a relevant modality, we introduce a new notion of ℛ-total derivability in context-free grammars, i.e., existence of a derivation in which each rule is used at least a given number of times. It is stated that the ℛ-totality problem is NP-hard for context-free grammars. Also we pinpoint algorithmic complexity of ℛ-total derivability for more general classes of generative grammars. [ABSTRACT FROM AUTHOR]

In the literature on self-referential paradoxes one of the hardest and most challenging problems is that of revenge. This problem can take many shapes, but, typically, it besets non-classical accounts of some semantic notion, such as truth, that depend on a set of classically defined meta-theoretic concepts, like validity, consistency, and so on. A particularly troubling form of revenge that has received a lot of attention lately involves the concept of validity. The difficulty lies in that the non-classical logician cannot accept her own definition of validity because it is given in a classical meta-theory. It is often suggested that this mismatch between the consequence relation of the account being espoused and the consequence relation of the meta-theory is a serious embarrassment. The main goal of the paper is to explore whether certain substructural accounts of the paradoxes can avoid this sort of embarrassment. Typically, these accounts are expressively incomplete, since they cannot assert in the object language that certain invalid arguments are in fact invalid. To overcome this difficulty I develop a novel type of hybrid proof-procedure, one that takes invalidities to be just as fundamental as validities. I prove that this proof-procedure enjoys a number of interesting properties and I analyze the prospects of applying it to languages capable of expressing self-referential statements. [ABSTRACT FROM AUTHOR]

Given a consequence relation in many-valued logic, what connectives can be defined? For instance, does there always exist a conditional operator internalizing the consequence relation, and which form should it take? In this paper, we pose this question in a multi-premise multi-conclusion setting for the class of so-called intersective mixed consequence relations, which extends the class of Tarskian relations. Using computer-aided methods, we answer extensively for 3-valued and 4-valued logics, focusing not only on conditional operators, but also on what we call Gentzen-regular connectives (including negation, conjunction, and disjunction). For arbitrary N-valued logics, we state necessary and sufficient conditions for the existence of such connectives in a multi-premise multi-conclusion setting. The results show that mixed consequence relations admit all classical connectives, and among them pure consequence relations are those that admit no other Gentzen-regular connectives. Conditionals can also be found for a broader class of intersective mixed consequence relations, but with the exclusion of order-theoretic consequence relations. [ABSTRACT FROM AUTHOR]

A commutative residuated lattice A is said to be subidempotent if the lower bounds of its neutral element e are idempotent (in which case they naturally constitute a Brouwerian algebra A - ). It is proved here that epimorphisms are surjective in a variety K of such algebras A (with or without involution), provided that each finitely subdirectly irreducible algebra B ∈ K has two properties: (1) B is generated by lower bounds of e, and (2) the poset of prime filters of B - has finite depth. Neither (1) nor (2) may be dropped. The proof adapts to the presence of bounds. The result generalizes some recent findings of G. Bezhanishvili and the first two authors concerning epimorphisms in varieties of Brouwerian algebras, Heyting algebras and Sugihara monoids, but its scope also encompasses a range of interesting varieties of De Morgan monoids. [ABSTRACT FROM AUTHOR]

Generalized bunched implication algebras (GBI-algebras) are defined as residuated lattices with a Heyting implication, and are positioned between Boolean algebras with operators and lattices with operators. We characterize congruences on GBI-algebras by filters that are closed under Gumm–Ursini terms, and for involutive GBI-algebras these terms simplify to a dual version of the congruence term for relation algebras together with two more terms. We prove that representable weakening relation algebras form a variety of cyclic involutive GBI-algebras, denoted by RWkRA, containing the variety of representable relation algebras. We describe a double-division conucleus construction on residuated lattices and on (cyclic involutive) GBI-algebras and show that it generalizes Comer's double coset construction for relation algebras. Also, we explore how the double-division conucleus construction interacts with other class operators and in particular with variety generation. We focus on the fact that it preserves a special discriminator term, thus yielding interesting discriminator varieties of GBI-algebras, including RWkRA. To illustrate the generality of the variety of weakening relation algebras, we prove that all distributive lattice-ordered pregroups and hence all lattice-ordered groups embed, as residuated lattices, into representable weakening relation algebras on chains. Moreover, every representable weakening relation algebra is embedded in the algebra of all residuated maps on a doubly-algebraic distributive lattice. We give a number of other instructive examples that show how the double-division conucleus illuminates the structure of distributive involutive residuated lattices and GBI-algebras. [ABSTRACT FROM AUTHOR]

Lambek elegantly characterized part of natural language. As is well-known, his substructural logic L, and its non-associative version NL, handle basic function/argument composition well, but not scope taking and syntactic displacement—at least, not in their full generality. In previous work, I propose NL λ , which is NL supplemented with a single structural inference rule ("abstraction"). Abstraction closely resembles the traditional linguistic rule of quantifier raising, and characterizes both semantic scope taking and syntactic displacement. Due to the unconventional form of the abstraction inference, there has been some doubt that NL λ should count at a legitimate substructural logic. This paper argues that NL λ is perfectly well-behaved. In particular, it enjoys cut elimination and an interpolation result. In addition, perhaps surprisingly, it is decidable. Finally, I prove that it is sound and complete with respect to the usual class of relational frames. [ABSTRACT FROM AUTHOR]

Our main goal is to investigate whether the infinitary rules for the quantifiers endorsed by Elia Zardini in a recent paper are plausible. First, we will argue that they are problematic in several ways, especially due to their infinitary features. Secondly, we will show that even if these worries are somehow dealt with, there is another serious issue with them. They produce a truth-theoretic paradox that does not involve the structural rules of contraction. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

We prove the finite embeddability property for a wide range of varieties of fully distributive residuated lattices and FL-algebras. Part of the axiomatization is assumed to be a knotted inequality and some appropriate generalization of commutativity. The construction is based on distributive residuated frames and extends to subvarieties axiomatized by any division-free equation. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

We introduce a systematic method for densification, i.e., embedding a given chain into a dense one preserving certain identities, in the framework of FL algebras (pointed residuated lattices). Our method, based on residuated frames, offers a uniform proof for many of the known densification and standard completeness results in the literature. We propose a syntactic criterion for densification, called semianchoredness. We then prove that the semilinear varieties of integral FL algebras defined by semi-anchored equations admit densification, so that the corresponding fuzzy logics are standard complete. Our method also applies to (possibly non-integral) commutative FL chains. We prove that the semilinear varieties of commutative FL algebras defined by knotted axioms $${x^{m} \leq x^{n}}$$ (with $${m, n > 1}$$ ) admit densification. This provides a purely algebraic proof to the standard completeness of uninorm logic as well as its extensions by knotted axioms. [ABSTRACT FROM AUTHOR]

Adding a transparent truth predicate to a language completely governed by classical logic is not possible. The trouble, as is well-known, comes from paradoxes such as the Liar and Curry. Recently, Cobreros, Egré, Ripley and van Rooij have put forward an approach based on a non-transitive notion of consequence which is suitable to deal with semantic paradoxes while having a transparent truth predicate together with classical logic. Nevertheless, there are some interesting issues concerning the set of metainferences validated by this logic. In this paper, we show that this logic, once it is adequately understood, is weaker than classical logic. Moreover, the logic is in a way similar to the paraconsistent logic LP. [ABSTRACT FROM AUTHOR]

This note motivates a logic for a theory that can express its own notion of logical consequence-a 'syntactically closed' theory of naive validity. The main issue for such a logic is Curry's paradox, which is averted by the failure of contraction. The logic features two related, but different, implication connectives. A Hilbert system is proposed that is complete and non-trivial. [ABSTRACT FROM AUTHOR]

If $ {\mathbb {V}} $ is a subvariety of $ {\mathbb {BL}} $ generated by a class of standard BL-algebras, then $ {\mathbb {V}} $ is generated by a finite class of standard BL-algebras. [ABSTRACT FROM AUTHOR]

We solve several open problems on the cardinality of atoms in the subvariety lattice of residuated lattices and FL-algebras [4, Problems 17-19, pp. 437]. Namely, we prove that the subvariety lattice of residuated lattices contains continuum many 4-potent commutative representable atoms. Analogous results apply also to atoms in the subvariety lattice of FL-algebras and FL-algebras. On the other hand, we show that the subvariety lattice of residuated lattices contains only five 3-potent commutative representable atoms and two integral commutative representable atoms. Inspired by the construction of atoms, we are also able to prove that the variety of integral commutative representable residuated lattices is generated by its 1-generated finite members. [ABSTRACT FROM AUTHOR]

Grammar can be formulated as a kind of substructural propositional logic. In support of this claim, we survey bare Gentzen style deductive systems and two kinds of non-commutative linear logic: intuitionistic and compact bilinear logic. We also glance at their categorical refinements. [ABSTRACT FROM AUTHOR]

The Lambek-Grishin calculus is a symmetric version of categorial grammar obtained by augmenting the standard inventory of type-forming operations (product and residual left and right division) with a dual family: coproduct, left and right difference. Interaction between these two families is provided by distributivity laws. These distributivity laws have pleasant invariance properties: stability of interpretations for the Curry-Howard derivational semantics, and structure-preservation at the syntactic end. The move to symmetry thus offers novel ways of reconciling the demands of natural language form and meaning. [ABSTRACT FROM AUTHOR]

In this paper I present a range of substructural logics for a conditional connective ↦. This connective was original introduced semantically via restriction on the ternary accessibility relation R for a relevant conditional. I give sound and complete proof systems for a number of variations of this semantic definition. The completeness result in this paper proceeds by step-by-step improvements of models, rather than by the one-step canonical model method. This gradual technique allows for the additional control, lacking in the canonical model method, that is required. [ABSTRACT FROM AUTHOR]

Categorial grammar predated Syntactic Structures by two decades. While dramatic linguistic revolutions occupied centre stage, it tended to be the preserve of formal philosophy and philosophical linguistics: the philosophers’ grammar. Fashions change but style endures. The 1980s saw the rediscovery of the categorial calculus of Lambek (1958) and the advent of linear logic and substructural logic generally providing a context for categorial grammar so-construed, since named type logical grammar (TLG). I think the history of the genesis and evolution of type-logical ideas is not widely known, but that the interpretation of the past is important to give direction to the future. This is the story of how a field came to a new pass. [ABSTRACT FROM AUTHOR]

Substructural logics have received a lot of attention in recent years from the communities of both logic and algebra. We discuss the algebraization of substructural logics over the full Lambek calculus and their connections to residuated lattices, and establish a weak form of the deduction theorem that is known as parametrized local deduction theorem. Finally, we study certain interpolation properties and explain how they imply the amalgamation property for certain varieties of residuated lattices. [ABSTRACT FROM AUTHOR]

This paper presents a neighborhood semantics for logics of entailment. It begins with a minimal system Min that expresses the most fundamental assumptions about the entailment relation, and continues by examining various extensions that reflect further assumptions that might be made about entailment. This leads first to the logic B that is the basic relevant logic, and then to more powerful systems. All of these logics are proved to be sound and strongly complete. With B the neighborhood semantics meets the Routley–Meyer relational semantics for relevant logic; these connections are examined. The minimal and basic entailment logics are shown to have the finite model property, and hence to be decidable. [ABSTRACT FROM AUTHOR]

In Moortgat (1996) the Lambek Calculus L(Lambek, 1958) is extended by a pair of residuation modalities ♦ and □↓. Categorial Grammars based on the resulting logic L♦ are attractive for the purpose of modelling linguistic phenomena since they offer a compromise between the strict constituent structures imposed by context free grammars and related formalisms on the one hand, and the complete absence of hierarchical information in Lambek grammars on the other hand. The paper contains some results on the generative capacity of Categorial Grammars based on L♦. First it is shownthat adding residuation modalities does not extend the weak generative capacity. This is proved by extending the proof for the context freeness of L-grammars from Pentus (1993) to L♦. Second, the strong generative capacity of L♦-grammars is compared to context free grammars. The results are mainly negative; the set of tree languages generated by L♦-grammars neither contains nor is contained in the class of context free tree languages. [ABSTRACT FROM AUTHOR]

This paper reports results and some new problems in one of the domains to which automatic first-order theorem provers have been most successfully applied: axiomatics of nonclassical propositional logics. It is well known that one of the standard axioms of the denumerable-valued pure implication logic of Łukasiewicz becomes derivable from the remainder in the presence of negation. Here it is shown that the same axiom is similarly derivable using conjunction and disjunction instead of negation. This closes a problem left open by Harris and Fitelson ( Journal of Automated Reasoning 27, 2001). Related problems are discussed, and five such open problems are proposed as challenges to the automated reasoning community. [ABSTRACT FROM AUTHOR]

Routley-Meyer type relational complete semantics are constructed for intuitionistic contractionless logic with reductio. Different negation completions of positive intuitionistic logic without contraction are treated in a systematical, unified and semantically complete setting. [ABSTRACT FROM AUTHOR]

In this paper we prove the equivalence between the Gentzen system G LJ*\ c, obtained by deleting the contraction rule from the sequent calculus LJ* (which is a redundant version of LJ), the deductive system IPC*\ c and the equational system associated with the variety RL of residuated lattices. This means that the variety RL is the equivalent algebraic semantics for both systems G LJ*\ c in the sense of [18] and [4], respectively. The equivalence between G LJ*\ c and IPC*\ c is a strengthening of a result obtained by H. Ono and Y. Komori [14, Corollary 2.8.1] and the equivalence between G LJ*\ c and the equational system associated with the variety RL of residuated lattices is a strengthening of a result obtained by P.M. Idziak [13, Theorem 1]. An axiomatization of the restriction of IPC*\ c to the formulas whose main connective is the implication connective is obtained by using an interpretation of G LJ*\ c in IPC*\ c. [ABSTRACT FROM AUTHOR]

The aim of this paper is to show that the implicational fragment BKof the intuitionistic propositional calculus (IPC) without the rules of exchange and contraction has the finite model property with respect to the quasivariety of left residuation algebras (its equivalent algebraic semantics). It follows that the variety generated by all left residuation algebras is generated by the finite left residuation algebras. We also establish that BKhas the finite model property with respect to a class of structures that constitute a Kripke-style relational semantics for it. The results settle a question of Ono and Komori [OK85]. [ABSTRACT FROM AUTHOR]

We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic logic. [ABSTRACT FROM AUTHOR]