Over the last few decades, considerable attention has been paid to substructural logics-that is, logical systems that forego at least one of the structural principles sanctioned by classical logic. However, little or no attention has been paid to the dual notion of a suprastructural logic, that is, a system that sanctions at least one structural principle that classical logic rejects. In the present paper, we explore this notion and present different types of systems where at least one classically invalid structural metainference holds. We introduce two families of suprastructural logics-Boolean logics and Strong-Kleene logics-as examples of different ways to achieve suprastructurality by revising the traditional conception of inferential validity. Afterwards, we present some strictly suprastructural logics. We show that $ extbf{LP}$ and $ extbf{K3}$ are strictly suprastructural from a global perspective, which also exemplifies a way to achieve suprastructurality that does not alter the usual sense of inferential validity. We then introduce metainferential logics that are strictly suprastructural from a local perspective and show that some of them are also supraclassical. This leads us to consider two different notions of suprastructurality: one that focuses on metainferences and the other that focuses on closure properties.
In [8], the authors introduced Kleene algebras with intuitionistic negation, referred to as KAN-algebras. This work arises from an interest in better understanding of the relationship between strong negation and intuitionistic negation in Nelson algebras. Nelson algebras are characterized by the presence of two types of negation: a strong negation and an intuitionistic negation. Although both are present in the structure, the intuitionistic negation is not considered a primitive operation, and thus its role remains partially hidden. In this paper, we introduce and study centered KAN-algebras with tense operators. Specifically, we prove a Glivenko-style theorem for tense pseudocomplemented distributive lattices, establish a categorical equivalence between tense centered KAN-algebras and tense distributive p$_{0}$-algebras, and extend Monteiro's construction to the tense setting, showing that the categories of tense KAN-algebras, tense centered KAN-algebras, and tense distributive p$_{0}$-algebras are related by a commutative diagram up to natural isomorphism.
In this paper, we contribute to the further development of non-deterministic semantics for propositional modality within the 8-valued framework. As our point of departure, we take MnD, a very weak modal logic where modal operators are inter-definable and uninterpreted. We study its extensions with respect to $\Box ,\Diamond ,\vee ,\wedge , ightarrow $ by means of simple refinements. We provide axiomatisations for all extensions obtained through these refinements. This systematic approach enables the exploration of a wide range of non-deterministic modal logics and hones our understanding of non-deterministic semantics for modality.
Abstract In its initial formulation, $CG_{3}^{\prime}$ is a three-valued paraconsistent calculus derived from specific modifications to the matrix of Gödel logic $G_{3}$. We show that enriching $CG_{3}^{\prime}$ with the so-called Aristotle’s theses, or their equivalent variants, leads to a trivial logic. To resolve this issue, we define certain proper subsystems of $CG_{3}^{\prime}$ in a manner that prevents trivialization. However, unlike prevailing perspectives in connexive logic, we do not assume that certain classically valid formulas must be rejected due to their counter-intuitive nature. By extending some subsystems of $CG_{3}^{\prime}$ with Aristotle’s theses, our objective is to develop calculi that validate as many $CG_{3}^{\prime}$-valid formulas as possible while remaining non-trivial.
In the literature, there are several common approaches to defining a c.e. set of constructive objects. In the first one, the non-empty set is called c.e. if it is the range of a computable function or if it is the domain of a partial computable function. In the second one, the set is called c.e. if it has a computable numbering. In this paper, we study how the approaches to defining a c.e. set of effective reals represented by constructive reals and Specker reals are related to each other.
Abstract Computational trinitarianism is the view that a single notion of computation has three different manifestations: in logic as proofs, in typed $\lambda $-calculus as programs, and in category theory as morphisms. This idea has traditionally been closely associated with intuitionistic logic but here we argue that the connection is not exclusive. We provide a logician friendly, self-contained introduction to this topic by presenting the trinities for linear, affine, and relevant logic. The ground we set for that goal is then used to show how to obtain paraconsistent trinities by including the De Morgan negation.
We extend Stone duality to domain theory, establishing a logical representation of recursive domains in denotational semantics. Specifically, we prove a dual equivalence between the category $ extbf{LAD}$ of Lawson compact algebraic $L$-domains with spectrally continuous functions and the category $ extbf{NOD}$ of NOD-lattices with NOD-lattice homomorphisms. The duality is constructed via two inverse correspondences: the compact stable open subsets of any Lawson compact algebraic $L$-domain form an NOD-lattice, and the spectrum $\operatorname{Spec}(L)$ of any NOD-lattice $L$ is a Lawson compact algebraic $L$-domain. Moreover, these correspondences are mutually inverse up to isomorphism, yielding two representation theorems: every NOD-lattice is isomorphic to the lattice of compact stable open subsets of its spectrum, and every Lawson compact algebraic $L$-domain is isomorphic to the spectrum of its lattice of compact stable open subsets. This result deepens the structural link connecting semantic domains with lattices admitting finite disjoint decomposition, thereby offering a new tool for the logical analysis of recursive computational structures.
In this study, we introduce and examine the concept of weakly r-supplemented modules and establish several fundamental properties concerning them. It is shown that if the radical of a weakly supplemented module M serves as a supplement submodule in M, then M is necessarily weakly r-supplemented. We also demonstrate that every factor module, every homomorphic image, and every r-small cover of a weakly r-supplemented module inherit the weakly r-supplemented property. Moreover, if a module M can be written as the sum M = M-1 + M-2 + ... + M-n where each Mi (i = 1, 2, ..., n) is weakly rsupplemented, then M itself enjoys the same property. Finally, it is established that whenever M is weakly r-supplemented, any finitely M-generated R-module is also weakly r-supplemented.
In this study, homotopic contraction mappings studied by Frigon in 1991 were investigated. Kannan-type homotopic contraction mappings, Chatterjea-type homotopic contraction mappings, and almost homotopic contraction mappings are defined, and some fixed point results are obtained. Furthermore, the relationship between Kannan-type and Chatterjaa-type contraction mappings and almost contraction mappings is given, and an example is presented.
We present correct and natural development of continuity theory in a predicative set theory called ${ extsf{PZF}<^>{ extsf{U}}}$. This is done by using a delicate and careful choice of those Dedekind cuts that are taken as real numbers. ${ extsf{PZF}<^>{ extsf{U}}}$ is based on ancestral logic rather than on first-order logic. Its key feature is that it is definitional in the sense that every object that is shown in it to exist is defined by some closed term of the theory. This allows for a very concrete, computationally oriented model of it. The development of analysis in ${ extsf{PZF}<^>{ extsf{U}}}$ does not involve coding, and the definitions it provides for the basic notions are the natural ones.
Kumar and Banerjee (Some algebras and logics from quasiorder-generated covering-based approximation spaces. J Appl Non-classical Log 2024;34:248-68) characterized a subclass of quasiorder-generated covering-based approximation spaces for which the algebra of definable sets forms a Stone algebra. In this paper, we characterize those subclasses for which the definable sets form dual Stone, regular double Stone, linear Heyting, and well-connected Heyting algebras. As a consequence, discrete dualities of the aforementioned algebras are also obtained. Furthermore, we provide representation theorems of the aforementioned algebras in terms of rough sets determined by a quasiorder.
Kearns semantics for modal logic has been introduced in 1981 and was revived by Omori and Skurt in 2016, who recasted the semantics using the framework of non-deterministic matrices. However, it was unclear whether the semantics is analytic: given a partial model, can it be extended to a complete modal? In this paper we provide an affirmative answer for the case of logics K and KT.
This paper develops new closed form normal approximations for the ergodic distribution of a renewal-reward process $X(t)$ describing a semi-Markovian inventory model of type $(s, S)$. When demand sizes follow a Weibull distribution with shape parameter $\alpha \ge 3$, the renewal function can be well approximated by that of a normal distribution, as shown by Cui and Xie. We use this observation to derive a new numerical method for computing the ergodic distribution $Q_{X}(x)$ of the process $X(t)$. The resulting formulas are easy to evaluate and avoid repeated numerical computation of the Weibull renewal function. Numerical examples show that the approximations are accurate over a wide range of parameter values and that, as the replenishment threshold increases, the ergodic distribution of the inventory level approaches a uniform distribution.
This study introduces and investigates a Gentzen-style sequent calculus, sQBDi, for Niki and Omori's extended first-order intuitionistic Belnap-Dunn logic, QBDi. The propositional fragment of QBDi is an intuitionistic variant of De and Omori's extended Belnap-Dunn logic, BD+, with classical negation. The intuitionistic-negation-less propositional fragment of QBDi is an intuitionistic variant of Avron's self-extensional paraconsistent four-valued logic, SE4. In this study, the cut-elimination, Kripke completeness, and Craig interpolation theorems for sQBDi are proved through several theorems concerning syntactical and semantical embeddings of sQBDi into a Gentzen-style sequent calculus for first-order intuitionistic logic. The paraconsistent and constructive properties of sQBDi are also derived. This study also provides some comparisons, including one between sQBDi (which follows the American plan for negation) and Moisil-Leitgeb's HYPE (which follows the Australian plan for negation).
The arithmetic $ extbf{R}<^>{\boldsymbol{\sharp }}$ is obtained by postulating standard axioms for Peano arithmetic on a basis of the relevant logic R rather than classical logic. It is known that there is no way to extend $ extbf{R}<^>{\boldsymbol{\sharp }}$ from a theory of natural numbers to one of rational numbers meeting "obvious" desiderata. In this paper, we consider one way of obtaining a relevant number theory more congenial to rational arithmetic, by strengthening the postulate "zero is not a successor", adding that if it is a successor then 0 = 1. We call the resulting theory $ extbf{R}<^>{\boldsymbol{ atural }}$. Many properties of $ extbf{R}<^>{\boldsymbol{\sharp }}$ carry over to $ extbf{R}<^>{\boldsymbol{ atural }}$. For instance, there is still a finitary proof of absolute consistency, and there are still infinite propositional structures interpreting the relevant implication connective even though the models of equations are simplified down to the classical (bivalent) ones. One important result concerning $ extbf{R}<^>{\boldsymbol{\sharp }}$ that does not apply to $ extbf{R}<^>{\boldsymbol{ atural }}$ is the Friedman-Meyer proof of the non-admissibility of material detachment and consequent incompleteness for classical Peano arithmetic in the classical vocabulary. While it remains an open question whether material detachment is admissible, it does hold for formulae in the classical vocabulary, so all theorems of classical arithmetic are provable relevantly in $ extbf{R}<^>{\boldsymbol{ atural }}$.
Over the past few years, a new cluster of abstract algebras has emerged within the general context of research in rough set theory. Among them, one is the weakly topological quasi-Boolean algebra. This paper studies the vicinity of weakly topological quasi-Boolean algebra from algebraic and logical perspectives. The weak pre-rough algebra is defined, and a cluster of intermediate algebras between it and the quasi-Boolean algebra is explored. The interrelationship and independence among them are presented. We also establish sound and complete sequential systems for these algebras. Further, we show the finite model property and construct decidable algorithms for weakly topological quasi-Boolean algebra and its weaker variants by context-free grammars. Rough set models of some of these algebras have been presented.
In several papers [6-8], Beall argues that, since we can add to non-classical (including paraconsistent) arithmetics rules that restore classicality, we can effectively recover classical arithmetical reasoning in non-classical systems. According to Halbach and Nicolai [18], however, the move to non-classical arithmetic comes at the expense of proof-theoretic strength, undermining Beall's claims. Then how can paraconsistent arithmetics be said to recover classical strength? It is not sufficient to prove classical arithmetical consequences in a fragment of the language, as done e.g. by Friedman and Meyer [14], since this would yield strictly weaker theorems. In this paper, I provide a so-called classical recapture result for Zach Weber's paraconsistent arithmetic $ extsf{subDLQ-A}$, based on the logic $ exttt{subDLQ}$ [43]. I reconstruct a notion of coding and recursion for this paraconsisent arithmetic, and show that the theory, if supplemented with additional forms of induction and classical axioms for identity, supports Gentzen's classical lower bound proof for transfinite induction up to any ordinal less than $\varepsilon _{0}$.
In its initial formulation, CG'(3) is a three-valued paraconsistent calculus derived from specific modifications to the matrix of G & ouml;del logic G(3). We show that enriching CG'(3) with the so-called Aristotle's theses, or their equivalent variants, leads to a trivial logic. To resolve this issue, we define certain proper subsystems of CG'(3) in a manner that prevents trivialization. However, unlike prevailing perspectives in connexive logic, we do not assume that certain classically valid formulas must be rejected due to their counter-intuitive nature. By extending some subsystems ofCG'(3) with Aristotle's theses, our objective is to develop calculi that validate as many CG'(3)-valid formulas as possible while remaining non-trivial.
In this paper, we introduce the variety of equality algebras endowed with universal quantifiers (called uE-algebras), and establish an equivalent category for the corresponding category. Most significantly, we present an expansion of uE-algebras by enriching them with an internal state operator (which are referred to as state uE-algebras), and investigate some of their fundamental algebraic properties. In particular, we discuss the correspondence between state m-deductive systems and m-congruences of state uE-algebras. We also provide a set of characterizations for subdirectly irreducible state uE-algebras, together with characterizations for local and simple state-morphism uE-algebras, which play a crucial role in studying the variety of state uE-algebras. Finally, using the notion of adjoint m-pairs, we obtain a representation for state-morphism operators on uE-algebras.
The relationship between formal and informal provability has been a significant subject of philosophical and mathematical investigation. Formal systems such as G & ouml;del-L & ouml;b logic (GL) capture formal provability but do not validate the reflection schema-a principle stating that if a statement is provable, it must be true. This schema is intuitively valid for the informal notion of provability as understood and used in mathematical practice. Several logical systems have been developed to capture this informal notion of provability, including BAT, CABAT, and T-BAT. However, a first-order version of T-BAT logic has not yet been developed. This paper aims to address this research gap by providing such an extension.
