Essence and accident modalities meet Belnapian truth values

1 Introduction

• The authors adopt the Marcos–Steinsvold reading: ◦A is conditionally essentially true, while •A is true but possibly false.On this reading, ◦⊥ says that if ⊥ were true, it would be true at every accessible world, rather than asserting that ⊥ is actually true.Source: §1 · pp. 1–2
• The alternative modality ⊡A = A ∧ □A collapses to □A in reflexive modal logics, so studying it without that collapse requires a non-reflexive logic.This is presented as a limitation of that alternative approach.Source: §1 · p. 2
• The value-indexed modalities cover essential and accidental truth, falsity, inconsistency, and indeterminacy, while separate operators address being at least true or at least false.For values b and n, the modalities capture inconsistency and indeterminacy; the at-least operators concern designated truth or falsity status.Source: §1 · pp. 2–3
• The system extends FDE with Boolean negation and implication, retaining De Morgan negation to handle contradictory and partial information and using implication to define essence.The two negations support the paper’s definitions of the many-valued modalities.Source: §1 · p. 2
• FDE’s values are treated as epistemic statuses: true, false, contradictory information, or no information.The paper consequently treats essence and accident modalities as epistemic as well.Source: §1 · p. 2
• The paper uses a four-valued S5 semantics and develops hypersequent proof theory for the modalities, building on an earlier extension of Restall’s S5 calculus.The paper also reports embedding results and derives soundness, completeness, cut admissibility, and decidability.Source: §1 · p. 3

2 Semantics

• The semantics uses nonempty worlds and valuations into the four FDE values, with truth-value conditions for the propositional connectives and □ and ♢.The paper also defines the two-valued S5 model and its classical truth conditions as a reference point.Source: §2 · p. 4
• The truth and falsity conditions define essential and accidental operators for particular values and for at-least-true or at-least-false status using local and accessible-world conditions.The conditions distinguish universal persistence across worlds from existential variation in a world’s value.Source: §2 · p. 5
• The semantic conditions establish equivalences among the four operator forms under Boolean negation and relate the T- and F-indexed operators through De Morgan negation.For value-indexed operators, the conditions also relate modalities for n to those for b under negation and conflation.Source: §2 · pp. 5–6
• Abbreviations A_i identify formulas expressing that A has a specified FDE value, while A_T and A_F express the corresponding classical truth or falsity components.The semantics also distinguishes at-least-true and at-least-false conditions through membership of T or F in the valuation.Source: §2 · pp. 4–6
• The authors retain the full family of 24 operators as primitives even though many are definable from other operators and □ and ♢.They do so to provide a uniform semantic and proof-theoretic treatment of the different truth statuses.Source: §2 · p. 6

3 Hypersequent calculi

• A hypersequent is a finite multiset of sequents, and it is valid when at least one component sequent is valid.Each sequent is an ordered pair of finite multisets of formulas.Source: §3 · p. 7
• The calculi build on Restall’s S5 hypersequent calculus and extend it with rules for Boolean negation, propositional connectives, and modal operators.Rules for conjunction and disjunction are given in multiplicative form to shorten the embedding proofs.Source: §3 · pp. 7–8
• The calculus adopts a more general external weakening rule, allowing arbitrary hypersequents, including the empty one.This formulation is associated with a constructive cut-elimination proof in earlier work, though constructive cut elimination is not pursued here.Source: §3 · p. 7
• Cut elimination for FDES5 is proved using embedding procedures, which do not require rules to be invertible.This avoids relying on invertibility of Merge, which fails because p ⇒ | ⇒ p is invalid while p ⇒ p is valid.Source: §3 · p. 8
• The essence-and-accident calculus replaces the necessity and possibility rules with rules for Belnapian essence and accident operators.The section presents rules for two groups of both essence and accident operators, alongside rules for truth-value connectives.Source: §3 · pp. 8–10

4 Embedding theorems

• FDES5□♢ proves a hypersequent H exactly when S5 proves its translation f(H).The weak embedding lemma supplies the cut-free directions used to establish the equivalence.Source: §4 · p. 12
• Cut is admissible in FDES5□♢, and the system is sound and complete for its semantics.Cut admissibility follows from the syntactic embedding and cut admissibility for Restall’s S5 hypersequent calculus; soundness and completeness follow from the syntactic and semantic embeddings.Source: §4 · pp. 12–13
• The semantic embedding preserves and reflects formula values between FDES5□♢ and S5 under f, with corresponding models constructible in both directions.The lemmas relate values of A and ¬A in the source model to those of f(A) and f(¬A) in the translated model.Source: §4 · pp. 12–13
• A weak syntactic embedding maps FDES5◦• into FDES5□♢ by translating ◦_I A as g(A_I) → □g(A_I).The mapping g otherwise carries negations, connectives, and modalities through the translation; the passage begins an inductive proof of the embedding.Source: §4 · p. 13
• The syntactic embedding theorem relates FDES5 hypersequent derivability to derivability in the FDES5 system with necessity and possibility.The theorem states the embedding for each hypersequent.Source: §4 · p. 16
• Cut is admissible in FDES5.The proof follows from Theorems 5 and 2.Source: §4 · p. 16
• Theorem 7 names a semantic embedding from FDES5 ◦• into FDES5 □♢; Lemma 6 states that T ∈ ϑ(¬A, x) in M1 iff T ∈ ϑ′(g(¬A), x) in M2.Source: §4 · p. 17
• FDES5 is decidable.The proof uses the decidability of S5 together with Theorems 1 and 5.Source: §4 · p. 18

• Some modalities, including ◦b and ◦n, cannot be expressed in two-valued modal logic.Source: §5 · p. 18
• The modalities could be studied in K3, LP, or n-valued logics, with J-operators offering one proposed definition for n-valued essence.The proposed definition is −◦kA = JkA →□JkA.Source: §5 · p. 18
• A bi-facial logic could distinguish modalities such as essential ontological truth and accidental epistemic falsity.Its four values are T1, T0, F1, and F0, separating ontological and epistemic components.Source: §5 · p. 18
• The modalities could also be investigated with modal logics beyond S5, including K5, GL, and other modal systems.Source: §5 · p. 18
• Further work could develop first-order hypersequent calculi and incorporate definite descriptions through ι-terms or hybrid operators.Source: §5 · p. 18
• Many-valued hybrid operators are proposed for truth-value, essential-value, and accidental-value conditions across modal worlds; their combined form needs separate investigation.The combined operator describes ψ accidentally taking value i where φ essentially takes value i.Source: §5 · p. 18