Splitting Meanings: A Unified View on Paraconsistency and Inconsistency Measurement

1 Introduction

Real-world knowledge bases frequently exhibit inconsistencies because information is aggregated from diverse sources, using different methodologies, or at different times. This heterogeneity often results in conflicts within these knowledge bases. Classical propositional logic is inadequate for reasoning under such conditions: once an inconsistency arises, the principle of explosion makes every formula derivable. Consequently, this limitation has motivated the development of various formalisms for handling inconsistency, including argumentation [Besnard and Hunter, 2008], belief revision [Hansson, 2022], and paraconsistency [Priest et al., 2022]. Inconsistency measurement complements these by providing quantitative ways to assess how far a knowledge base is from consistency (e.g., see [Thimm, 2018; Bona et al., 2019]).

In this paper, we propose a framework that can serve as a common basis for both tasks. The main idea is to distinguish between the surface level, where formulas are written in an ordinary propositional language, and a marked level, where each occurrence of an atom is equipped with a marker. Markers are interpreted as pointers to worlds in a possibleworlds structure [Kripke, 1959]. Intuitively, a marker identifies a context, source, or meaning in which the corresponding occurrence is evaluated. Two occurrences of the same propositional variable need not share a truth value unless they share a marker.

Using the possible-worlds semantics, we define minimality-based entailment through abnormality functions. An abnormality function assigns to each model a set of defects. We compare models by set inclusion and prefer those with smaller defect sets. Our approach is inspired by abnormality minimization in nonmonotonic reasoning [McCarthy, 1986]. Different choices of abnormality function capture different notions of what should be considered problematic: splitting markers into different worlds, changing the truth value of a variable across markers, or deviating from the normal world. Importantly, all these instantiations live in the same simple semantic universe.

Despite its simplicity, the framework is expressive. On the one hand, it can recover a variety of paraconsistent entailment relations. First, it can capture an entailment relation based on maximal satisfiable subsets (MSSes) [Rescher and Manor, 1970] by using markers that distinguish different formulas and a minimality criterion that penalizes non-normal markers. Second, it can encode the minimally inconsistent Logic of Paradox [Priest, 1991] via two special markers and an abnormality function that counts variables taking abnormal truth values. Third, it can reproduce an entailment relation defined through occurrence-based semantics [Salhi, 2025] by using an abnormality function that minimizes the number of variables whose occurrences are forced to disagree in truth value. Each of these formalisms arises as a particular choice of marking strategy and abnormality function within the same generic scheme.

On the other hand, our framework can be used to give a uniform basis for a broad family of inconsistency measures. Different measures correspond to different ways of counting or minimizing abnormalities in marked models. In particular, by choosing appropriate markings and abnormality functions, we can express:

• formula-based measures such as those defined in terms of MSSes and problematic formulas [Grant and Hunter, 2011];

• model-based measures such as Dalal's distance-based measures [Grant and Hunter, 2017];
• paraconsistency-based measures such as contension [Konieczny et al., 2003; Grant and Hunter, 2011];
• a forgetting-based measure [Besnard, 2016], which quantifies how many occurrences must be forgotten (replaced by constants) to restore consistency.

In each case, the value of the measure is recovered as the cardinality of some minimal abnormality set.

The benefits of our framework can be summarized as follows. First, the underlying logic is purely propositional with a standard, two-valued semantics at each world. Markers and abnormality functions add only a lightweight layer to this classical basis. Second, different forms of paraconsistent reasoning are obtained by only varying the marking strategy and the choice of abnormality function. Third, diverse approaches to inconsistency measurement, which are usually presented in different frameworks, can be seen as instances of the same general pattern of minimality over marked models.

2 RelatedWork

Our use of markers is connected to various labelled formalisms in the literature. Labelled proof systems attach labels to formulas at the syntactic level in order to reason about possible worlds, time points, or other parameters [Fitch, 1966; Gabbay, 1996; Vigan`o, 2000]. In particular, labelled systems for the normal modal logic S5 can avoid an explicit accessibility relation by working inside a single equivalence class of worlds. Hybrid logics [Blackburn, 2000] also enrich modal languages with special atomic symbols, called nominals, together with an operator that allows one to express that a formula holds at a designated state. In this way, hybrid logics provide a formal mechanism for contextual reasoning, with nominals serving to identify and reason about distinct contexts. Other approaches to contextual reasoning based on syntactic or semantic enrichment have been developed in various forms in the literature; see, for example, [Ghidini and Giunchiglia, 2001; Serafini and Bouquet, 2004; Klarman and Guti´errez-Basulto, 2011; Serafini and Homola, 2012; G´omez ´Alvarez and Rudolph, 2021]. However, these frameworks are not designed to single out and manipulate propositional variables via labels, nor do they aim to model inconsistency or defining inconsistency-tolerant entailment relations. In particular, they do not typically combine labels with explicit minimality principles that directly target abnormal behavior of variables or occurrences.

To deal with inconsistency, our framework uses multiple worlds to allow an atom to be associated with more than one truth value. Assigning more than one truth value to an atom is a central idea in paraconsistency, and in particular in the (minimally inconsistent) Logic of Paradox [Priest, 1991]. In contrast to many-valued approaches, however, our use of worlds and markers yields a more fine-grained perspective: it operates at the level of occurrences of atoms, rather than at the level of atoms alone.

In a recent article [Salhi, 2025], occurrence-based entailment relations were introduced. However, that approach does not enforce that particular occurrences share the same truth value, whereas our framework achieves this through a shared marker. Moreover, the semantics proposed in [Salhi, 2025] does not single out any occurrence as normal, while our framework designates a dedicated marker corresponding to the normal world. Finally, that approach does not support the range of minimality conditions naturally expressible in the present framework.

Despite these differences, we show that both the Logic of Paradox and occurrence-based entailment relations can be encoded in a simple and uniform way in this framework.

3 Preliminaries

Let Prop be a countable set of propositional variables. The set PF of propositional formulas over Prop is defined inductively by the grammar ϕ ::= p | ⊥ | ¬ϕ | (ϕ ∧ ϕ) | (ϕ ∨ ϕ), where p ∈ Prop. We use the usual definitions of the other connectives.

Let vars(ϕ) denote the set of propositional variables occurring in ϕ.

An interpretation over Prop is a function ω : Prop → {0, 1}, where 1 stands for true and 0 for false. We write Ω(Prop) for the set of all interpretations.

The satisfaction relation ω |=CL ϕ is defined inductively as usual.

For a set Γ ⊆ PF, we write ω |=CL Γ iff ω |=CL ϕ for all ϕ ∈ Γ. We say that Γ is satisfiable (or consistent) iff there exists ω ∈ Ω(Prop) such that ω |=CL Γ. Otherwise, Γ is unsatisfiable (or inconsistent).

In connection with inconsistency, we focus on the following three standard notions.

Definition 1 (Minimal Unsatisfiable Subset). A subset M ⊆ Γ is a minimal unsatisfiable subset (MUS) of Γ iff: (i) M is unsatisfiable; and (ii) for every M ′ ⊊ M, the set M ′ is satisfiable.

Definition 2 (Maximal Satisfiable Subset). A subset S ⊆ Γ is a maximal satisfiable subset (MSS) of Γ iff: (i) S is satisfiable; and (ii) for every ϕ ∈ Γ \ S, the set S ∪ {ϕ} is unsatisfiable.

Definition 3 (Minimal Correction Subset). A subset C ⊆ Γ is a minimal correction subset (MCS) of Γ iff: (i) Γ \ C is satisfiable; and (ii) for every C ′ ⊊ C, the set Γ\C ′ is unsatisfiable.

For a set of formulas Γ, we denote by MUS(Γ) (resp., MSS(Γ), MCS(Γ)) the set of all minimal unsatisfiable subsets of Γ (resp., maximal satisfiable subsets of Γ, minimal correction subsets of Γ).

4 A Propositional Logic withMarkers

In this section, we introduce a propositional logic in which occurrences of propositional variables are equipped with markers, and show how these markers can be used to handle inconsistency.

Consider a set of formulas K = {p ∨ q, ¬p, ¬q}, which is clearly inconsistent. In many situations, we do not want to treat the two occurrences of p or those of q as describing exactly the same piece of information. For example:

• p could be read as "the system is hot" in two different physical contexts (e.g., two different sensors, or two different time points);
• or as "this student is eligible for the scholarship" as assessed by two different models;
• or more generally as the same predicate used with different meanings or sources.

Intuitively, it is coherent to accept that one source says p while another says ¬p, without collapsing into triviality.

To capture this formally, we introduce markers that allow us to distinguish occurrences of the same variable. For instance, we can write K⋆ = {pα ∨ qβ , ¬pγ , ¬qβ }, where α, β and γ are markers. If α ̸= γ, the two occurrences of p may receive different truth values. Thus, the marked set K⋆ is satisfiable. At the same time, we retain the option of forcing two occurrences to share the same meaning by giving them the same marker. This can be observed for the two occurrences of q.

As a result, the logic with markers distinguishes two levels: (1) the surface level, where the same letter p may appear in many places; (2) the marked level, where each occurrence is refined into pα, and only occurrences with the same marker are required to share a truth value. This provides a natural way to reason about inconsistency that is sensitive to potential differences in meaning or information source.

Let us now introduce the syntax and the semantics of the logic with markers, denoted ML. We assume a countable set of markers Mk that contains the specific symbol ν. Markers are denoted by letters such as α, β, and γ, possibly with subscripts.

The set of ML formulas (marked formulas) is obtained by the following grammar: ϕ ::= pα | ⊥ | ¬ϕ | (ϕ ∧ ϕ) | (ϕ ∨ ϕ), where p ∈ Prop and α ∈ Mk.

Intuitively, pν is read as "p in the normal context", while pα, with α ̸= ν, is read as "p in context, source, or meaning α". Two occurrences pα and pβ are treated as potentially distinct pieces of information unless we explicitly identify α and β.

A central idea of the semantics is that markers control which occurrences must share a truth value. We model this by allowing valuations to depend on equivalence classes of markers.

An ML-model is a tuple M = 〈W, w0, V, λ〉, where W is a set of possible worlds, w0 ∈ W, V : W → 2Prop is a valuation function, and λ : Mk →W with λ(ν) = w0. Intuitively, w0 is used to represent what we regard as the "normal" meaning/context.

Given an ML-model M = 〈W, w0, V, λ〉 and an ML formula ϕ, the satisfaction relationM |=ML ϕ is defined inductively as follows:

We use M(Prop,Mk) for the set of all ML-models.

A set of marked formulas Γ is satisfiable iff there exists an ML-model M such that M |=ML ϕ for all ϕ ∈ Γ. We write

Mod(Γ) = {M ∈ M(Prop, Mk) | M |=ML Γ}.

We define a marker configuration of an ML-model as the equivalence relation ∼λ on markers induced by λ: α ∼λ β iff λ(α) = λ(β).

Different choices of marker configuration ∼λ correspond to different assumptions about when two occurrences must share a meaning:

• If ∼λ is the identity relation (only α ∼λ α), then markers are fully independent. In this case, occurrences like pα and pβ (with α ̸= β) may freely receive different truth values.
• If ∼λ is the universal relation (all markers equivalent), then for each p there is effectively a single truth value shared by all pα. In this case, we recover the classical semantics for propositional logic.

Therefore, the logic with markers provides a flexible framework in which we can control, via the marker configuration, which occurrences of the same propositional variable are forced to behave classically and which may diverge. This allows a more fine-grained analysis of inconsistency.

5 Minimality and Entailment

The introduction of markers can greatly increase the number of models satisfying a marked formula, since both the marker configuration and the valuation can vary while still satisfying the same marked formula. Intuitively, however, not all of these models should be considered equally plausible. Some models are more conservative: they identify more markers with one another, or keep propositional variables as stable as possible across their occurrences. Other models exhibit more abnormal behavior, for instance by splitting markers into different worlds or allowing the same variable to take different truth values.

When information is potentially inconsistent, it is natural to define entailment using only those models that are minimal in a well-motivated sense. This idea is common in nonmonotonic reasoning and belief revision: among the possible ways of handling the information, one prefers those that deviate as little as possible from a preferred pattern of behavior. Our approach is particularly inspired by abnormality minimization in nonmonotonic reasoning [McCarthy, 1986].

In our setting, the idea is as follows: we split meanings only when necessary, and we change truth values only when unavoidable. We capture this by associating with each model a set of abnormalities and then restricting attention to models whose abnormality set is minimal under set inclusion.

Definition 4 (Abnormality functions and minimal models). An abnormality function is any function f : M(Prop,Mk) → 2U , where U is some fixed universe of (abnormality) items (e.g. markers, variables, or both).

For a set Γ of marked formulas, the set of f-minimal models of Γ is defined by Modmin f (Γ) = {M∈ Mod(Γ) ∣∣ ∄N ∈ Mod(Γ) such that f(N) ⊊ f(M)}.

Entailment is defined via truth in all f-minimal models.

Definition 5 (Minimality-based entailment). Let f be an abnormality function. For sets Γ of ML formulas and an ML formula ϕ, we define the entailment relation |∼mk f as follows:

Different choices of abnormality function f give rise to different entailment relations. Conceptually, f(M) specifies what the current instantiation regards as problematic in M, and minimality then selects those models that minimize the problematic items.

We now describe a few simple but useful abnormality functions. These will serve as building blocks in later sections, where we show how different choices of f and different marking strategies recover a range of well-known inconsistencytolerant entailment relations.

Let M = 〈W, w0, V, λ〉 be an ML-model.

1. Non-normal markers. We first quantify how much a model deviates from the normal world by using markers that do not point to w0:

Minimizing f1 favors models in which as many markers as possible are interpreted at the normal world, i.e., models that use the normal meaning or context whenever this is compatible with consistency.

1. Splitting of markers. Next, we measure to what extent markers are separated into different worlds. The following abnormality function works relative to a fixed set of formulas Γ. Indeed, we restrict our attention to the set of markers that actually occur in Γ. We use MkΓ to denote the set of markers occurring in Γ.

Each pair {α, β} in f Γ 2 (M) indicates that α and β belong to distinct ∼λ-equivalence classes. Thus, minimizing f Γ 2 favors models that identify as many markers as possible, i.e., models with fewer distinct meanings or contexts. In what follows, we write f2 instead of f Γ 2 whenever the underlying set Γ is clear from the context.

1. Truth-value changes. A third dimension of abnormality concerns variables whose truth value is not stable across worlds pointed to by markers:

Thus, a propositional variable p is in f3(M) iff p takes a different truth value at some marker world than it does at the normal world. Minimizing f3 expresses a preference for models in which each variable keeps a single truth value across all its occurrences, unless inconsistency forces a change.

1. Variable-marker abnormalities. Finally, we may wish to record not only which variables change truth value, but also where they change. This provides a more finegrained abnormality function:

In this case, the abnormalities are individual pairs (p, α) at which p deviates from its normal truth value. Minimizing f4 penalizes each such deviation separately, allowing more fine-grained control over the trade-offs between splitting meanings and changing truth values.

These functions can also be combined or refined in various ways. In the rest of the paper we will show that, together with suitable marking strategies, they suffice to recover several familiar forms of inconsistency-tolerant entailment relations, as well as a broad range of inconsistency measures.

6 Encoding Paraconsistent Entailment Relations

To illustrate the flexibility of our framework, we now show how it can encode several paraconsistent entailment relations. More precisely, we consider three instantiations: an entailment relation based on MSSes [Rescher and Manor, 1970], the entailment relation of the minimally inconsistent Logic of Paradox [Priest, 1991], and an entailment relation defined via an occurrence-based semantics [Salhi, 2025]. These examples cover approaches that are often seen as orthogonal in the literature and demonstrate that the ML semantics, combined with suitable abnormality functions, can uniformly capture a spectrum of paraconsistent reasoning principles.

6.1 AnMSS-based Entailment

We first consider the following well-known entailment relation based on MSSes [Rescher and Manor, 1970]. For Γ ⊆ PF and ϕ ∈ PF, the entailment relation ⊢MSS is defined as follows:

To relate this to our framework, we first transform formulas to marked formulas. Given a formula ψ and a marker α, we write τform(ψ, α) for the marked formula obtained from ψ by replacing each occurrence of a variable p with pα.

We now fix a marking strategy that associates with each formula ψ ∈ Γ a distinct marker αψ ̸= ν (i.e. different formulas receive different non-normal markers). Given a set of formulas Γ, we set τform(Γ) = {τform(ψ, αψ) ∣∣ ψ ∈ Γ}.

The following lemma states that, whenever a marker α is interpreted at the normal world w0, the satisfaction of the marked translation τform(ψ, α) coincides with the classical satisfaction of ψ at w0.

Lemma 1. Let M = 〈W,w0, V, λ〉 be an ML-model and ωM the classical interpretation defined by ωM(p) = 1 iff p ∈ V (w0). Then, for every formula ψ ∈ PF and every marker α with λ(α) = w0, M |=ML τform(ψ, α) iff ωM |=CL ψ.

Proof. By a straightforward induction on the structure of ψ, using the clauses for ML-satisfaction and the definition of τform.

Now, we can characterize MSS-based entailment in terms of our marked semantics and the abnormality function f1 from Section 5 (f1(M) is the set of markers that do not point to the normal world w0).

Note that the correspondence requires each formula in the considered set to be classically satisfiable. Our encoding represents the choice of keeping or discarding a formula in an MSS by deciding whether its marker can stay at the normal world w0 or must be assigned to a non-normal world.

If a formula ψ is itself inconsistent, then τform(ψ, α) is unsatisfiable at every world, so there is no model in which ψ can be kept. In that case, the one-to-one correspondence between MSSes of Γ and f1-minimal models of τform(Γ) breaks down.

Theorem 1. For every set Γ whose members are individually consistent, and every formula ϕ, Γ ⊢MSS ϕ iff τform(Γ) |∼mk f1 τform(ϕ, ν).

Intuitively, each f1-minimal model of τform(Γ) corresponds to choosing an MSS of Γ: the formulas whose markers stay at the normal world w0 are exactly those that are kept, while moving a marker away from w0 amounts to discarding the corresponding formula. Lemma 1 guarantees that truth at w0 for the marked translations coincides with classical truth for the original formulas. Conversely, every MSS of Γ can be turned into an f1-minimal model by assigning its formulas to w0 and the others to non-normal worlds.

6.2 Minimally Inconsistent Logic of Paradox

We now recall the minimally inconsistent Logic of Paradox LPm [Priest, 1991] and show how it can be captured in our framework.

An LPm interpretation is a function µ : PF → {{0}, {1}, {0, 1}} that assigns to each propositional formula ϕ ∈ PF a set of classical truth values and satisfies the following conditions: µ(⊥) = {0}, µ(¬ϕ) = {1 - v | v ∈ µ(ϕ)}, µ(ϕ ∧ ψ) = {min{v, v′ } | v ∈ µ(ϕ), v′ ∈ µ(ψ)}, and µ(ϕ ∨ ψ) = {max{v, v′ } | v ∈ µ(ϕ), v′ ∈ µ(ψ)}.

We write µ! = {p ∈ Prop | µ(p) = {0, 1}} for the set of variables that receive both truth values under µ.

We say that µ is an LPm model of a formula ϕ, and write µ |=LPm ϕ, iff 1 ∈ µ(ϕ). The LPm interpretation µ is an LPm model of a set of formulas Γ, written µ |=LPm Γ, iff it is a model for every formula in Γ.

The LPm interpretation µ is a minimally inconsistent (or simply minimal) LPm model of Γ iff µ |=LPm Γ, and for every LPm interpretation µ′ with µ′ ! ⊊ µ!, µ′ ̸|=LPm Γ.

A set of formulas Γ entails ϕ in LPm, written Γ ⊢LPm ϕ,

iff for every minimal LPm model µ of Γ, we have µ |=LPm ϕ. Let pos and neg be two distinct markers in Mk\{ν}. Given a formula ϕ ∈ PF, we define the marked translations πpos (ϕ) and πneg (ϕ) inductively as follows:

• πpos (⊥) = ⊥, πneg (⊥) = ⊥; πpos (p) = ppos , πneg (p) = pneg ;
• πpos (¬ψ) = ¬πneg (ψ), πneg (¬ψ) = ¬πpos (ψ);
• πα(ψ ⊗ χ) = πα(ψ) ⊗ πα(χ) for α ∈ {pos, neg} and ⊗ ∈ {∧, ∨}.

Given an LPm interpretation µ, we associate with it an ML-model Mµ = 〈W,w0, V, λ〉, where W = {w0,w1}, V (w0) = {p ∈ Prop | 1 ∈ µ(p)}, V (w1) = {p ∈ Prop | µ(p) = {1}}, and λ(pos) = w0, λ(neg) = w1, and λ(β) = w0 for each other marker β. Intuitively, w1 is used to assign value 0 to occurrences marked by neg. More precisely, if µ(p) = {0} then p is in neither V (w0) nor V (w1); if µ(p) = {1} then p is in both; and if µ(p) = {0, 1} then p is in V (w0) but not in V (w1).

The following lemma states that the f3-abnormal variables of Mµ are exactly those variables p such that µ(p) = {0, 1}.

Proof. Let us recall that f3(M) is the set of propositional letters p such that p takes different truth values at the normal world w0 and at some world designated by a marker (in our setting, the only relevant such markers are pos and neg, with λ(pos) = w0 and λ(neg) = w1).

We distinguish the three possible values of µ(p).

• If µ(p) = {1}, then p ∈ V (w0) and p ∈ V (w1): p has the same (true) value at both worlds, so p /∈ f3(Mµ).
• If µ(p) = {0}, then p /∈ V (w0) and p /∈ V (w1): p has the same (false) value at both worlds, so p /∈ f3(Mµ).
• If µ(p) = {0, 1}, then 1 ∈ µ(p), hence p ∈ V (w0), but µ(p) ̸= {1}, so p /∈ V (w1). Thus p takes different truth values at w0 and w1, so p ∈ f3(Mµ).

It follows that f3(Mµ) consists exactly of those p such that µ(p) = {0, 1}.

The following lemma shows that, in the associated model Mµ, the translations πpos and πneg exactly reflect the two truth components of µ.

Lemma 3. Let µ be an LPm interpretation. Then, for every formula ϕ, the following holds:

Using the two previous lemmas, we can show that whenever µ is a minimal LPm model of Γ, the associated structure Mµ is an f3-minimal ML-model of {πpos (ϕ) | ϕ ∈ Γ}.

For the converse direction, let M = 〈W,w0, V, λ〉 be an ML-model such that λ(pos) = w0, λ(β) = w0 for every β ̸= neg, and V (λ(neg)) ⊆ V (w0). Let µM be defined by 1 ∈ µM(p) iff p ∈ V (λ(pos)), 0 ∈ µM(p) iff p /∈ V (λ(neg)). Under these restrictions, f3(M) coincides with µM!.

Lemma 4. Let Mbe an ML-model satisfying the above compatibility condition, and let µM be the associated LPm interpretation. Then, for every formula ϕ:

1. 1 ∈ µM(ϕ) iffM |=ML πpos (ϕ);
2. 0 ∈ µM(ϕ) iffM̸|=ML πneg (ϕ).

The previous lemma, together with the observation f3(M) = µM! for LPm-compatible ML-models, guarantees that if M is an f3-minimal LPm-compatible ML-model of {πpos (ϕ) | ϕ ∈ Γ}, then the associated interpretation µM is a minimal LPm model of Γ.

The following theorem establishes the correctness of our encoding of ⊢LPm in our framework. The proof is obtained by exploiting the correspondence between minimal LPm models and f3-minimal ML-models using the translations Mµ and µM.

Theorem 2. For every set of formulas Γ and every formula ϕ, Γ ⊢LPm ϕ iff πpos (Γ) |∼mk f3 πpos (ϕ), where πpos (Γ) = {πpos (ψ) | ψ ∈ Γ}.

6.3 Occurrence-based Semantics

We now show how to encode, within our framework, an entailment relation defined via an occurrence-based semantics [Salhi, 2025].

Intuitively, instead of assigning a single truth value to each variable, we assign truth values to occurrences of variables and then prefer interpretations that minimize the number of disagreements between occurrences of the same variable.

A syntactic occurrence of a variable p in a formula ϕ can be identified by a triple (p, i, ϕ), where i is the position of that occurrence when counting from left to right. We write Occ(ϕ) for the set of all such occurrences in ϕ, and for a set Γ of formulas we set Occ(Γ) = ⋃ψ∈Γ Occ(ψ). Furthermore, let Occ(Γ, p) be the set of occurrences of the variable p in Γ. For an occurrence o ∈ Occ(Γ), we denote by var(o) the propositional variable that occurs at o.

Let R be a function that assigns to each occurrence o ∈ Occ(Γ) a distinct fresh propositional variable R(o). Given a formula ϕ, we write R(ϕ) for the formula obtained from ϕ by replacing, for each o ∈ Occ(ϕ), that occurrence by R(o).

An occurrence-based interpretation (or o-interpretation) of Γ is a function ϵ : Occ(Γ) → {0, 1}. We say that ϵ is an o-model of Γ iff there exists a classical interpretation ωϵ such that ωϵ(R(o)) = ϵ(o) for all o ∈ Occ(Γ), and ωϵ |=CL R(ψ) for all ψ ∈ Γ. Thus, an o-model assigns truth values to occurrences in a way that can be realized by a classical model of the occurrence-renamed version of Γ.

To define the corresponding nonmonotonic entailment relation, we impose a minimality condition on o-models. For an o-interpretation ϵ of Γ, let diff(ϵ) = {{o, o′ } ⊆ Occ(Γ) | var(o) = var(o′ ) and ϵ(o) ̸= ϵ(o′ )}. In words, diff(ϵ) records all pairs of occurrences of the same variable that receive different truth values under ϵ.

We define a preorder ⪯ on o-interpretations of Γ by ϵ ⪯ ϵ′ iff diff(ϵ) ⊆ diff(ϵ′ ). The associated strict preorder is denoted by ≺, i.e. ϵ ≺ ϵ′ iff ϵ ⪯ ϵ′ and diff(ϵ) ̸= diff(ϵ′ ).

An o-model ϵ of Γ is minimal if it is minimal with respect to ⪯: whenever ϵ′ is an o-interpretation of Γ with ϵ′ ≺ ϵ, then ϵ′ is not an o-model of Γ.

We say that a classical interpretation ω is compatible with an o-interpretation ϵ of Γ if, for every propositional variable p occurring in Γ, there exists an occurrence o ∈ Occ(Γ) with var(o) = p such that ω(p) = ϵ(o). In other words, ω assigns to each variable a value that agrees with at least one of its occurrences under ϵ.

The occurrence-based entailment relation ⊢occ is then defined as follows:

Definition 6. For a set of propositional formulas Γ and a formula ϕ, we write Γ ⊢occ ϕ iff for every minimal o-model ϵ of Γ and every classical interpretation ω compatible with ϵ, we have ω |=CL ϕ.

To encode this entailment relation in our framework, we introduce two marking schemes.

Occurrence-marking. The translation τocc assigns a distinct marker αo to each occurrence o ∈ Occ(Γ) of a propositional variable in the formulas under consideration. We write τocc(Γ) for the set of marked formulas obtained from Γ by replacing each occurrence o of a variable p with pαo .

Variable-marking. The translation τvar assigns a distinct marker αp to each propositional variable p (all occurrences of p receive the same marker αp). We write τvar(ϕ) for the formula obtained from ϕ by replacing each occurrence of p with pαp . We assume that the markers used by τocc and those used by τvar are pairwise distinct.

For convenience, we continue to write αo for the marker associated with an occurrence o, and αp for the marker associated with the variable p.

Theorem 3. For every finite set of formulas Γ and every formula ϕ, Γ ⊢occ ϕ iff τocc(Γ) |∼mk f2 (Θ → τvar(ϕ)), where Θ = ∧p∈vars(ϕ) ∨o∈Occ(Γ,p) (pαp ↔ pαo ).

Intuitively, τocc(Γ) records truth values at the level of occurrences, while τvar(ϕ) evaluates ϕ at the level of variables. The formula Θ ties each variable-marker αp in ϕ to at least one occurrence marker αo of p in Γ. Minimizing f2 then mimics the minimization of diff(ϵ) in the original occurrencebased semantics: we prefer models that identify as many markers as possible, i.e., models that make as many occurrences of the same variable agree as the formulas in Γ allow.

It is worth noting that our encoding applies only to finite sets of formulas. This restriction comes from the auxiliary formula Θ, which must explicitly include all occurrences.

7 InconsistencyMeasurement

Inconsistency measures are intended to quantify the degree of contradiction present in a knowledge base. They have been widely studied in the literature, often within postulatebased frameworks that capture different desirable properties of such measures (see, e.g., [Hunter and Konieczny, 2010; Thimm, 2018; Bona et al., 2019; Besnard and Grant, 2020]). Inconsistency measures have been applied in a variety of areas, including paraconsistency [Salhi, 2021; Corea et al., 2024], databases [Parisi and Grant, 2023; Grant and Parisi, 2024], spatio-temporal qualitative reasoning [Condotta et al., 2016], business rule analysis [Corea et al., 2021], and deontic reasoning [Arieli et al., 2024].

A knowledge base (KB) is a finite set K ⊆ PF of individually consistent formulas. We use KB to denote the set of KBs.

We impose the consistency of individual formulas mainly to ensure that formula-level marking, via τform(K), can restore consistency. Indeed, if a formula ψ is itself inconsistent, then τform(ψ, α) is unsatisfiable at every world. Thus, there is no model in which ψ can be retained. However, this assumption is not essential: it can be removed by a simple preprocessing step that filters out inconsistent formulas. Moreover, for our other marking approaches, the results can be generalized to KBs that may contain inconsistent formulas.

Definition 7 (Inconsistency Measure). An inconsistency measure is a mapping I : KB → R≥0 ∞ such that, for every KB K, CONSISTENCY I(K) = 0 iff K is consistent.

Beyond CONSISTENCY, a number of additional postulates have been proposed to further constrain inconsistency measures (e.g., see [Thimm, 2018]). We do not commit to a particular collection of such postulates here. Instead, we focus on showing how several well-known measures can be expressed within our logical framework by associating their values with the cardinalities of suitable minimal abnormality sets in marked models.

7.1 Examples of InconsistencyMeasures

We briefly recall some measures from the literature. Let K be a KB.

• The MSS-counting measure [Grant and Hunter, 2011]: Imss(K) = |MSS(K)| - 1.
• A problematic-formula measure [Grant and Hunter, 2011]: IP(K) = |Problematic(K)|, where Problematic(K) = ⋃ MUS(K).
• A contension-based measure [Konieczny et al., 2003; Grant and Hunter, 2011]: IC(K) = Contension(K), where Contension(K) = min{ |µ!| | µ |=LPm K}.
• A formula-based hitting-set measure [Grant and Hunter, 2017]: IH(K) = min{|X| | X ⊆ K, ∀K′ ∈ MUS(K),X ∩K′ ̸= ∅}.
• A model-based hitting-set measure [Thimm, 2016]: Ihs(K) = min{|H| | H ∈ HS(K)} - 1, where HS(K) is the family of model-based hitting sets for K, i.e., HS(K) = {H ⊆ Ω(Prop) | ∀ϕ ∈ K, ∃ω ∈ H : ω |=CL ϕ}.
• The Dalal-sum distance measure [Grant and Hunter, 2017]: I Σ dalal (K) = min{∑ϕ∈K d(ϕ, ω) | ω ∈ Ω(Prop)}, where d(ϕ, ω) is Dalal's distance between ϕ and the interpretation ω.
• A forgetting-based measure [Besnard, 2016; Thimm,
• 2018]:
• Iforget(K) = min{k | ∃(pj, ij, cj)kj=1 (∧ K)[p1, i1 ↦→ c1; . . . ; pk, ik ↦→ ck] ̸⊢ ⊥, cj ∈ {⊤,⊥}}. Here, for a formula ϕ and a triple (p, i, c) with p ∈ Prop, i ∈ N, and c ∈ {⊤,⊥}, we write ϕ[p, i ↦→ c] for the formula obtained from ϕ by replacing the i-th occurrence of p in ϕ (counted from left to right) by the constant c. For a finite sequence (pj, ij, cj)kj=1 , the notation ϕ[p1, i1 ↦→ c1; . . . ; pk, ik ↦→ ck] denotes the result of performing all these replacements.

7.2 ExpressingMeasures viaMarkers and Abnormalities

We now show how our logical framework with markers and abnormality functions can express all of the above inconsistency measures.

Formula-level marking. We first consider the marking τform defined in Section 6.1: each formula ϕ in the considered KB is assigned its own marker αϕ ̸= ν, and τform(K) denotes the set of corresponding marked formulas.

Proposition 1. Let K be a KB. Then:

• Ihs(K) = min{|Mk/∼λM| | M∈ Mod(τform(K))} - 1, where Mk/∼λM is the set of equivalence classes of markers induced by λM;
• Imss(K) = |{f1(M) | M∈ Modmin f1 (τform(K)) }|-1;
• IP(K) = | ⋃{f1(M) | M∈ Modmin f1 (τform(K))}|;
• IH(K) =min{|f1(M)| | M∈ Mod(τform(K))};
• I Σ dalal (K) =min{|f4(M)| | M∈ Mod(τform(K))}.

As noted above, if inconsistent formulas are allowed in KBs, the preceding results can be easily adapted. For instance, in this setting we obtain Imss(K) = |{ f1(M) | M ∈ Modmin f1 (τform(K\Inc(K)))}|+|Inc(K)|-1, where Inc(K) denotes the set of inconsistent formulas in K.

Polarity-levelmarking. We nowconsider themarking πpos introduced in Section 6.2, which uses two markers pos and neg to encode the Logic of Paradox.

Here, IC counts the minimal number of variables that must take two truth values in order to satisfy K, and f3 captures exactly such deviations in our framework.

Occurrence-level marking. Finally, we consider the marking τocc defined in Section 6.3, which assigns a distinct marker to each occurrence of a propositional variable in the formulas of K.

Intuitively, τocc(K) makes it possible to forget individual occurrences of variables by allowing them to deviate from their normal values, and f4 counts how many such deviations are needed to restore consistency. This mirrors the definition of Iforget.

8 Conclusion and Perspectives

We have introduced a logical framework that separates the surface propositional language from a marked layer, where occurrences of atoms are evaluated at possibly different worlds. Abnormality functions assign to each model a set of defects, which induces a preference ordering over models. This provides a uniform semantic basis for inconsistencytolerant entailment and inconsistency measurement: by varying the marking scheme and the notion of abnormality, we can recover MSS-based entailment, the minimally inconsistent Logic of Paradox, an occurrence-based entailment relation, and a wide range of inconsistency measures.

There are several natural directions for future work. First, it would be useful to develop proof systems and algorithms for our framework. Second, we could extend the approach to richer logics (e.g., first-order or description logics) and to settings with time or multiple sources. Third, viewing inconsistency measures and entailment through the common lens of markers and abnormalities may support a systematic, postulate-based analysis of existing measures and guide the design of new ones.