arXiv subjects

Yaroslav Petrukhin

Publications and source records attributed to Yaroslav Petrukhin.

7 recordsLinked to original sources

arXiv2026

Essence and accident modalities meet Belnapian truth values

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.

cs.LO↗

arXiv2026

On Three-Valued Dependence-Like Logics

In this paper, we investigate connections between dependence logics, viewed as a subclass of relating logics, and three-valued logics. More specifically, we identify common features of Epstein's subject-matter semantics and the variable-inclusion conditions characteristic of some infectious many-valued logics. Inspired by Del Cerro and Lugardon's sequent calculi for dependence logics, in which classical connectives are combined with connectives satisfying Epstein-style conditions, we introduce two three-valued dependence-like logics that combine classical conjunction and disjunction with infectious negation and implication. We also provide sound, complete, and cut-free bisequent calculi for these logics.

cs.LO↗

arXiv2025

On a Second-Order Version of Russellian Theory of Definite Descriptions

Definite descriptions are first-order expressions that denote unique objects. In this paper, we propose a second-order counterpart, designed to refer to unique relations between objects. We investigate this notion within the framework of Russell's theory of definite descriptions. While full second-order logic is incomplete, its fragment defined by Henkin's general models admits completeness. We develop our theory within this fragment and formalize it using a cut-free sequent calculus.

cs.LO↗

arXiv2024

A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic

The method Kürbis used to formalise definite descriptions with a binary quantifier I, such that I$x[F,G]$ indicates `the F is G', is examined and improved upon in this work. Kürbis first looked at I in intuitionistic logic and its negative free form. It is well-known that intuitionistic reasoning approaches truth constructively. We also want to approach falsehood constructively, in Nelson's footsteps. Within the context of Nelson's paraconsistent logic N4 and its negative free variant, we examine I. We offer an embedding function from Nelson's (free) logic into intuitionistic (free) logic, as well as a natural deduction system for Nelson's (free) logic supplied with I and Kripke style semantics for it. Our method not only yields constructive falsehood, but also provides an alternate resolution to an issue pertaining to Russell's interpretation of definite descriptions. This comprehension might result in paradoxes. Free logic, which is often used to solve this issue, is insufficiently powerful to produce contradictions. Instead, we employ paraconsistent logic, which is made to function in the presence of contradicting data without devaluing the process of reasoning.

cs.LO↗

arXiv2024

Bisequent Calculi for Neutral Free Logic with Definite Descriptions

We present a bisequent calculus (BSC) for the minimal theory of definite descriptions (DD) in the setting of neutral free logic, where formulae with non-denoting terms have no truth value. The treatment of quantifiers, atomic formulae and simple terms is based on the approach developed by Pavlović and Gratzl. We extend their results to the version with identity and definite descriptions. In particular, the admissibility of cut is proven for this extended system.

cs.LO↗

arXiv2024

Uniform Cut-free Bisequent Calculi for Three-valued Logics

We present a uniform characterisation of three-valued logics by means of the bisequent calculus (BSC). It is a generalised form of a sequent calculus (SC) where rules operate on the ordered pairs of ordinary sequents. BSC may be treated as the weakest kind of system in the rich family of generalised SC operating on items being some collections of ordinary sequents, like hypersequent and nested sequent calculi. It seems that for many non-classical logics, including some many-valued, paraconsistent and modal logics, the reasonably modest generalisation of standard SC offered by BSC is sufficient. In this paper we examine a variety of three-valued logics and show how they can be formalised in the framework of BSC. We present a constructive syntactic proof provided that these systems are cut-free, satisfy the subformula property, and allow one to prove the interpolation theorem in many cases.

cs.LO↗

arXiv2022

Normalisation for Some Infectious Logics and Their Relatives

We consider certain infectious logics (Sfde, dSfde, K3w, and PWK) and several their non-infectious modifications, including two new logics, reformulate previously constructed natural deduction systems for them (or present such systems from scratch for the case of new logics) in way such that the proof of normalisation theorem becomes possible for these logics. We present such a proof and establish the negation subformula property for the logics in question.

cs.LO↗