This paper concerns the categoricity problems, or Carnap’s problems, of some non-classical logics. I first review the categoricity theorems of LP and K3 proved by Tabakci (2024) and give a counterexample to a proposition in his paper. Then I prove some categoricity results of FDE and a theorem connecting that of FDE and those of LP and K3. I also prove that FDE is categorical regarding the star models and that LP and K3 are not categorical regarding their star models.
Kernel contraction, introduced by Sven Ove Hansson, is a fundamental method for withdrawing information from belief bases. Through the Levi Identity —which defines revision in terms of contraction— kernel contraction also induces the corresponding revision operator known as kernel revision. Recent work has proposed a non-prioritized variant of kernel contraction which, unlike its classical counterpart, may violate the Success postulate, and thereby permits some non-tautological beliefs to be protected from removal. This article develops a corresponding notion of non-prioritized kernel revision. Building on the machinery of classical kernel revision and non-prioritized kernel contraction, we define a revision mechanism that need not always incorporate incoming evidence. The proposal is given both a constructive formulation, via a generalized Levi Identity, and an axiomatic (postulational) characterization. Finally, we analyse its epistemic impact by showing how non-prioritized kernel revision can weaken or reinforce the degree of firmness of selected beliefs within a belief base, and how these effects can accumulate under iteration, eventually yielding endorsement of the epistemic input and de-endorsement of its negation.
The well-known“slingshot” argument concludes that sentences designate neither facts, nor situations, nor propositions, but instead designate one of the two truth values. We find fault with the argument by laying it out in the context of Bressan’s (1972) improved version of Carnap’s (1947) “method of extension and intension”: The argument is fallacious inasmuch as it employs the “method of the name relation,” which awards each sentence only one semantic value instead of both an extension and an intension.
Second-order purely universal axioms can be reduced to arithmetical inference rules that allow a proof analysis. We apply this axioms-as-rules method to a classical second-order monadic modal logic ( SOML_c ) with explicit predicative comprehension for a countable language. This logic is shown, through a reduction procedure, to be a conservative extension of first-order modal logic extended with rules ( FOML_c ). Termination of the reduction procedure requires an explicit vector expression measure that corresponds to induction on natural numbers. As a consequence the consistency of a second-order arithmetic with predicative comprehension follows assuming transfinite induction up to ε _0 on elementary recursive predicates EA-TI(ε _0) . The second part implements the method for Gödel’s ontological proof. Two standard variants, Scott’s version and Anderson’s emendation, of the argument are considered. The ontological argument proving the necessary existence of a godlike individual, formally ∃ x. G(x) , uses classical indirect reasoning to prove the possible existence of a godlike individual. By the reduction of SOML_c extended with ontological rules to FOML_c , and by a formula transformation that replaces G with falsity, intuitionistic underivability of ∃ x. G(x) is shown for the predicative monadic modal logic. The proof of reduction reduces derivability of ∃ x. G(x) in SOML_c to derivability of an inconsistency in propositional modal logic. Because the second-order underivability result requires the reduction to first-order provability, the proof is relative, and assumes EA-TI(ε _0) .
We introduce a general rough set–based semantic framework for propositional logics that are not algebraizable in the sense of Blok–Pigozzi. The approach is based on the identification of a well-behaved algebraizable fragment of the language, which is interpreted as an observational level over the space of algebraic valuations. This restriction induces a natural indistinguishability relation and, consequently, non-trivial rough approximations in the sense of Pawlak. Within this setting, semantic indeterminacy emerges as a structural phenomenon generated by the loss of algebraic information under projection onto the chosen fragment. In particular, formulas whose semantic values cannot be reconstructed from the observational level give rise to non-empty rough boundaries. This motivates the notion of rough indeterminacy, which is defined and characterized independently of the derivability of explicit contradictions. The paraconsistent logic C_ω is used as a motivating case study, illustrating how rough indeterminacy naturally arises when negation fails to be algebraically determined by the positive fragment. More generally, the proposed framework provides a structural and informational perspective on non-algebraizability and suggests a methodological tool for the semantic analysis of logics whose full language resists standard algebraic treatment.
Abstract Good sequences are central to Mundici’s categorical equivalence between MV-algebras and unital $$\ell $$ ℓ -groups. We eliminate the reliance on Chang’s subdirect representation theorem traditionally used in the proof, replacing it with an entirely constructive argument based on entailment relations.
In this paper, we consider the set of all proper filters of a residuated lattice, equipped with the coarse lower topology. We study some topological properties of this space and we show that this space is spectral. Then after introducing a family of proper filters that satisfies the avoidance property, meaning that if a filter is included in the union of the family, then it is included in some member of the family, we show that a family of proper filters satisfies the avoidance property if and only if it is quasi-compact in the coarse lower topology. Moreover, by providing related examples and results, we construct families with this property. Finally, we show that the avoidance property does not necessarily hold for the family of minimal prime filters of a residuated lattice. As an application of this concept, by characterizing residuated lattices whose family of minimal prime filters satisfies the avoidance property, we prove that a residuated lattice is quasi-complemented if and only if the family of its minimal prime filters satisfies the avoidance property. Several further related results are also derived.
This paper investigates many-valued generalisations of the classical essence and accident modalities. In two-valued logic, a proposition is essentially true (resp. false) if, whenever it is true (resp. false), it is necessarily true (resp. false); it is accidentally true (resp. false) if it is true (resp. false) but not necessarily so. Many-valued logics provide a natural setting for introducing further modalities of this kind. We focus on Belnap–Dunn’s First-Degree Entailment (FDE), a four-valued system that generalises the classical truth values. More precisely, we consider an extension of FDE with Boolean negation and implication. In addition to modalities of essential and accidental truth and falsity, we define modalities of essential and accidental inconsistency and indeterminacy. We present a four-valued S5-based Kripke semantics and cut-free hypersequent calculi for the resulting logics. We then prove semantic and syntactic embedding theorems for these logics into a four-valued version of S5 with necessity and possibility modalities. These embeddings clarify the intended interpretation of the Belnapian essence and accident modalities and yield soundness, completeness, and cut-admissibility results.
This paper investigates the logic of compatibility as a ground for the logic of conditionals. We identify a family of principles expressing key properties of compatibility, which can be coherently ordered. Assuming that conditionals are definable in terms of incompatibility—the negation of compatibility—each of the principles identified yields corresponding principles governing conditionals. Clarifying these derivability relations provides a new perspective on several existing accounts of conditionals.
In this paper, we offer an account of a paradox analogous to Fitch’s paradox of knowability, elaborated around knowledge of necessary truths—such as mathematical or logical truths. In particular, we highlight at which semantic levels the paradox does and does not rise, and explain why that happens. The account employs a novel modal operator and language, which present some distinctive semantic features, such as being unable to characterise many frame properties characterisable in normal modal logic, a fact which may be used in interesting ways to study the logics of the proposed language. Following recent studies, this work may be seen as a case study of semantically insensitive non-normal modal logics.
The paper investigates Nuel Belnap’s idea of double time references and its application to speech act theory. First, Belnap’s metalinguistic analysis of speech act reports in the branching-time setting is presented. Second, it is proven that these reports can be analyzed within the object language of Ockhamist logic if the language includes the indexicals now and then. Belnap complained that the language of the “tree dwellers” lacks the expressiveness required to capture the idea of double time references. This paper resolves this issue.
The two main titular results are (I) no finite matrix of values characterizes propositional Core Logic ℂ , and (II) the connectives of propositional Core Logic are independent. These results echo the corresponding ones for propositional Intuitionistic Logic. Our reason for expounding them for Core Logic is that their metaproofs are easier and more accessible in that setting; and the result for Intuitionistic Logic corresponding to (II) is then a corollary to the Admissibility of Cut in Core Logic.
The notion of reduced sequents plays an important role in proving the decidability of some sequent calculi. A reduced sequent is a sequent without repetitive substructures. While it is straightforward to obtain reduced sequents in Gentzen-style calculi, it is unclear how to obtain them algorithmically in modal display calculi, because modal display calculi contain more complex structures in sequents so that repetitive substructures cannot be recognized at first sight. This paper provides an algorithm to count minimal repetitive substructures in a sequent and to obtain reduced sequents and shows that reduced sequents obtained from a sequent are ‘equivalent’ in a certain sense. Moreover, the paper discusses a proposal for proving the decidability of a modal display calculus and analyzes the reasons why it does not work. The algorithm and proposal may serve as a stepping stone for analyzing calculi with complex structures in sequents and proving their decidability.
In 2007, Diaconescu and Georgescu introduced tense MV-algebras, and later, in 2015, Botur and Paseka continued the study of this class of algebras, obtaining various types of representation theorems. The aim of this work is to investigate tense MV-algebras and determine a topological duality for these algebras.
Display calculi were introduced by Nuel Belnap in [3] as a natural extension of Gentzen’s sequent calculi, as a uniform and modular framework capable of encompassing broad classes of logics. In [28], the properly displayable (D)LE-logics are syntactically characterized as the logics axiomatised by analytic inductive axioms for any signature. We extend the framework of proper display calculi for LE-logics to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. This class of axioms covers and properly extends all Sahlqvist axioms. The present framework takes inspiration from Schroeder-Heister’s calculus of Higher-Level Rules [32] and captures the whole acyclic fragment of the substructural hierarchy [7] when generalized to arbitrary signatures. We apply unified correspondence theory and the algorithm ALBA to uniformly generate analytic rules for the aforementioned axiomatic extensions.
Selective revision operators are well-known non-prioritized revision operators that allow for the acceptance of only part of the new information while rejecting the rest. In this paper, we introduce their contraction counterparts, which we refer to as selective contraction operators. These operators enable the removal of only part of the input information. As such, selective contractions can be viewed as a method for removing some of the beliefs that support the input belief without eliminating the belief itself. In this sense, selective contraction operators allow for a weakening of the input belief’s strength without discarding it. We provide representation theorems for various classes of selective contraction operators.
We further develop the formal foundations of Paraconsistent Belief Revision (PBR) by introducing Logics of Formal Inconsistency (LFIs) specifically designed to support the development of epistemic entrenchment-based models for belief change. The interpretation of formal consistency—and, more broadly, of paraconsistency—in terms of the epistemic attitudes adopted by rational agents and of these agents reasoning with potentially contradictory yet non-trivial epistemic states, respectively, is already well-established within the literature on PBR based on LFIs. However, previous approaches faced a key limitation: the absence of replacement in most LFIs prevented the construction of entrenchment-based operations. We address this gap by first revisiting and systematizing core properties essential for such modeling, formalizing them within Cbr, a previously introduced logic whose foundational properties we now examine and develop in depth. Building on this, we introduce RCbr, a replacement-enriched, self-extensional extension of Cbr, which makes it possible—within an LFI-based framework—to formally define epistemic entrenchment and to construct entrenchment-based belief revision mechanisms. This development enables a fully constructive approach to Belief Revision in paraconsistent settings, further advancing the theoretical treatment of LFIs and paraconsistency within the broader landscape of epistemic states and belief dynamics.
We encode Belnap’s basic theory of display calculi in the proof assistant Coq/Rocq version 8.18.0 and formalise the proof that Belnap’s conditions C2–C8 imply the cut-elimination theorem. Our framework allows us to formally prove meta-theoretic results such as Hilbert-completeness and derivability of explicit rules, such as cut, but also others if required. What makes our formalisation powerful is that it works entirely with an abstraction that can be instantiated to many possible logics and display calculi, although we make no attempt to precisely characterise the logics that can be properly displayed in our formalisation. For this reason, our work can be seen as a formalisation of a display calculus framework and a cut-elimination theorem for a wide range of display calculi. As examples, we apply our work to classical propositional logic (CPL), tense logic (Kt), and non-commutative non-associative Lambek calculus to obtain complete display calculi as well as formally proved cut-elimination theorems, but we believe our formalisation to be also applicable to many others. We also encoded a proof of the decidability of CPL that relies only on the structure of proofs within an additive display calculus for CPL. To our knowledge, our work is the first formalisation of a decidability result in display calculus. Moreover, all of our formal proofs are constructive as they never require the addition of the law of excluded middle in Coq’s environment (which is constructive by default), which means we were also able to extract computer programs from our proof of cut-elimination able to convert CPL/Kt/Lambek derivation trees into cut-free ones. As formal proofs are known to be significantly longer to write than usual pen-and-paper proofs, our work led to the development of a multitude of files of Coq code comprising more than 15,000 lines.
