Searcharxiv⌕ Search

arXiv · 2610.08323

Essence and accident modalities meet Belnapian truth values

Abstract

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.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Yaroslav Petrukhin. 2026-10-06. Essence and accident modalities meet Belnapian truth values. https://doi.org/10.1007/s11225-026-10250-z

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Proving at Scale for Universal Algebra

We introduce SemiBase, a project that computes and formally certifies finite identity bases for small semigroups. Deciding finite basability is undecidable for finite algebras and remains open for finite semigroups. The task requires a proof that a candidate basis is complete, or a proof that none exists, rather than a single first-order validity query. LLM-guided agents search for these proofs; a referee agent rebuilds them from source, and the Lean kernel checks the resulting corpus in a final audit. Humans choose targets and approve final outcomes. We certify every semigroup of order at most 6: all 1309 semigroups of order at most 5 and all 15973 of order 6, including proofs that the four known nonfinitely based semigroups have no finite basis. The bases for order 6 define 505 distinct varieties, whose inclusion order Vampire determines except for four pairs. The resulting catalogue is a machine-checked account of results scattered across the literature and a tested foundation for order 7.

cs.LO↗

From Zero-Dimensional to Continuous Dualities: A Double-Categorical Account

We investigate how to systematically construct continuous dualities from zero-dimensional dualities, employing well-known methods from algebra, topology, category theory, and domain theory. While our method is general, this paper focusses on the move from Stone spaces to compact Hausdorff spaces and the move from Priestley spaces to compact ordered Hausdorff spaces. The engine of our approach is Stone duality for relations: on the space side quotienting by a preorder turns zero-dimensional spaces into continuous ones, while distributive lattices with a proximity relation are their algebraic duals. Our duality for relations is inherently order-enriched. Double categories organise both functional and relational morphism in the same structure. The move from zero-dimensional to continuous dualities is then a three-step construction: extend a duality from functional to relational morphism, split idempotents, restrict to maps.

cs.LO↗

A First Introduction to Isabelle/ML Metaprogramming: Automatic Estimation of Polynomial Degrees

This article offers an introduction to metaprogramming in Isabelle/HOL for beginners, based on a running example for working with multivariate polynomials. The example is motivated by our formalisation of universal Diophantine pairs. We describe the implementation of the poly_degree command, which computes upper bounds on the total degrees of multivariate polynomials and automatically proves their correctness. The complete metaprogram handles a variety of special cases but herein we present a simplified version for the sake of exposition. We describe our development process and design decisions; our goal is to offer a small and self-contained tutorial on Isabelle/ML, for mathematicians who want to get started with metaprogramming.

cs.LO↗