arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.08323

Essence and accident modalities meet Belnapian truth values

Yaroslav Petrukhin
View original source ↗Read source document ↗Export metadata ↓

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

cs.LOmath.LO

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

arXiv2026

A Logspace-Constructive Proof of L=SL

We formalize the proof of Reingold's Theorem that SL=L [Rei05] in the theory of bounded arithmetic VL, which corresponds to ``logspace reasoning''. As a consequence, we get that VL=VSL, where VSL is the theory of bounded arithmetic for ``symmetric-logspace reasoning''. This resolves in the affirmative an old open question from Kolokolova [Kol05] (see also Cook-Nguyen [NC10]). Our proof relies on the Rozenman-Vadhan alternative proof of Reingold's Theorem ([RV05]). To formalize this proof in VL, we need to avoid reasoning about eigenvalues and eigenvectors (common in both original proofs of SL=L). We achieve this by using some results from Buss-Kabanets-Kolokolova-Koucký [Bus+20] that allow VL to reason about graph expansion in combinatorial terms.

cs.LO↗
arXiv2026

A new method for proving confluence on abstract reduction systems --- Confluence of non-E-overlapping weakly-shallow TRSs ---

This paper proposes a new method for proving the confluence of an abstract reduction system (ARS) by clarifying the sufficient conditions, called compatibility and edge commutativity, for expanding a given finite sub-ARS into a confluent one by adding rewrite edges. This method can be regarded as an extension of our earlier work, which showed that a weakly non-overlapping, shallow, and non-collapsing term rewriting system (TRS) is confluent. Furthermore, we apply our method to demonstrate that a non-$E$-overlapping and weakly shallow TRS is confluent. Here, a term is weakly shallow if each defined function symbol occurs either at the root or in the ground subterms, and a TRS is weakly shallow if both sides of all its rewrite rules are weakly shallow. This drops the non-collapsing condition assumed in our previous work on weakly shallow TRSs. Moreover, since a weakly shallow TRS is non-$E$-overlapping whenever it is non-$ω$-overlapping, and the latter property is decidable, we also obtain a decidable sufficient condition for confluence: non-$ω$-overlapping and weakly shallow TRSs are confluent.

cs.LO↗
arXiv2026

Two-Variable Logic with Arbitrarily Many Successor Relations

We study two-variable first-order logic with a finite, input-dependent number of distinguished successor relations and arbitrary additional unary and binary predicates. Each distinguished relation must be the exact immediate-successor relation of some linear order on the common domain; the orders themselves are not available in the language and may have arbitrary order types. We prove that satisfiability belongs to 2NEXPTIME, uniformly in the number of successors. The proof gives finite certificates for possibly infinite models. A closure operation separates local neighbourhood descriptions, called star types, into those of bounded multiplicity and those that can be realized infinitely often. The bounded part is represented explicitly. Outside it, integer height vectors allow overlapping successor requirements to be matched without creating cycles or unintended identifications. Ordering the resulting path components densely then recovers exact successor relations. Consistent assignments of the additional binary predicates handle witnesses involving the bounded part. The same certificates decide infinite satisfiability in 2NEXPTIME and give a doubly exponential threshold above which a finite model guarantees an infinite model. A doubly exponentially large finite core can be forced with only two successors and unary predicates. For finite models, we prove that satisfiability subject to a bound on the total number of reference adjacencies lost by the other orders is NEXPTIME-complete, even when the budget is encoded in binary and the number of successors is part of the input.

cs.LO↗