Paraconsistency in hybrid logic

Abstract

As in standard knowledge bases, hybrid knowledge bases (i.e. sets of information specified by hybrid formulas) may contain inconsistencies arising from different sources, namely from the many mechanisms used to collect relevant information. Being a fact, rather than a queer anomaly, inconsistency also needs to be addressed in the context of hybrid logic applications. This article introduces a paraconsistent version of hybrid logic which is able to accommodate inconsistencies at local points without implying global failure. A main feature of the resulting logic, crucial to our approach, is the fact that every hybrid formula has an equivalent formula in negation normal form. The article also provides a measure to quantify the inconsistency of a hybrid knowledge base, useful as a possible basis for comparing knowledge bases. Finally, the concepts of extrinsic and intrinsic inconsistency of a theory are discussed.

1 Introduction

Management of knowledge and information is a key issue in all infrastructures underlying modern information-centric societies. Therefore, the study and development of flexible logical systems able to handle heterogeneous and complex data has become more and more relevant in the last two decades, resorting to interdisciplinary research in Linguistics, Computer Science, Mathematics and even Philosophy.

A knowledge (management) base is a process which stores in digital form huge, complex information, either structured or unstructured to be processed by several sorts of software systems. A crucial ingredient in this process is the inference of new data from old, which entails the need for its precise representation in an adequate logical formalism.

Description logics are variants of first-order logic which count as one of the most popular formalisms to deal with knowledge bases. In strict first-order logic, the evaluation of a formula is unable to consider the context in which it takes place. Since data is obtained from different sources, and often through an elementary natural language interface, special care is required to distinguish and classify formulas according to the different modes (or degrees, or stages) in which they can be understood as true statements. Modal logic [9] provides a formalism for distinguishing between various modes of truth, or modalities, such as, knowledge, necessity or time. From a proof-theoretical point of view, such logics have interesting algorithmic properties, and, moreover, can naturally be translated into first-order logic. However, they lack the ability to explicitly refer to specific states, or stages of interpretation, which, in a number of cases, is a desirable feature. Hybrid logic [8], on the other hand, overcomes this limitation by introducing a new set of propositional symbols, called nominals, each of them holding only at a specific state—the state it names.

Often the act of collecting data for populating a knowledge base introduces contradictions. Being a common fact rather than a queer anomaly, contradictions have to be suitably addressed. In particular, one needs to handle data exhibiting, at the same time, assertions of the form |$q$| and |$\neg q$|⁠, configuring local contradictions, but without producing global inconsistency. This is certainly a problem for database operations with theorem-provers, and so has drawn much attention from computer scientists. Techniques for removing contradictory information have been investigated, e.g. in [29]. Yet, all of them have limited applicability, and, in any case, do not guarantee that consistency has been enforced.

An alternative approach offers a safe way to ‘live’ with inconsistency. Such is the domain of paraconsistent reasoning—a natural way to deal with inconsistency allowing both a sentence and its negation to be true. Paraconsistent logic is a mature and well established field of mathematical logic as the entry ‘03B53 - Paraconsistent logics’ in the 2010 Mathematics Subject Classification evidences.

A paraconsistent logic is a kind of non-classical logical system that does not obey the Principle of Explosion which states that from contradictory premises any formula can be derived. The Russian Vasil’év proposed, in 1910, a modified Aristotelian syllogistic including statements of the form: ‘S is both P and not P’, which seems to be the earliest paraconsistent logic in the contemporary era. However, the proposal did not make any significant impact at the time. Later on, the Polish logician Stanisław Jaśkowski, disciple of Łukasiewicz, developed the first (formal) system of propositional paraconsistent logic [22]. Afterwards, for the last sixty years, many philosophers, logicians and mathematicians have become involved in the area. The Brazilian logic school (Newton da Costa, Walter Carnielli, Jean-Yves Béziau, João Marcos, etc.) is prominent among them. The theory of paraconsistent logic has developed considerably as witnessed by both the increase in the number of publications, the number of dedicated specialized journals, and that of international conferences (e.g. 5th World Congress on Paraconsistency, in Kolkata, India, 2014; see [4, 6, 12, 26] for the proceedings of previous congresses).

Several variants of paraconsistent logic have been proposed, often to meet different aims or target-specific applications [24]. Research has been driven not only by theoretical interest, but also by genuine problems in different scientific domains, namely Computer Science, Medicine and Robotics. In the medical practice, e.g. consulting two or more doctors may lead to (partially) contradictory diagnoses, none of them to be dismissed. In Physics, paraconsistent logic was used to deal with some aspects of quantum mechanics in [14]. In Computer Science, subdomains like requirements engineering [18], artificial intelligence [15] and automated reasoning within information processing knowledge bases [16] are among the most relevant areas in which paraconsistent logic can address theoretical difficulties raised by inconsistent data. Other applications are discussed in [28].

To the best of our knowledge, published work in this direction is only concerned with inconsistencies in knowledge bases represented by first-order formulas. The work of Grant and Hunter and their collaborators is the most representative [9–21]. In particular, they propose Quasi-Classical (QC) logic, in [5, 19], which provides a measure for the inconsistency of data represented as a set of first-order formulas. Measuring inconsistency is crucial to an effective management of information, namely for comparing between different knowledge w.r.t. contradictions, allowing us to choose the ones with less conflicts. (The measure of inconsistency has also been studied by other logicians, e.g. Arieli and Zamansky in [2, 3].) The notion of Tarski’s satisfaction in [19] is decoupled into two interpretations for the predicate symbols: one for positive literals and another for negative ones. This semantics leads to weaker paraconsistent logics commonly known as First-Degree Entailment. As in the standard case, models (which are bistructures) can be represented by a set of ground literals. The definition of minimal QC models is introduced and it is proved that no useful information is lost when resorting to these models only. The inconsistency measure of a model is given by the quotient between the number of contradictions actually present in the bistructure and the total possible number of contradictions it may have.

This article proposes a new mathematical procedure to reason about knowledge bases formalized in hybrid logic that may contain inconsistencies arising from the way data was obtained. A variant of paraconsistent hybrid logic, following the work of Grant and Hunter [19], is presented. An important result that makes this generalization possible is the existence of Robinson diagrams in (global) hybrid logic. The method of diagrams, introduced by L. A. Henkin and A. Robinson, is a useful tool in model theory; for instance, the diagram of |$A$|⁠, the set of all atomic sentences and negation of atomic sentences that are true in |$A$|⁠, ‘characterizes’ all the models into which |$A$| can be embedded. This implies that hybrid models can be represented by a set of hybrid formulas in an extended language with new nominals such that all worlds are named.

In order to avoid double negation, we assume that all formulas are in negation normal form. The generalization is not straightforward, as explained below, but it allows for a reformulation of several notions (e.g. bistructure, minimal model, conflict base, etc.) in a new context. It should be remarked that there is already a number of studies concerned with paraconsistency in modal logic—e.g. the work of João Marcos in modal logic [23] and that of Torben Braüner on hybridization of Nelson’s logic N4 [11]. However, none of them discusses a measure of inconsistency in the models. Although it is an important issue, in this work we do not discuss the proof-theoretical aspects of this new logic which combines paraconsistency and hybrid logic; this topic is left for further research. For now, the measure of inconsistency is the main issue addressed.

Outline of the article.Section 2 reviews the introductory material to hybrid logic, namely its syntax and semantics together with the notion of bisimulation with constants. Then, Section 3 presents quasi-hybrid (QH) logic, which can be used to reason about knowledge bases represented by hybrid formulas. A measure for the inconsistency of a hybrid theory is proposed. We give several examples to illustrate the main concepts. This approach allows us to discuss whether a source is more consistent than other and by which degree. Bisimulation is discussed in section 4. We conclude by summarizing the main achievements of this work and by enumerating some topics for further research.

2 Hybrid Logic

Hybrid logic was introduced by Prior [25] in the 1950’s. The theory was significantly extended by his student Robert Bull. He developed a number of completeness results for generalizations of Prior’s hybrid logic. Some years later, in the 1980’s, the Bulgarian School of Logic (namely Passy, Tinchev, Gargov and Goranko) revived the interest in hybrid logic, studying, in particular, the possible roles of the binder operator. More recently, Areces and Blackburn expanded hugely the theory, addressing in particular the complexity of the satisfiability problem. Hybrid logics [8] are a brand of modal logics that provide appropriate syntax for the possible worlds semantics through nominals. In particular, it adds to the modal description of transition structures the ability to refer to specific states. If modal logics have been successfully used for specifying reactive systems, the hybrid component adds the possibility to refer to individual states and reason about the system’s local behaviour at each of them.

With hybrid logic we may express equality between states named by |$i$| and |$j$||$(@_i j)$| or accessibility of the latter from the former through a modality |$(@_i \Diamond j)$| or a statement at a specific state (⁠|$@_i \varphi$|⁠). Moreover, hybrid logic is strictly more expressive than its modal fragment. For example, irreflexivity |$(i \rightarrow \neg \Diamond i)$|⁠, asymmetry |$(i \rightarrow \neg \Diamond\Diamond i)$| or antisymmetry |$(i \rightarrow \Box ( \Diamond i \rightarrow i))$| are properties of the underlying transition structure which are simply not definable in standard modal logic [9]. Note that for the propositional case the satisfiability problem is still decidable.

Another important feature that will be central in our approach is the fact that basic hybrid logic can specify Robinson Diagrams. Namely, |$@_i p$| says that the proposition |$p$| is true at the state named by |$i$|⁠, while |$ \neg @_i p$| (logically equivalent to |$ @_i \neg p$|⁠) denies this; |$ @_i j$| says that the states named by |$i$| and |$j$| are identical, while |$ \neg @_i j$| (logically equivalent to |$ @_i \neg j$|⁠) states that they are distinct; finally, |$@ i \Diamond j$| says that the state named by |$j$| is a successor of the state named by |$i$|⁠, and |$\neg@ i \Diamond j$| (logically equivalent to |$ @_i \Box \neg j$|⁠) denies this. Consequently, in hybrid logic we are able to completely describe models. This way of looking at models as sets of formulas will be useful to measure the contradictions in a model, analogously to the QC case.

2.1 The basic hybrid language

We start by presenting the simplest form of hybrid logic: the basic hybrid language. The basic hybrid language introduces nominals and the satisfaction operator into the propositional modal logic. Although being a simple extension, it carries great power in terms of expressivity.

 

Definition 2.1

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom} \rangle$| be a hybrid similarity type where |$\mathrm{Prop}$| is a set of propositional symbols and |$\mathrm{Nom}$| is a set disjoint from |$\mathrm{Prop}$|⁠. We use |$p, q, r, etc.$| to refer to the elements in |$\mathrm{Prop}$|⁠. The elements in |$\mathrm{Nom}$| are called nominals and we typically write them as |$i, j, k, etc$|⁠. The set of well-formed formulas over |$L$|⁠, |$\mathrm{Form}_@(L)$|⁠, is defined by the following grammar:

$$WFF:=i|p|\mathrm{\perp }|\mathrm{\top }|\mathrm{\neg }\phi |\phi \vee \psi |\phi \wedge \psi |◊\phi |◻\phi |{@}_i\phi .$$

For any nominal |$i$|⁠, |$@_i$| is called a satisfaction operator.

 

Definition 2.2

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom} \rangle$| be a hybrid similarity type. A hybrid structure|$\mathcal{H}$| over |$L$| is a tuple |$(W, R, N, V)$|⁠. Here, |$W$| is a non-empty set called domain whose elements are called states or worlds, and |$R$| is a binary relation such that |$R\subseteq W\times W$| and is called the accessibility relation. |$N:\mathrm{Nom}\rightarrow W$| is a function called hybrid nomination that assigns nominals to elements in |$W$| such that for any nominal |$i$|⁠, |$N(i)$| is the element of |$W$| named by |$i$|⁠. We call this element the denotation of |$i$| under |$N$|⁠. |$V$| is a hybrid valuation, which means that |$V$| is a function with domain |$\mathrm{Prop}$| and range |$Pow(W)$| such that |$V(p)$| tells us at which states (if any) each propositional symbol is true.

The pair |$(W, R)$| is called the frame underlying |$\mathcal{H}$| and |$\mathcal{H}$| is said to be a structure based on this frame.

We define a homomorphism between hybrid structures by considering them as first-order structures. Concretely,

 

Definition 2.3

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom} \rangle$| be a hybrid similarity type, |$\mathcal{H}=(W, R, N, V)$| and |$\mathcal{H}'=(W', R', N', V')$| be two hybrid structures over |$L$|⁠. A homomorphism |$h$| from |$\mathcal{H}$| to |$\mathcal{H}'$| is a map |$h:W\rightarrow W'$| such that

• (1) for any |$p\in \mathrm{Prop}$| and any |$w\in W$|⁠, |$w\in V(p)$| iff |$h(w)\in V'(p)$|⁠;

• (2) for any |$i\in \mathrm{Nom}$|⁠, |$h(N(i))=N'(i)$|⁠;

• (3) for any |$w,s\in W$|⁠, |$w R s$| implies that |$h(w) R' h(s)$|⁠.

We say that |$h$| is an embedding if it is injective and the condition (3) holds in the strong version:

for any |$w,s\in W$|⁠, |$w R s$| iff |$h(w) R' h(s)$|⁠.

The satisfaction relation, which is defined as follows, is a generalization of Kripke-style satisfaction.

 

Definition 2.4

(Satisfaction) The local satisfaction relation |$\models$| between a hybrid structure |$\mathcal{H}=(W, R, N, V)$|⁠, a state |$w\in W$| and a hybrid formula is recursively defined by:

• (1) |$\mathcal{H}, w\models i$| iff |$w=N(i) $|⁠;

• (2) |$\mathcal{H}, w\models p$| iff |$w\in V(p) $|⁠;

• (3) |$\mathcal{H}, w\models \bot$| never;

• (4) |$\mathcal{H}, w\models \top$| always;

• (5) |$\mathcal{H}, w\models \neg \varphi$| iff not |$\mathcal{H}, w \models \varphi$|⁠;

• (6) |$\mathcal{H}, w\models \varphi\wedge\psi$| iff |$\mathcal{H}, w \models \varphi$| and |$\mathcal{H}, w \models \psi$|⁠;

• (7) |$\mathcal{H}, w\models \varphi\vee\psi$| iff |$\mathcal{H}, w \models \varphi$| or |$\mathcal{H}, w \models \psi$|⁠;

• (8) |$\mathcal{H}, w\models \Diamond\varphi$| iff |$\exists w'\in W(w R w'$| and |$\mathcal{H}, w'\models \varphi)$|⁠;

• (9) |$\mathcal{H}, w\models \Box\varphi$| iff |$\forall w'\in W(w R w' \Rightarrow \mathcal{H}, w'\models \varphi)$|⁠;

• (10) |$\mathcal{H}, w\models @_i \varphi$| iff |$\mathcal{H}, w'\models \varphi$|⁠, where |$w'=N(i)$|⁠.

If |$\mathcal{H}, w\models \varphi$| we say that |$\varphi$| is satisfied in|$\mathcal{H}$| at |$w$|⁠. If |$\varphi$| is satisfied at all states in a structure |$\mathcal{H}$|⁠, we write |$\mathcal{H}\models \varphi$|⁠. If |$\varphi$| is satisfied at all states in all structures based on a frame |$\mathcal{F}$|⁠, then we say that |$\varphi$| is valid on|$\mathcal{F}$| and we write |$\mathcal{F}\models\varphi$|⁠. If |$\varphi$| is valid on all frames, then we simply say that |$\varphi$| is valid and we write |$\models\varphi$|⁠. For |$\Delta\subseteq\mathrm{Form}_@(L)$|⁠, we say that |$\mathcal{H}$| is a model of |$\Delta$| iff for all |$\theta\in\Delta \mathcal{H}\models\theta$|⁠.

It is easy to see that boolean connectives have the usual properties, and that |$\Box\varphi$| is equivalent to |$\neg\Diamond\neg\varphi$|⁠.

 

Definition 2.5

A formula |$\varphi^*\in \mathrm{Form}_@(L)$| is said to be (logically) equivalent to|$\varphi\in \mathrm{Form}_@(L)$| iff for every hybrid structure |$\mathcal{H}=(W, R, N, V)$|⁠, for all |$w\in W$|⁠,

$$\mathcal{H},w\models \phi \iff \mathcal{H},w\models {\phi }^{\ast }.$$

We should point out that this notion of equivalence satisfies the replacement property. This fact will be important later, in the proof of Proposition 3.2.

Next lemma states some properties about the satisfaction operator that will be important in the sequel.

 

Lemma 2.6

Let |$\varphi, \psi$| be hybrid formulas. Then,

• (1) |$@_i(\varphi\vee\psi)$| is equivalent to |$@_i\varphi\vee @_i\psi$|⁠;

• (2) |$@_i(\varphi\wedge\psi)$| is equivalent to |$@_i\varphi\wedge @_i\psi$|⁠;

• (3) |$@_i@_j\varphi$| is equivalent to |$@_j\varphi$|⁠;

• (4) |$\neg@_i\varphi$| is equivalent to |$@_i\neg\varphi$|⁠;

• (5) |$@_i(\varphi_1\wedge\psi_1)\vee @_i(\varphi_2\wedge\psi_2)$| is equivalent to |$(@_i\varphi_1\vee@_i\varphi_2)\wedge(@_i\varphi_1\vee@_i\psi_2)\wedge(@_i\psi_1\vee@_i\varphi_2)\wedge (@_i\psi_1\vee@_i\psi_2) $|⁠.

2.2 Hybrid diagrams

In order to define the diagram of a hybrid structure , we have to define first the concept of literal.

 

Definition 2.7

For a hybrid similarity type |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$|⁠, we define

• (1) |$Hybrid\ atoms$| over |$L$|⁠:

  |$\mathrm{HAt}(L)=\{@_i p,\ @_i j,\ @_i\Diamond j\ |1, j\in \mathrm{Nom}, p\in \mathrm{Prop} \}$|

• (2) |$Hybrid\ literals$| over |$L$|⁠:

  |$\mathrm{HLit}(L)=\{ @_i p,\ @_i\neg p,\ @_i j,\ @_i\neg j, @_i\Diamond j,\ @_i\Box\neg j\ |\ i, j\in \mathrm{Nom}, p\in \mathrm{Prop} \}$|⁠.

An important feature of hybrid logic is the fact that we can specify Robinson diagrams [7]. As in first-order logic, in order to define the diagram of a hybrid structure, we expand the hybrid similarity type |$L$| by adding new nominals for the elements of the domain |$W$|⁠. We write |$L(W)$| for this new hybrid similarity type; in other words, |$L(W)=\langle \mathrm{Prop}, \mathrm{Nom} \cup W \rangle$|⁠.

Given a hybrid structure |$\mathcal{H}=(W, R, N, V)$| over |$L$|⁠, we denote by |$\mathcal{H}(W)$| the natural expansion of |$\mathcal{H}$| to |$L(W)$| by taking |$N$| the identity on the new symbols.

The diagram of a hybrid structure |$\mathcal{H}$| over |$L$| is the set of literals over |$L(W)$| that are valid in |$\mathcal{H}(W)$|⁠. Formally,

 

Definition 2.8

For a hybrid similarity type, |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$|⁠, and a hybrid structure over |$L$|⁠, |$\mathcal{H}=(W, R, N, V)$|⁠, the elementary diagram of|$\mathcal{H}$|⁠, |$diag(\mathcal{H})$|⁠, is the set of hybrid literals over |$L(W)$| that hold in |$\mathcal{H}(W)$|⁠, i.e.

$$\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(\mathcal{H})=\{\alpha \in \mathrm{H}\mathrm{L}\mathrm{i}\mathrm{t}(L(W))|\mathcal{H}(W)\models \alpha \}.$$

Actually, |${\rm diag}(\mathcal{H})$| behaves like the standard diagram for first-order logic:

 

Theorem 2.9

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type, |$\mathcal{H}=(W, R, N, V),$| and |$\mathcal{H}'=(W', R', N', V')$| be two hybrid structures over |$L$|⁠. Then, there is an embedding from |$\mathcal{H}$| to |$\mathcal{H}'$| iff |$\mathcal{H}'$| can be expanded to a model of |$diag(\mathcal{H})$|⁠.

 

Proof

Let |$h$| be an embedding from |$\mathcal{H}$| to |$\mathcal{H}'$|⁠.

Define the expansion |$\mathcal{H}'^h=(W', R', N'^h, V')$| of |$\mathcal{H}'$| to |$L(W)$| by extending |$N$| to |$\mathrm{Nom} \cup W$| by |$N'^h(w)=h(w)$| for |$w\in W$|⁠. It is not hard to show that |$\mathcal{H}'^h$| is a model of the diagram of |$\mathcal{H}$|⁠.

Conversely, let |$\overline{\mathcal{H}'}=(W',R', \bar N,V')$| be an expansion of |$\mathcal{H}'$| to |$L(W)$| which is a model of the diagram of |$\mathcal{H}$|⁠. Define the map |$h:W\rightarrow W'$| by |$h(w)=\bar N(w)$|⁠. Clearly, |$h$| is injective. Moreover, it is not difficult to see that |$h$| is a homomorphism. Hence, it is an embedding. ■

 

Example 1

Let |$L=\langle \{p, q\}, \{\}\rangle$|⁠, and |$W=\{u, v, w\}$|⁠.

Consider the hybrid structure |$\mathcal{H}$| represented in Figure 1.

The diagram of |$\mathcal{H}$| is given by:

$$\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(\mathcal{H})=\{{@}_{u}p,{@}_u\mathrm{\neg }q,{@}_v\mathrm{\neg }p,{@}_{v}q,{@}_{w}p,{@}_{w}q,$$

$${@}_{u}u,{@}_{v}v,{@}_{w}w,$$

$${@}_u\mathrm{\neg }v,{@}_u\mathrm{\neg }w,{@}_v\mathrm{\neg }u,{@}_v\mathrm{\neg }w,{@}_w\mathrm{\neg }u,{@}_w\mathrm{\neg }v,$$

$${@}_u◊v,{@}_u◻\mathrm{\neg }u,{@}_u◻\mathrm{\neg }w,{@}_v◊w,{@}_v◻\mathrm{\neg }u,$$

$${@}_v◻\mathrm{\neg }w,{@}_w◻\mathrm{\neg }u,{@}_w◻\mathrm{\neg }v,{@}_w◻\mathrm{\neg }w\}.$$

Figure 1.

A hybrid structure.

2.3 Bisimulation

In this section, we recall the notion of bisimulation of hybrid structures, sometimes called bisimulation with constants.

 

Definition 2.10

(Bisimulation) Let |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type. Let |$\mathcal{H}=(W, R, N,V)$| and |$\mathcal{H}'=(W', R',N', V')$| be two hybrid structures. A bisimulation between |$\mathcal{H}$| and |$\mathcal{H}'$| is a non-empty relation |$Z\subseteq W\times W'$| such that:

• all points named by nominals are related by |$Z$|⁠, i.e. for each |$i\in \mathrm{Nom}$||$N(i) Z N'(i)$|⁠;

• for every pair |$(w,w')\in Z$| we have:

  • – Atomic conditions:

    • * |$w\in V(p)$| iff |$w'\in V'(p)$|⁠, for all |$p\in \mathrm{Prop}$|⁠.

    • * for all |$ i\in \mathrm{Nom} ,\; N(i)=w$| iff |$N'(i)=w'$|⁠.

  • – if |$ w R u$| for some |$u \in W$|⁠, then there is some |$u'\in W'$| such that |$w' R' u'$| and |$u Z u'$|(Zig),

  • – Similarly, in the opposite direction: if |$w' R' u'$| for some |$u' \in W'$|⁠, then there is some |$u\in W$| such that |$w R u$| and |$u Z u'$|(Zag).

Two pointed hybrid structures, |$(\mathcal{H}, w)$| and |$(\mathcal{H}', w')$|⁠, are bisimilar if there is a bisimulation |$Z$| between |$\mathcal{H}$| and |$\mathcal{H}'$| such that |$w Z w'$|⁠.

It is well known that modal satisfaction is invariant under bisimulation.

 

Theorem 2.11

([27]) Hybrid logic is invariant under bisimulation: let |$L$| be a hybrid similarity type; if two pointed hybrid structures |$(\mathcal{H}, w)$| and |$(\mathcal{H}', w')$| are bisimilar, then for any |$\varphi\in \mathrm{Form}_@(L)$|⁠,

$$(\mathcal{H},w)\models \phi \text{\hspace{0.5em}iff\hspace{0.5em}}({\mathcal{H}}^{\prime },w^{\prime })\models \phi .$$

3 Paraconsistency in Hybrid Logic

In this section, we study paraconsistency in Hybrid logic following an approach inspired by the work of Grant and Hunter [19, 20]. First of all, we define a Quasi-hybrid (⁠|$\mathrm{QH}$|⁠) Basic Logic. Analogously to the assumption in [19], where it is assumed that all formulas are in prenex conjunctive normal form, we will assume that all formulas are in negation normal form. This assumption does not lead to loss of generality since in Proposition 3.2 we show that any hybrid formula is equivalent to a formula in negation normal form.

Concepts of bistructure, decoupled and strong satisfaction and |$\mathrm{QH}$| model will be presented. We define the paraconsistent diagram of a bistructure and we prove a very important theorem concerning the construction of |$\mathrm{QH}$| models, which are sets of QH literals, whose definition will also be introduced. Afterwards, we consider minimal |$\mathrm{QH}$| models and we present some examples with illustrations.

The inconsistency measure, the central goal of this article, is introduced and, consequently, the notion of preferred |$\mathrm{QH}$| model appears. We define the extrinsic and intrinsic inconsistency for preferred |$\mathrm{QH}$| models, and we present some analogous results to the ones in [19].

3.1 |$\mathrm{QH}$| basic logic

In order to generalize the approach in [19] to the hybrid case, we have to consider formulas in negation normal form (i.e. formulas in which the negation symbol occurs immediately before propositional symbols and/or nominals).

We define the notion of negation normal form for hybrid logic and we establish an analogous result to the one in [10] for classical propositional logic that states that any modal formula is logically equivalent to one in the negation normal form; we would also like to point out that the same result was presented without proof in [17] for the modal case. Therefore, we can restrict our attention to formulas in negation normal form.

 

Definition 3.1

Let |$L=\langle\mathrm{Prop},\mathrm{Nom}\rangle$| be a hybrid similarity type. The negation normal form of a formula, for short |$\mathrm{NNF}$|⁠, is defined just as in propositional logic: a formula is said to be in |$\mathrm{NNF}$| if negation only appears directly before propositional variables and/or nominals. The set of |$\mathrm{NNF}$| formulas over |$L$|⁠, |$\mathrm{Form}_{\mathrm{NNF}(@)}(L)$|⁠, is recursively defined as follows:

For |$p\in\mathrm{Prop},\ i\in\mathrm{Nom}$|⁠,

• (1) |$\bot, \top$| are in |$\mathrm{NNF}$|⁠;

• (2) |$p,\ i,\ \neg p,\ \neg i$| are in |$\mathrm{NNF}$|⁠;

• (3) if |$\varphi,\ \psi$| are formulas in |$\mathrm{NNF}$|⁠, then |$\varphi\vee\psi,\ \varphi\wedge\psi$| are in |$\mathrm{NNF}$|⁠;

• (4) if |$\varphi$| is in |$\mathrm{NNF}$|⁠, then |$\Box\varphi,\ \Diamond\varphi$| are in |$\mathrm{NNF}$|⁠;

• (5) if |$\varphi$| is in |$\mathrm{NNF}$|⁠, then |$@_i\varphi$| is in |$\mathrm{NNF}$|⁠.

The next proposition states that we can consider only formulas in negation normal form.

 

Proposition 3.2

Every formula |$\varphi\in \mathrm{Form}_@(L)$| is logically equivalent to a formula |$\varphi^*\in \mathrm{Form}_{\mathrm{NNF}(@)}(L)$|⁠.

 

Proof

The proof is by induction on the complexity of |$\varphi$|⁠. The base step is trivial, since an atomic formula is already in negation normal form. The cases of conjunctions, disjunctions and the |$\{\Box,\Diamond, @\}$|-prefixed formulas are also trivial.

The non-trivial case is to prove that if |$A$| is equivalent to the negation normal form |$A^*$| then |$\neg A$| is equivalent to some negation normal form |$A^\dagger$|⁠. This divides into seven subcases according to the form of |$A^*$|⁠. The case where |$A^*$| is atomic is trivial, since we may simply let |$A^\dagger$| be |$\neg A^*$|⁠. In case |$A^*$| is of form |$\neg B$|⁠, so |$\neg A^*$| is |$\neg\neg B$|⁠, we may let |$A^\dagger$| be B. In case |$A^*$| is of form |$B\vee C$|⁠, so |$\neg A^*$| is |$\neg(B\vee C)$|⁠, which is logically equivalent to |$(\neg B\wedge\neg C)$|⁠, by the induction hypothesis the simpler formulas |$\neg B$| and |$\neg C$| are equivalent to formulas |$B^\dagger$| and |$C^\dagger$| of the required form, so we may let |$A^\dagger$| be |$(B^\dagger\wedge C^\dagger)$|⁠. The case of conjunction is similar. In case |$A^*$| is of form |$\Diamond B$|⁠, so that |$\neg A^*$| is |$\neg\Diamond B$|⁠, which is logically equivalent to |$\Box\neg B$|⁠, by the induction hypothesis the simpler formula |$\neg B$| is equivalent to a formula |$B^\dagger$| of the required form, so we may let |$A^\dagger$| be |$\Box B^\dagger$|⁠. The case of box is similar. If |$A^*$| is of the form |$@_i B$|⁠, so that |$\neg A^*$| is |$\neg @_i B$|⁠, which is logically equivalent to |$@_i\neg B$|⁠, and since by hypothesis |$\neg B$| is equivalent to a formula |$B^\dagger$| of the required form, then we can conclude that |$A^\dagger$| is |$@_i B^\dagger$|⁠. ■

Based on this proof, a recursive procedure that puts formulas in negation normal form can be formulated. Formally, |$nnf: \mathrm{Form}_@(L)\rightarrow \mathrm{Form}_{\mathrm{NNF}(@)}(L)$| is defined as follows:

• (1) |$nnf(l)\stackrel{\rm def}{=} l, \text{if } l\ \text{ is a literal}$|⁠;

• (2) |$nnf(\psi_1\vee\psi_2)\stackrel{\rm def}{=} nnf(\psi_1)\vee nnf(\psi_2)$|⁠;

• (3) |$nnf(\psi_1\wedge\psi_2)\stackrel{\rm def}{=} nnf(\psi_1)\wedge nnf(\psi_2)$|⁠;

• (4) |$nnf(\neg(\psi_1\vee\psi_2))\stackrel{\rm def}{=} nnf(\neg\psi_1)\wedge nnf(\neg\psi_2)$|⁠;

• (5) |$nnf(\neg(\psi_1\wedge\psi_2))\stackrel{\rm def}{=} nnf(\neg\psi_1)\vee nnf(\neg\psi_2)$|⁠;

• (6) |$nnf(\Box\psi)\stackrel{\rm def}{=} \Box nnf(\psi)$|⁠;

• (7) |$nnf(\neg\Box\psi)\stackrel{\rm def}{=} \Diamond nnf(\neg \psi)$|⁠;

• (8) |$nnf(\Diamond\psi)\stackrel{\rm def}{=} \Diamond nnf(\psi)$|⁠;

• (9) |$nnf(\neg\Diamond\psi)\stackrel{\rm def}{=} \Box nnf(\neg\psi)$|⁠;

• (10) |$nnf(\neg\neg\psi)\stackrel{\rm def}{=} nnf(\psi)$|⁠;

• (11) |$nnf(@_i\psi)\stackrel{\rm def}{=} @_i nnf(\psi)$|⁠;

• (12) |$nnf(\neg @_i\psi)\stackrel{\rm def}{=} @_i nnf(\neg\psi)$|⁠.

Without loss of generality (Theorem 3.2), we will assume that all formulas are in negation normal form, i.e. given a hybrid similarity type |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$|⁠, the set of formulas is |$\mathrm{Form}_{\mathrm{NNF}(@)} (L)$|⁠.

 

Definition 3.3

Let |$\theta$| be a formula in |$\mathrm{NNF}$|⁠. We define the complementation operation |$\sim$| from |$\sim\theta:=nnf(\neg\theta)$|⁠.

The |$\sim$| operator is not part of the object hybrid similarity type but it makes some definitions clearer.

Recall that a hybrid structure for a hybrid similarity type |$L$| is a tuple |$(W, R, N, V)$|⁠. However, in order to accommodate contradictions in a model, we will use two valuations for propositions: |$V^+ $| and |$V^-$|⁠.

 

Definition 3.4

A hybrid bistructure is a tuple |$(W, R, N, V^+, V^-)$|⁠, where |$(W, R, N, V^+)$| and |$(W, R, N, V^-)$| are hybrid structures.

The map |$V^+$| is interpreted as the acceptance of a propositional symbol, and |$V^-$| as the rejection. This is formalized in the definition for decoupled satisfaction.

 

Definition 3.5

For a hybrid bistructure |$E=(W, R, N, V^+, V^-)$| we define a satisfiability relation |$\models_d$| called decoupled satisfaction at |$w\in W$| for propositional symbols and nominals as follows:

• (1) |$E,w\models_d p \ \text{iff} \ w \in V^+(p)$|⁠;

• (2) |$E,w\models_d i \ \text{iff} \ w=N(i)$|⁠;

• (3) |$E,w\models_d \neg p \ \text{iff} \ w \in V^-(p)$|⁠;

• (4) |$E,w\models_d \neg i \ \text{iff} \ w \neq N(i)$|⁠.

Since we allow both a positive and a negative propositional symbol to be satisfiable, we have decoupled, at the level of the structure, the link between a formula and its negation. In contrast, if a classical hybrid structure satisfies a propositional symbol at some world, it is forced to not satisfy its negation at that world.

This decoupling gives us the basis for a semantic for paraconsistent reasoning.

 

Definition 3.6

A satisfiability relation |$\models_s$|⁠, called strong satisfaction, is defined as follows:

• (1) |$E, w \models_s\top$| always;

• (2) |$E, w \models_s\bot$| never;

• (3) |$E, w \models_s p\text{ iff } E, w \models_d p$|⁠;

• (4) |$E, w \models_s \neg p\text{ iff } E, w \models_d \neg p$|⁠;

• (5) |$E, w \models_s i\text{ iff } E, w \models_d i$|⁠;

• (6) |$E, w \models_s \neg i\text{ iff } E, w \models_d \neg i$|⁠;

• (7) |$E, w \models_s \theta_1\vee \theta_2\text{ iff } [E, w \models_s\theta_1\ or\ E, w \models_s \theta_2] \ {\rm and} \ [E, w \models_s \sim\theta_1\Rightarrow E, w \models_s \theta_2]$| and |$[E, w \models_s \sim\theta_2\Rightarrow E, w \models_s \theta_1]$|⁠;

• (8) |$E, w \models_s \theta_1\wedge\theta_2\text{ iff } E, w \models_s \theta_1 \ {\rm and} \ E, w \models_s \theta_2$|⁠;

• (9) |$E, w \models_s \Diamond \theta\text{ iff } \exists w'(wRw'\ \&\ E, w'\models_s \theta)$|⁠;

• (10) |$E, w \models_s \Box \theta\text{ iff } \forall w'(wRw'\Rightarrow E, w' \models_s \theta)$|⁠;

• (11) |$E, w \models_s @_i \theta\text{ iff } E, w' \models_s \theta \ {\rm where} \ w'=N(i)$|⁠.

We define strong validity as follows:

$$E{\models }_s\theta \text{\hspace{0.5em}iff for all\hspace{0.5em}}w\in W,E,w{\models }_s\theta .$$

3.2 |$\mathrm{QH}$| models

Analogously to the definition in the basic hybrid case of a model of a set |$\Delta$| of formulas, we say that a bistructure |$E$| is a |$\mathrm{QH}$|model of |$\Delta$| iff for all |$\theta\in\Delta, E\models_s\theta$|⁠.

To make it easier to follow, we will assume that |$N$| maps nominals to themselves; hence |$W$| will always contain all the nominals in |$L$|⁠. This also means that all nominals are mapped to distinct elements, i.e. |$N$| is an inclusion map. Hence, for a given hybrid similarity type |$L=\langle \mathrm{Prop}, \mathrm{Nom} \rangle$| and a domain |$W$| of a bistructure we must have |$\mathrm{Nom}\subseteq W$|⁠.

As we pointed out before, hybrid logic can specify Robinson diagrams. Following our assumption that |$N$| is injective, in order to define diagrams we do not need the hybrid literals regarding equality between nominals, i.e. |$@_i j$|⁠, |$@_i \neg j$|⁠. Therefore, in this context, we reformulate the notion of atom and literal as follows:

 

Definition 3.7

For a hybrid similarity type |$L=\langle\mathrm{Prop}, \mathrm{Nom}\rangle$|⁠,

• (1) |$\mathrm{QH}$|atoms over|$L$|⁠:

  |$\mathrm{QHAt}(L)=\{@_i p,\ @_i\Diamond j\ |\ i, j\in \mathrm{Nom}, p\in \mathrm{Prop} \}$|⁠;

• (2) |$\mathrm{QH}$|literals over|$ L$|⁠:

  |$\mathrm{QHLit}(L)=\{@_i p,\ @_i\neg p,\ @_i\Diamond j,\ @_i\Box\neg j\ |\ i, j\in \mathrm{Nom}, p\in \mathrm{Prop} \}$|⁠.

To build the paraconsistent diagram, we add new nominals for the elements of |$W$| which are not named yet, and we denote this expanded similarity type by |$L(W)$|⁠, i.e. |$L(W)=\langle \mathrm{Prop}, W\rangle$| (recall that |$\mathrm{Nom}\subseteq W$|⁠). As in the standard case, |$E(W)$| denotes the natural expansion of the bistructure |$E$| to the hybrid similarity type |$L(W)$|⁠, by taking |$N$| the identity for the new nominals. Moreover, we will assume that |$\mathrm{Prop}$| and |$\mathrm{Nom}$| are finite sets for any hybrid similarity type |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$|⁠, as well as the domain |$W$| of any bistructure.

 

Definition 3.8

Let |$L=\langle\mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type, and |$E=(W, R, N, V^+,V^-)$| be a hybrid bistructure over |$L$|⁠. The elementary paraconsistent diagram of|$E$|⁠, denoted by |${\rm Pdiag}(E)$|⁠, is the set of QH literals over |$L(W)$| that hold in |$E(W)$|⁠, i.e.

$$\mathrm{P}\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{g}(E)=\{\alpha \in \mathrm{Q}\mathrm{H}\mathrm{L}\mathrm{i}\mathrm{t}(L(W))|E(W){\models }_s\alpha \}.$$

The paraconsistent diagram |${\rm Pdiag}(E)$| defines the bistructure |$E$| in the sense that two distinct bistructures over |$L$|⁠, with the same domain |$W$| and |$N$|⁠, induce two distinct paraconsistent diagrams (over |$L(W)$|⁠). Therefore, in the sequel, we will represent a (finite) bistructure |$E=(W, R, N, V^+, V^-)$| by its (finite) paraconsistent diagram |${\rm Pdiag}(E)$|⁠. This syntactic representation will play an important role throughout this article.

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type, |$\Delta\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| and |$W$| a finite set. We write |$\mathrm{QH}(L,\Delta, W)$| to denote the set of representations (i.e. paraconsistent diagrams) of hybrid bistructures that are models of |$\Delta$| with domain |$W$|⁠. Recall that the domain and the hybrid similarity type are considered to be finite. This implies that the bistructures are finite and consequently the representations of |$\mathrm{QH}$| models are also finite. This fact is relevant in the next section when discussing the measure of inconsistency of a model.

The syntactic representations of models will be denoted by |$\mathcal{M}$|⁠, |$\mathcal{M}_1$|⁠, etc. Let |$\mathcal{M}$| be the representation of |$E$| with domain |$W$|⁠. For |$w\in W$|⁠, we write |$\mathcal{M},w\models_s\varphi$| if |$E,w\models_s\varphi$|⁠. Analogously, we write |$\mathcal{M}\models_s\varphi$| if |$E\models_s\varphi$|⁠.

3.3 Construction of syntactic |$\mathrm{QH}$| models

In order to make it easier to construct |$\mathrm{QH}$| models as sets of QH literals, we will prove some properties about the satisfaction operator, and we will introduce a very important theorem which will make it possible to use only QH literals when transforming a formula in negation normal form into a quasi-equivalent positive boolean combination of |$\mathrm{QH}$|-literals.

 

Definition 3.9

A formula |$\varphi^*\in\operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| is said to be quasi-equivalent to a formula |$\varphi\in \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$|⁠, denoted |$\varphi\equiv_q \varphi^*$|⁠, iff for all hybrid bistructure |$E=(W, R, N, V^+,V^-)$| and any |$w\in W$|⁠,

$$E,w{\models }_s\phi \iff E,w{\models }_s{\phi }^{\ast }.$$

We now present some properties of the satisfaction operator in QH logic:

 

Lemma 3.10

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type, and |$\varphi, \psi\in \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| be hybrid formulas in negation normal form. Then,

• (1) |$@_i(\varphi\vee\psi)\equiv_q @_i\varphi\vee @_i\psi$|⁠;

• (2) |$@_i(\varphi\wedge\psi)\equiv_q @_i\varphi\wedge @_i\psi$|⁠;

• (3) |$@_i@_j\varphi\equiv_q @_j\varphi$|⁠;

• (4) |$\neg@_i\varphi\equiv_q @_i\neg\varphi$|⁠.

 

Proof

(1) Let |$E$| be an arbitrary bistructure, and |$w$| be an arbitrary world in |$E$|⁠:

$\begin{array}{rcl} E, w\models_s @_i(\varphi\vee\psi) & \Leftrightarrow & E, w'\models_s \varphi\vee\psi, w'=N(i)\\ & \Leftrightarrow & [E, w'\models_s \varphi\ {\rm or}\ E, w'\models_s\psi]\\ & & {\rm and}\ [E, w'\models_s nnf(\neg\varphi) \Rightarrow E, w'\models_s \psi]\\ & &{\rm and}\ [E, w'\models_s nnf(\neg\psi) \Rightarrow E, w'\models_s \varphi], w'=N(i)\\ & \Leftrightarrow & [E, w\models_s @_i\varphi\ {\rm or} \ E, w\models_s @_i\psi]\\ & &{\rm and}\ [E, w\models_s @_i(nnf(\neg\varphi)) \Rightarrow E, w\models_s @_i\psi]\\ & &{\rm and}\ [E, w\models_s @_i(nnf(\neg\psi))\Rightarrow E, w\models_s @_i\varphi]\\ & \Leftrightarrow & [E, w\models_s @_i\varphi\ {\rm or}\ E, w\models_s @_i\psi]\\ & & {\rm and}\ [E, w\models_s nnf(\neg(@_i \varphi)) \Rightarrow E, w\models_s @_i\psi]\\ & & {\rm and}\ [E, w\models_s nnf(\neg(@_i \psi)) \Rightarrow E, w\models_s @_i\varphi]\\ & \Leftrightarrow & E, w\models_s @_i\varphi \vee @_i\psi \end{array}$

■

The distributive law does not hold as shown in the following example.

 

Example 2

Let |$L=\langle\{p, q, r\}, \{i\}\rangle$| be a hybrid similarity type. Consider the bistructure |$E$|⁠, with domain |$W=\{i\}$|⁠, |$R=\emptyset$| and the valuation |$V$| defined by |$V^+(p)=\emptyset, V^-(p)=\{i\}, V^+(q)=V^-(q)=\{ i\}, V^+(r)=\{i\}, V^-(r)=\emptyset$|⁠.

Clearly, the formula |$@_i p \vee (@_i q\wedge @_i r)$| is valid in |$E$|⁠. However, the formula |$(@_i p \vee @_i q) \wedge (@_i p \vee @_i r)$| is not valid in |$E$|⁠. This shows that in QH logic the distributive law does not hold.

The following theorem is very important to construct the representation of hybrid bistructures using QH literals:

 

Theorem 3.11

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type, and |$\mathcal{M}$| be the representation of a finite hybrid bistructure over |$L$| with domain |$W$|⁠. Then for each formula |$\varphi\in \mathrm{Form}_{\mathrm{NNF}(@)}{L}$|⁠, there is a positive boolean combination of QH literals |$\bar \varphi$| over |$L(W)$| such that

$$\mathcal{M}{\models }_s\phi \iff \mathcal{M}{\models }_s\overline{\phi }.$$

 

Proof

We start by noticing that for a |$\mathrm{QH}$| model with finite domain |$W=\{i_1, i_2, ..., i_n\}$| we have

$$\mathcal{M}{\models }_s\phi \iff \mathcal{M}{\models }_s{@}_{i_1}\phi \wedge {@}_{i_2}\phi \wedge ...\wedge {@}_{i_n}\phi .$$

Since the conjunction of positive boolean combinations of QH literals remains a positive boolean combination of QH literals, the proof follows by defining a procedure to transform any formula |$@_{i_*} \varphi$| in a quasi-equivalent positive boolean combination of QH literals, PBCL for short.

• if |$\varphi=p, @_{i_*} p$| is a PBCL;

• if |$\varphi=\neg p, @_{i_*} \neg p$| is a PBCL;

• if |$\varphi=i, @_{i_*} i$| is quasi-equivalent to

  $\left\{ \begin{array}{ll} \top , & \hbox{ if } i=i_*\\ \bot, & \hbox{if } i\neq i_* \end{array} \right.$
  which is a PBCL.

• if |$\varphi= \neg i, @_{i_*} \neg i$| is quasi-equivalent to

  $\left\{ \begin{array}{ll} \top , & \hbox{ if } i\neq i_*\\ \bot, & \hbox{if } i = i_* \end{array} \right.$
  which is a PBCL.

For the induction step, suppose that |$@_{i_*}\phi, @_{i_*}\psi$| are equivalent to PBCL formulas,

• if |$\varphi=\phi\vee\psi$|⁠, |$@_{i_*} \phi\vee\psi$| is quasi-equivalent to |$@_{i_*} \phi\vee @_{i_*}\psi$| which by Ind. Hyp. is quasi-equivalent to a PBCL;

• if |$\varphi=\phi\wedge\psi$|⁠, |$@_{i_*} \phi\wedge\psi$| is quasi-equivalent to |$@_{i_*} \phi\wedge @_{i_*}\psi$| which by Ind. Hyp. is quasi-equivalent to a PBCL;

• if |$\varphi=\Box\phi$|⁠, |$@_{i_*} \Box\phi$| is quasi-equivalent to |$(@_{i_*}\Box\neg i_1\vee@_{i_1}\phi)\wedge(@_{i_*}\Box\neg i_2\vee@_{i_2}\phi)\wedge...\wedge(@_{i_*}\Box\neg i_n\vee@_{i_n}\phi)$| which by Ind. Hyp. is quasi-equivalent to a PBCL;

• if |$\varphi=\Diamond\phi$|⁠, |$@_{i_*} \Diamond\phi$| is quasi-equivalent to |$(@_{i_*}\Diamond i_1\wedge@_{i_1}\phi)\vee(@_{i_*}\Diamond i_2\wedge@_{i_2}\phi)\vee...\vee(@_{i_*}\Diamond i_n\wedge@_{i_n}\phi)$| which by Ind. Hyp. is quasi-equivalent to a PBCL;

• if |$\varphi=@_{i_k}\phi$|⁠, |$@_{i_*} @_{i_k}\phi$| is quasi-equivalent to |$@_{i_k}\phi$| which by Ind. Hyp. is quasi-equivalent to a PBCL.

■

This theorem will be very useful when determining |$\mathrm{QH}$| models. As we have already pointed out, we can represent bistructures by the QH literals that are true there. Therefore, we will consider models to be representations of bistructures and consequently, we will want to build models as sets of QH literals. So, for a given set |$\Delta$|⁠, to make it easier to construct models in that desired form, we apply this theorem to each formula in |$\Delta$|⁠.

3.3.1 Minimal |$\mathrm{QH}$| models

The next definition will be the basis to prove that we can deal only with models with the least number of elements:

 

Definition 3.12

Let |$L$| be a hybrid similarity type. For a set |$K$| of |$\mathrm{QH}$| models, the set of satisfied literals in |$K$| is the set |${\it SLit}(K)$| defined as follows:

$$\mathrm{S}\mathrm{L}\mathrm{i}\mathrm{t}(K)=\{\alpha \in \mathrm{Q}\mathrm{H}\mathrm{L}\mathrm{i}\mathrm{t}(L(W))|\mathrm{\forall }\mathcal{M}\in K,\mathcal{M}{\models }_s\alpha \}.$$

Since different hybrid similarity types contain different sets of formulas, it will be useful to have |$L$| as a parameter when we discuss concepts about models. Also, we will assume that |$\Delta$| is a set of formulas of |$L$|⁠. The domain is also important and we consider it as a parameter.

Models with the least number of elements are now defined:

 

Definition 3.13

Let |$L$| be a hybrid similarity type, |$\Delta\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| and |$W$| be a non-empty set. The set of minimal |$\mathrm{QH}$| models of |$\Delta$| with domain |$W$| is the set |$\mathrm{MQH}(L,\Delta,W)$|⁠, defined as:

$$\mathrm{M}\mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W)=\{\mathcal{M}\in \mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W)|\text{\hspace{0.5em}\hspace{0.5em}if\hspace{0.5em}\hspace{0.5em}}{\mathcal{M}}^{\prime }\subset \mathcal{M}\text{\hspace{0.5em}\hspace{0.5em}then\hspace{0.5em}\hspace{0.5em}}{\mathcal{M}}^{\prime }\notin \mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W)\}$$

Clearly, every |$\mathrm{QH}$| model contains a minimal |$\mathrm{QH}$| model, i.e. for all |$\mathrm{QH}$| model |$\mathcal{M}_1$|⁠, there is a minimal |$\mathrm{QH}$| model |$\mathcal{M}_2$| such that |$\mathcal{M}_2\subseteq\mathcal{M}_1$|⁠.

It is not difficult to see that, if a variable |$p\in \mathrm{Prop}$| does not occur in |$\Delta$| then, |$p$| also does not occur in any model |$\mathcal{M}\in \mathrm{MQH}(L,\Delta,W)$|⁠.

Minimal |$\mathrm{QH}$| models are just models without irrelevant and useless information, according to the next theorem:

 

Theorem 3.14

Let |$L$| be a hybrid similarity type, |$\Delta\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| and |$W$| a non-empty set. Then

$$\mathrm{S}\mathrm{L}\mathrm{i}\mathrm{t}(\mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W))=\mathrm{S}\mathrm{L}\mathrm{i}\mathrm{t}(\mathrm{M}\mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W))$$

 

Proof

Since |$\mathrm{MQH}(L,\Delta,W)\subseteq \mathrm{QH}(L,\Delta,W)$|⁠, by the Galois connection, we have that |$\mathrm{SLit}(\mathrm{QH}(L,\Delta,W))\subseteq \mathrm{SLit}(\mathrm{MQH}(L,\Delta,W))$|⁠.

To prove the other inclusion, let |$\varphi\in \mathrm{SLit}(\mathrm{MQH}(L,\Delta,W))$|⁠. So, |$\mathcal{M}_i\models_s\varphi$|⁠, for all |$\mathcal{M}_i\in \mathrm{MQH}(L, \Delta, W)$|⁠.

For all |$\mathcal{M}_j'\in \mathrm{QH}(L,\Delta, W)$|⁠, there is a subset |$\mathcal{N}_j\subseteq \mathrm{QHLit}(L(W))$| and a model |$\mathcal{M}_i\in \mathrm{MQH}(L,\Delta, W)$| such that |$\mathcal{M}_i\cup \mathcal{N}_j=\mathcal{M}_j'$|⁠. Since |$\mathcal{M}_i\models_s\varphi$|⁠, for all |$\mathcal{M}_i\in \mathrm{MQH}(L, \Delta, W)$|⁠, then |$\mathcal{M}_i\cup \mathcal{N}_j\models_s\varphi$|⁠, for all |$\mathcal{M}_i\in \mathrm{MQH}(L, \Delta, W)$| and any |$ \mathcal{N}_j\subseteq \mathrm{QHLit}(L(W))$|⁠. So, |$\mathcal{M}_j'\models_s\varphi$|⁠, for all |$\mathcal{M}_j'\in \mathrm{QH}(L,\Delta, W)$|⁠. Therefore, |$\mathrm{SLit}(\mathrm{MQH}(L,\Delta,W))\subseteq {\rm SLit}(\mathrm{QH}(L,\Delta,W))$|⁠.

Thus, |$\mathrm{SLit}(\mathrm{QH}(L,\Delta,W))=\mathrm{SLit}(\mathrm{MQH}(L,\Delta,W))$|⁠. ■

The previous theorem does not hold if we consider all satisfied formulas, say |${\rm SForm}(K)$|⁠, instead of only satisfied literals. We would have the following counter-example:

 

Example 3

Let |$L=(\{p, q, r\},\{i, j\})$|⁠, |$W=\{i, j\}$| and |$\Delta=\{ @_i p\vee @_i q, @_i\neg p\vee@_i\neg q, @_j r\}$|⁠.

The two minimal |$\mathrm{QH}$| models of |$\Delta$| are:

|$\mathcal{M}_1=\{@_i p, @_i\neg q, @_j r \}$|⁠;

|$\mathcal{M}_2=\{@_i q, @_i\neg p, @_j r \}$|⁠.

It is easy to see that:

|$@_i r\vee @_j r\in \mathrm{SForm}(\mathrm{MQH}(L,\Delta, W))$|⁠.

However, |$@_i r\vee @_j r \notin \mathrm{SForm}(\mathrm{QH}(L,\Delta, W))$|⁠. In fact, if we consider the model |$\mathcal{M}=\{@_i p, @_i\neg q, @_j r, @_j\neg r \}$|⁠, we have that |$\mathcal{M} \nvDash_s @_i r\vee @_j r$| (this happens because |$\ \mathcal{M} \models_s \neg @_j r$| implies that |$\mathcal{M}$| would have to satisfy |$@_i r$|⁠, which is false). Thus, |$\mathrm{SForm}(\mathrm{MQH}(L,\Delta, W))\nsubseteq \mathrm{SForm}(\mathrm{QH}(L,\Delta, W))$|⁠.

Next we will present several examples that illustrate how to build models (which are sets of QH literals) for a set of formulas |$\Delta$|⁠, using Theorem 3.11.

 

Example 4

Let |$L=\langle \{p,q\}, \{i\}\rangle$|⁠, |$W=\{i\}$|⁠, and |$\Delta=\{@_i(p\wedge q),@_i\neg p \}$|⁠.

First, we notice that the formula |$@_i(p\wedge q)$| is quasi-equivalent to |$@_i p\wedge @_i q$|⁠. Hence, any minimal model of |$\Delta$| must contain the set |$\Omega=\{@_i\neg p, @_i q, @_i p\}$|⁠.

Observe that in a minimal model all transitions (or their lack) between states must be specified, hence we have to explore all possible transitions in |$W=\{i\}$|⁠. We have exactly two minimal |$\mathrm{QH}$| models of |$\Delta$|⁠:

|$\mathcal{M}_1=\{@_i\neg p, @_i q,@_i p, @_i\Box\neg i\}$|⁠;

|$\mathcal{M}_2=\{@_i\neg p, @_i q,@_i p, @_i\Diamond i\}$|⁠.

The minimal models |$\mathcal{M}_1$| and |$\mathcal{M}_2$| are represented in Figure 2a, and 2b, respectively.

Figure 2.

Minimal models – Example 4.

In this example, the minimal models have the same number of contradictions. However this is not always the case as we will see below.

 

Example 5

Let |$L=\langle \{p,q\}, \{i, j\}\rangle$|⁠, |$W=\{i, j\}$| and |$\Delta=\{p\vee q,@_i\neg p \}$|⁠.

Not all formulas in |$\Delta$| are PBCLs. Using the properties of the satisfaction operator and the method described in the proof of Theorem 3.11, let us make the necessary adjustments:

$$p\vee q{\equiv }_q({@}_i(p\vee q))\wedge ({@}_j(p\vee q)){\equiv }_q({@}_{i}p\vee {@}_{i}q)\wedge ({@}_{j}p\vee {@}_{j}q).$$

(1)

Since the formula |$@_i\neg p$| is mandatory in every model, from |$(@_i p\vee @_i q)$| follows that |$@_i q$| is mandatory too. The formula |$(@_j p\vee @_j q)$| is going to be split into two, since there is no restriction to which component consider. Hence, any minimal model of |$\Delta$| must contain one of these sets: |$\Omega_1=\{@_i\neg p, @_i q, @_j p\}$| or |$\Omega_2=\{@_i\neg p, @_i q, @_j q\}$|⁠.

As pointed out before, all connections (or lack of them) must be specified in minimal |$\mathrm{QH}$| models. We will leave some examples of minimal |$\mathrm{QH}$| models for the considered similarity type |$L$|⁠, set of formulas |$\Delta$| and domain |$W$|⁠, in a total of |$2^{2\times 2}=2^4=16$| possibilities, by combining QH literals of the form |$@_i\Diamond j, @_i\Box\neg j$|⁠.

We have, for instance, for |$\Omega_1$|⁠:

|$\mathcal{M}_1=\{@_i\neg p, @_i q, @_j p, @_i\Box\neg i, @_i\Box\neg j, @_j\Box\neg i, @_j\Box\neg j\}$|⁠;

|$\mathcal{M}_2=\{@_i\neg p, @_i q, @_j p, @_i\Box\neg i, @_i\Diamond j, @_j\Diamond i, @_j\Box\neg j\}$|⁠.

And for |$\Omega_2$|⁠:

|$\mathcal{M}_3=\{@_i\neg p, @_i q, @_j q, @_i\Box\neg i, @_i\Box\neg j, @_j\Box\neg i, @_j\Box\neg j\}$|⁠;

|$\mathcal{M}_4=\{@_i\neg p, @_i q, @_j q, , @_i\Box\neg i, @_i\Diamond j, @_j\Diamond i, @_j\Box\neg j\}$|⁠.

The minimal models |$\mathcal{M}_1,\mathcal{M}_2,\mathcal{M}_3$| and |$\mathcal{M}_4$| are represented in Figures 3a, 3b, 3c and 3d, respectively.

Figure 3.

Minimal models – Example 5.

 

Example 6

Let |$L=\langle \{p,q\}, \{i, j\}\rangle$|⁠, |$W=\{i, j, k\}$| and |$\Delta=\{@_i(p\wedge q),@_j(\neg p\wedge p)\}$|⁠.

None of the formulas in |$\Delta$| are PBCLs. Let us rearrange it:

• (1) |$@_i(p\wedge q) \equiv_q @_i p\wedge @_i q$|⁠;

• (2) |$@_j(\neg p\wedge p) \equiv_q @_j\neg p\wedge @_j p$|⁠.

The set of formulas that are satisfiable in all minimal |$\mathrm{QH}$| model is: |$\Omega=\{@_i p, @_i q, @_j p, @_j\neg p\}$|⁠.

One minimal model for |$\Delta$| is, e.g.

$ \begin{array}{rll} \mathcal{M}&=&\{@_i p, @_i q, @_j p, @_j\neg p, @_i\Box\neg i, @_i\Box\neg j, @_i\Box\neg k,\\ && @_j\Box\neg i, @_j\Box\neg j, @_j\Box\neg k, @_k\Box\neg i, @_k\Box\neg j, @_k\Box\neg k\}.\\ \end{array} $

The minimal model |$\mathcal{M}$| is represented in Figure 4:

Figure 4.

Minimal model |$\mathcal{M}$| – Example 6.

 

Example 7

Let |$L= \langle\{p\},\{i\}\rangle$|⁠, |$W=\{i\}$| and |$\Delta=\{@_i\Box\neg p, @_i\Box p\}$|⁠.

There are exactly two minimal |$\mathrm{QH}$| models with domain |$W=\{i\}$|⁠, which are:

|$\mathcal{M}_1=\{@_i \Box\neg i\}$|⁠;

|$\mathcal{M}_2=\{@_i \Diamond i, @_i p, @_i \neg p\}$|⁠.

The minimal models |$\mathcal{M}_1$| and |$\mathcal{M}_2$| are represented in Figures 5a and 5b, respectively.

Figure 5.

Minimal models – Example 7.

 

Example 8

Let |$L=\langle \{p,q,r\}, \{i,j\}\rangle$|⁠, |$W=\{i,j\}$| and |$\Delta=\{@_i\Diamond j\vee @_j\Diamond i, @_i\Diamond(p\vee q), @_i\Box q, @_i\Box\neg j, @_i\neg q\}$|⁠.

Some formulas in |$\Delta$| are not written as a PBCL. We will make the necessary adjustments:

• (1) |$@_i\Diamond(p\vee q) \equiv_q @_i\Diamond(p\vee q)\equiv_q (@_i\Diamond i\wedge @_i(p\vee q))\vee(@_i\Diamond j\wedge @_j(p\vee q))$|⁠;

• (2) |$@_i\Box q \equiv_q (@_i\Box\neg i\vee @_i q)\wedge(@_i\Box\neg j\vee @_j q)$|⁠.

There is a set of formulas that are true in every minimal model, which is: |$\Omega=\{@_i\Box\neg j, @_j\Diamond i, @_i\Diamond i, @_i q, @_i\neg q, @_i p\}$|⁠.

Again, although we already have some information about transitions between states, we need to complete it in order to have information about all connections (or their lack) between pairs of states. The only pair left is the pair |$(j, j)$|⁠. We have two possibilities: the connection exists, or it does not.

So, we have the following |$\mathrm{QH}$| minimal models:

|$\mathcal{M}_1=\{@_i\Box\neg j, @_j\Diamond i, @_i\Diamond i, @_i q, @_i\neg q, @_i p, @_j\Diamond j\}$|⁠;

|$\mathcal{M}_2=\{@_i\Box\neg j, @_j\Diamond i, @_i\Diamond i, @_i q, @_i\neg q, @_i p, @_j\Box\neg j\}$|⁠.

The minimal models |$\mathcal{M}_1$| and |$\mathcal{M}_2$| are represented in Figures 6a and 6b, respectively.

Figure 6.

Minimal models – Example 8.

Our interest in using |$\mathrm{MQH}(L,\Delta,W)$| rather than |$\mathrm{QH}(L,\Delta,W)$|⁠, for a set of formulas |$\Delta$|⁠, is that the models in |$\mathrm{MQH}(L,\Delta,W)$| do not contain irrelevant information for analysing inconsistency, and we do not lose any useful information.

3.4 The inconsistency measure

A theory may have different minimal |$\mathrm{QH}$| models depending on the hybrid similarity type and domain considered. Now we will introduce a way to measure the inconsistency of a |$\mathrm{QH}$| model. This measure is a ratio between 0 and 1 whose numerator is the number of contradictions in the model, and whose denominator is the total possible number of contradictions in the underlying hybrid similarity type.

The measure of inconsistency of a model is crucial in a diverse range of applications in artificial intelligence to compare between knowledge bases. As supported in [21], it may be a useful tool in analysing various information types, such as news reports, software specifications, integrity constraints and e-commerce protocols.

To make the notation in the next definition simpler, we define the set of inconsistency literals over |$L$| and |$W$| as

$$\mathrm{I}\mathrm{L}(L,W)=\{{@}_{i}p|i\in W,p\in \mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p}\}.$$

 

Definition 3.15

For a |$\mathrm{QH}$| model |$\mathcal{M}$|⁠,

$$\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}(\mathcal{M})=\{{@}_{i}p\in \mathrm{I}\mathrm{L}(L,W)|{@}_{i}p\in \mathcal{M}\mathrm{\&}{@}_i\mathrm{\neg }p\in \mathcal{M}\}.$$

Our inconsistency measure comes as follows:

 

Definition 3.16

The measure of inconsistency for a model |$\mathcal{M}$| in the context of a hybrid similarity type |$L$| and domain |$W$| is given by the |${\rm ModelInc}$| function, giving a value between 0 and 1, as follows:

$$\mathrm{M}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{I}\mathrm{n}\mathrm{c}(\mathcal{M},L,W)=\frac{|\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}(\mathcal{M})|}{|\mathrm{I}\mathrm{L}(L,W)|}.$$

The |${\rm ModelInc}$| is anti-monotonic in the following sense:

 

Theorem 3.17

Let |$L_1, L_2$| be hybrid similarity types and |$W_1, W_2$| non-empty sets. Then,

• If |$L_1\subseteq L_2$| then |${\rm ModelInc}(\mathcal{M}, L_1, W)\geq {\rm ModelInc}(\mathcal{M}, L_2, W)$|⁠.

• If |$W_1\subseteq W_2$| then |${\rm ModelInc}(\mathcal{M}, L, W_1)\geq {\rm ModelInc}(\mathcal{M}, L, W_2)$|⁠.

 

Example 9

In this example, we will consider again the minimal models presented in Examples 2–6 and we will compute their measures of inconsistency, i.e. the |${\rm ModelInc}$| function.

• (1) From Example 4, |${\rm Conflictbase}(\mathcal{M}_1)=\{@_i p\}$|⁠. Then,

  $$\mathrm{M}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{I}\mathrm{n}\mathrm{c}({\mathcal{M}}_1,L,W)=\frac{|\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}({\mathcal{M}}_1)|}{|\mathrm{I}\mathrm{L}(L,W)|}=\frac{1}{\mathrm{2}}.$$

  The same happens for |$\mathcal{M}_2$|⁠.

• (2) From Example 5, |${\rm Conflictbase}(\mathcal{M}_1)=\{\}$|⁠. Then,

  $$\mathrm{M}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{I}\mathrm{n}\mathrm{c}({\mathcal{M}}_1,L,W)=\frac{|\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}({\mathcal{M}}_1)|}{|\mathrm{I}\mathrm{L}(L,W)|}=\frac{0}{\mathrm{4}}=0.$$

  The same happens for |$\mathcal{M}_2$|⁠, |$\mathcal{M}_3$| and |$\mathcal{M}_4$|⁠.

• (3) From Example 6, |${\rm Conflictbase}(\mathcal{M})=\{@_j p\}$|⁠. Then,

  $$\mathrm{M}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{I}\mathrm{n}\mathrm{c}(\mathcal{M},L,W)=\frac{|\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}(\mathcal{M})|}{|\mathrm{I}\mathrm{L}(L,W)|}=\frac{1}{\mathrm{4}}.$$
• (4) From Example 7, |${\rm Conflictbase}(\mathcal{M}_1)=\{\}$|⁠. Then,

  $$\mathrm{M}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{I}\mathrm{n}\mathrm{c}({\mathcal{M}}_1,L,W)=\frac{|\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}({\mathcal{M}}_1)|}{|\mathrm{I}\mathrm{L}(L,W)|}=\frac{0}{\mathrm{1}}=0.$$
  However, for |$\mathcal{M}_2$|⁠, |${\rm Conflictbase}(\mathcal{M}_2)=\{@_i p\}$|⁠. Hence,

  $$\mathrm{M}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{I}\mathrm{n}\mathrm{c}({\mathcal{M}}_2,L,W)=\frac{|\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}({\mathcal{M}}_1)|}{|\mathrm{I}\mathrm{L}(L,W)|}=\frac{1}{\mathrm{1}}=1.$$
• (5) From Example 8, |${\rm Conflictbase}(\mathcal{M}_1)=\{\}$|⁠. Then,

  $$\mathrm{M}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{I}\mathrm{n}\mathrm{c}({\mathcal{M}}_1,L,W)=\frac{|\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}({\mathcal{M}}_1)|}{|\mathrm{I}\mathrm{L}(L,W)|}=\frac{0}{\mathrm{6}}=0.$$

  The same happens for |$\mathcal{M}_2$|⁠.

An application where the measure of inconsistency has revealed itself useful in the health area has been discussed in [13], and concerns the path of a patient in the health care system, subject to contradictory diagnoses.

3.5 Preferred |$\mathrm{QH}$| models

We saw in Example 7 that minimal models for a certain |$\Delta$|⁠, over the same hybrid similarity type and domain, may have different number of contradictions and consequently the |${\rm ModelInc}$| function takes different values for each model.

In order to consider minimal models with the least number of inconsistencies, we restrict the class of minimal models by considering the so-called class of preferred models which are the ones with a minimal conflict base. This follows the approach of Grant and Hunter in [19]. This idea was already adopted in the context of the minimal four-valued logic [1].

 

Definition 3.18

Let |$L$| be a hybrid similarity type, |$\Delta\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| and |$W$| a non-empty set. The set of preferred |$\mathrm{QH}$| models for |$\Delta$| with domain |$W$| is given by

$$\begin{array}{ccc}\mathrm{P}\mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W)& =& \{\mathcal{M}\in \mathrm{M}\mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W)|\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{a}\mathrm{l}\mathrm{l}{\mathcal{M}}^{\prime }\in \mathrm{M}\mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W),\\ & & |\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}(\mathcal{M})|\le |\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{c}\mathrm{t}\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}({\mathcal{M}}^{\prime })|\}.\hfill \end{array}$$

 

Theorem 3.19

Let |$L$| be a hybrid similarity type, |$\Delta\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| and |$W_1,W_2$| non-empty sets with the same number of elements. If |$\mathcal{M}_1\in \mathrm{PQH}(L,\Delta,W_1)$| and |$\mathcal{M}_2\in \mathrm{PQH}(L,\Delta,W_2)$|⁠, then |${\rm ModelInc}(\mathcal{M}_1, L, W_1)={\rm ModelInc}(\mathcal{M}_2, L, W_2)$|⁠.

 

Proof

Suppose that |$\mathcal{M}_1\in \mathrm{PQH}(L,\Delta,W_1)$|⁠.

We construct a model |$\mathcal{M}_2\in \mathrm{PQH}(L,\Delta,W_2)$| as follows:

• Define a bijective function |$F: W_1\rightarrow W_2$| such that for all |$i\in \mathrm{Nom}, F(i)=i$|⁠.

• Write for each |$\mathrm{QH}$| literal |$\alpha\in L(W)$|⁠, |$F(\alpha)$| for the |$\mathrm{QH}$| literal where each |$i\in W_1$| is replaced by |$F(i)$|⁠.

• Let |$\mathcal{M}_2=\{F(\alpha)\,|\, \alpha\in\mathcal{M}_1\}$|⁠.

Clearly, |$\mathcal{M}_2\in \mathrm{QH}(L,\Delta,W_2)$|⁠. |$\mathcal{M}_2$| must also be minimal because if a proper subset of |$\mathcal{M}_2$| were a |$\mathrm{QH}$| model, by applying |$F^{-1}$| we could obtain a |$\mathrm{QH}$| model with |$W_1$| for the domain, making |$\mathcal{M}_1$| not minimal.

Similarly, we can show that |$\mathcal{M}_2$| is preferred. The result now follows. ■

Now, for a hybrid similarity type |$L$|⁠, we will define the extrinsic inconsistency of a set of formulas |$\Delta$|⁠:

 

Definition 3.10

We define the extrinsic inconsistency of a theory |$\Delta$| in a hybrid similarity type |$L$|⁠, |${\rm TheoryInc}(\Delta, L)$|⁠, as a sequence |$\langle r_1, \dots, r_n,\dots \rangle$|⁠, where for all |$n\geq 1$|⁠,

$$r_n=\{\begin{array}{cc}\mathrm{M}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{I}\mathrm{n}\mathrm{c}(\mathcal{M},L,W_n),& \text{\hspace{0.5em}if there is a model\hspace{0.5em}}\mathcal{M}\in \mathrm{P}\mathrm{Q}\mathrm{H}(L,\mathrm{\Delta },W_n)\\ & \text{\hspace{0.5em}with\hspace{0.5em}}{W}_n\text{\hspace{0.5em}a domain of size\hspace{0.5em}}n;\hfill \\ \ast ,\hfill & \text{otherwise.}\hfill \end{array}\hspace{0.17em}$$

We use |$*$| as a kind of null value.

This sequence captures how the measure of inconsistency of a theory |$\Delta$| in a hybrid similarity type |$L$| evolves with an increasing domain size. At one extreme, there are cases where we do not have contradictions for any domain size; e.g. for the trivial case when |$\Delta=\emptyset$|⁠, |${\rm TheoryInc}(\Delta,L)=\langle 0, 0, ...\rangle$|⁠. At the other extreme, there are theories |$\Delta$| such that |${\rm TheoryInc}(\Delta,L)=\langle 1, 1, ...\rangle$|⁠, such as |$\Delta=\{p\wedge\neg p: \text{for all } p\in \mathrm{Prop}\}$|⁠.

 

Example 10

We leave some examples on the computation of the extrinsic inconsistency of some theories:

• (1) Let |$L=\langle \{p\}, \{i, j\}\rangle$| and |$\Delta=\{@_i \neg p\vee @_j p, @_i p\}$|⁠.

  $$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L)=⟨\ast ,0,0,0,...⟩$$

• (2) Let |$L=\langle \{p,q\}, \{i, j\}\rangle$| and |$\Delta=\{@_i(p\wedge q),@_j(\neg p\wedge p)\}$|⁠.

  $$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L)=⟨\ast ,\frac{1}{\mathrm{4}},\frac{1}{\mathrm{6}},...⟩$$

• (3) Let |$L=\langle \{p\}, \{i\}\rangle$| and |$\Delta=\{@_i p, @_i\neg p\}$|⁠.

  $$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L)=⟨1,\frac{1}{\mathrm{2}},\frac{1}{\mathrm{3}},...⟩$$

• (4) Let |$L=\langle \{p, q\}, \{i, j\}\rangle$| and |$\Delta=\{@_i \neg p, @_j\neg q, p\wedge\neg p\wedge q\}$|⁠.

  $$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L)=⟨\ast ,\frac{3}{\mathrm{4}},\frac{4}{\mathrm{6}},\frac{5}{\mathrm{8}},...⟩$$

• (5) Let |$L=\langle \{p\}, \{i, j\}\rangle$| and |$\Delta=\{i\vee j\}$|⁠.

  $$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L)=⟨\ast ,0,\ast ,\ast ,...⟩$$

Some properties of |${\rm TheoryInc}$| are now announced and proved:

 

Proposition 3.21

Let |$L=\langle \mathrm{Nom}, \mathrm{Prop} \rangle$| be a hybrid similarity type such that |$|\mathrm{Nom}|=k$|⁠, |$\Delta\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| and |${\rm TheoryInc}(\Delta,L)=\langle x_1,x_2,...\rangle$|⁠. Then,

• for all |$i$| such that |$1\leq i< k, x_i=*$|⁠;

• if |$x_{k+1} \neq *$| then for all |$ j> k, x_j\neq * $|⁠.

 

Proof

The reason for the asterisks from |$x_1$| to |$x_{k-1}$| is that the domain, according to our definition, must have at least as many elements as the number of nominals in |$L$|⁠, |$|\mathrm{Nom}|$|⁠.

Suppose now that |$x_{k+1} \neq *$|⁠. Hence, there is a preferred model |$\mathcal{M}$| of |$\Delta$| with domain |$W$| which has |$k+1$| elements.

Let |$u$| be a new element not in |$W$|⁠, i.e. the element |$k+1$|⁠, and let |$z$| be the element of |$W$| that is not named by a nominal, i.e. the element |$k+2$|⁠. We define a new model |$\mathcal{M}'$| over |$L$| with domain |$W\cup\{u\}$|⁠, which has cardinality |$k+2$|⁠, admitting the following representation:

$$\begin{array}{ccc}& & {\mathcal{M}}^{\prime }=\mathcal{M}\cup \{{@}_u◊w|w\in W,{@}_z◊w\in \mathcal{M}\}\cup \{{@}_w◻\mathrm{\neg }u|w\in W\}\cup \hfill \\ & & \hfill \{{@}_u◻\mathrm{\neg }w|w\in W,{@}_z◻\mathrm{\neg }w\in \mathcal{M}\}\cup \{{@}_{u}p|p\in \mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p},{@}_{z}p\in \mathcal{M}\}\cup \\ & & \{{@}_u\mathrm{\neg }p|p\in \mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p},{@}_z\mathrm{\neg }p\in \mathcal{M}\}.\hfill \end{array}$$

We claim that:

Claim. for all|$\varphi \in \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$|⁠,

• |$\mathcal{M},z\models_s \varphi $| iff |$\mathcal{M}',u \models_s \varphi $| and

• |$\mathcal{M},z\models_s \sim \varphi $| iff |$\mathcal{M}',u \models_s \sim \varphi $|⁠.

In fact, this can be proved by induction. The base step is trivial. The steps for the conjunction, the satisfaction operator and the modal operators are also straightforward. Let us see what happens with the disjunction:

Let |$\varphi:=\varphi_1\vee \varphi_2$|⁠. We assume that the claim is true for formulas shorter than |$\varphi$| (note that a formula |$\psi_1$| is shorter than a formula |$\psi_2$| iff the formula |$\psi_1$| contains less boolean operators than the formula |$\psi_2$|⁠; however, the elements that compose |$\psi_1$| are not necessarily the same elements that compose |$\psi_2$|⁠). Then,

$$\begin{array}{ccc}\hfill \mathcal{M},z\models \phi & iff\hfill & \mathcal{M},z{\models }_s{\phi }_1\vee {\phi }_2\hfill \\ & iff\hfill & \hspace{0.17em}[\mathcal{M},z{\models }_s{\phi }_1\text{\hspace{0.5em}or\hspace{0.5em}}\mathcal{M},z{\models }_s{\phi }_2]\text{\hspace{0.5em}and}\hfill \\ & & \hspace{0.17em}[\mathcal{M},z{\models }_s\sim {\phi }_2\Rightarrow \mathcal{M},z{\models }_s{\phi }_1]\text{\hspace{0.5em}and}\hfill \\ & & \hspace{0.17em}[\mathcal{M},z{\models }_s\sim {\phi }_1\Rightarrow \mathcal{M},z{\models }_s{\phi }_2]\hfill \\ & if{f}^{(\ast )}\hfill & \hspace{0.17em}[{\mathcal{M}}^{\prime },u{\models }_s{\phi }_1\text{\hspace{0.5em}or\hspace{0.5em}}{\mathcal{M}}^{\prime },u{\models }_s{\phi }_2]\text{\hspace{0.5em}and}\hfill \\ & & \hspace{0.17em}[{\mathcal{M}}^{\prime },u{\models }_s\sim {\phi }_1\Rightarrow {\mathcal{M}}^{\prime },u{\models }_s{\phi }_2]\text{\hspace{0.5em}and}\hfill \\ & & \hspace{0.17em}[{\mathcal{M}}^{\prime },u{\models }_s\sim {\phi }_2\Rightarrow {\mathcal{M}}^{\prime },u{\models }_s{\phi }_1]\hfill \end{array}$$

The step (*) is by induction hypothesis.

As a consequence we have that |$\mathcal{M}'\models_s \Delta$|⁠. And consequently |$x_{k+2}\neq *$|⁠.

This argument can be recursively applied. ■

 

Proposition 3.22

Let |$L=\langle \mathrm{Nom}, \mathrm{Prop} \rangle$| be a hybrid similarity type with |$|\mathrm{Nom}|=k$|⁠, |$\Delta\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$| and |${\rm TheoryInc}(\Delta, L)=\langle x_1, x_2,...\rangle$|⁠. If |$x_{k+1}=0$| then for all |$ j> k+1, x_j =0$|⁠.

 

Proof

The same construction used in the previous proposition can also be applied here. The model |$\mathcal{M}'$| obtained has 0 contradictions since |$\mathcal{M}$| has 0 contradictions. ■

We can adopt a lexicographic ordering, denoted by the relation |$\preceq$| over the tuples generated by the |${\rm TheoryInc}$| function

 

Definition 3.23

Let |$L_1$| and |$L_2$| be hybrid similarity types and let |$\Delta_1, \Delta_2 \subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$|⁠. Let |${\rm TheoryInc}(\Delta_1, L_1)=\langle r_1, r_2, ...\rangle$| and |${\rm TheoryInc}(\Delta_2, L_2)=\langle s_1, s_2, ...\rangle$|⁠. We say that |${\rm TheoryInc}(\Delta_1, L_1)\preceq {\rm TheoryInc}(\Delta_2, L_2)$| iff for all |$i\geq 1,\ r_i\leq s_i\ or\ r_i=*\ or\ s_i=*$|⁠.

|${\rm TheoryInc}(\Delta_1, L_1)\prec {\rm TheoryInc}(\Delta_2, L_2)$| abbreviates |${\rm TheoryInc}(\Delta_1, L_1)\preceq {\rm TheoryInc}(\Delta_2, L_2)$| and |${\rm TheoryInc}(\Delta_1, L_1)\neq {\rm TheoryInc}(\Delta_2, L_2)$|⁠.

In case |$L_1=L_2(=L)$| we say that |$\Delta_1$| has smaller than or equal inconsistency as |$\Delta_2$| iff |${\rm TheoryInc}(\Delta_1, L)\preceq {\rm TheoryInc}(\Delta_2, L)$| and we write |$\Delta_1 \leq_{inc}^L \Delta_2$|⁠.

 

Example 11

Let |$L=\langle \{p\}, \{i\}\rangle, \Delta_1=\{@_i p\}$| and |$\Delta_2=\{@_i p, @_i\neg p\}$|⁠.

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}({\mathrm{\Delta }}_1,L)=⟨0,0,0,...⟩$$

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}({\mathrm{\Delta }}_2,L)=⟨\frac{1}{\mathrm{1}},\frac{1}{\mathrm{2}},\frac{1}{\mathrm{3}},...⟩.$$

Then |$\Delta_1 \leq_{inc}^L \Delta_2$|⁠.

 

Proposition 3.24

Let |$L$| be a hybrid similarity type, |$\Delta_1,\Delta_2\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$|⁠. If |$\Delta_1\subseteq\Delta_2$|⁠, then |${\rm TheoryInc}(\Delta_1, L)\preceq {\rm TheoryInc}(\Delta_2, L)$|⁠.

 

Proof

Additional statements may add but cannot subtract contradictions. ■

 

Proposition 3.25

Let |$L_1=\langle \mathrm{Prop}_1, \mathrm{Nom}_1\rangle$|⁠, |$L_2=\langle \mathrm{Prop}_2, \mathrm{Nom}_2\rangle$| and |$\Delta\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} }(L_1)$|⁠. If |$L_1\subseteq L_2$|⁠, i.e. |$\mathrm{Prop}_1\subseteq \mathrm{Prop}_2$| and |$\mathrm{Nom}_1\subseteq \mathrm{Nom}_2$|⁠, then

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L_1)⪯\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L_2).$$

 

Proof

Let |$n$| be such that |$r_n \neq *$|⁠. For a domain |$W_n$|⁠, such that |$|W_n|=n$|⁠, |$\mathrm{IL}( L_1(W_n))\subseteq \mathrm{IL}( L_2(W_n))$|⁠.

The fact that |$\mathrm{Prop}_1\subseteq\mathrm{Prop}_2$| does not interfere with the construction of preferred |$\mathrm{QH}$| models of |$\Delta$|⁠.

By Theorem 3.19, two preferred models for the same set of formulas |$\Delta$| and domain |$W_n$| have the same size of |${\rm Conflictbase}$|⁠.

Hence, for each |$W_n$|⁠, for |$\mathcal{M}_{1, n}\in \mathrm{PQH}(L_1,\Delta,W_n), \mathcal{M}_{2, n}\in \mathrm{PQH}(L_2,\Delta,W_n),$||$ |{\rm Conflictbase}(\mathcal{M}_{1, n})|=|{\rm Conflictbase}(\mathcal{M}_{2, n})|$|⁠.

But the denominator of |${\rm ModelInc}(\mathcal{M}_{1, n}, L_1, W_n), |\mathrm{IL}( L_1(W_n))|$|⁠, is smaller than the denominator of |${\rm ModelInc}(\mathcal{M}_{2, n}, L_2, W_n), |\mathrm{IL}( L_2(W_n))|$|⁠, for all |$W_n$|⁠.

Which means that |${\rm TheoryInc}(\Delta, L_1)\preceq {\rm TheoryInc}(\Delta, L_2)$|⁠. ■

The next example shows that if |$\Delta_1\subseteq\Delta_2$| and |$L_1\subseteq L_2$| then it is not necessarily the case that |${\rm TheoryInc}(\Delta_1, L_1)\preceq {\rm TheoryInc}(\Delta_2, L_2)$|⁠.

 

Example 12

Let

$$L_1=⟨\{p\},\{i\}⟩\text{\hspace{0.5em}\hspace{0.5em}and\hspace{0.5em}\hspace{0.5em}}{\mathrm{\Delta }}_1=\{{@}_{i}p\}$$

$$L_2=⟨\{p\},\{i\}⟩\text{\hspace{0.5em}\hspace{0.5em}and\hspace{0.5em}\hspace{0.5em}}{\mathrm{\Delta }}_2=\{{@}_{i}p,{@}_i\mathrm{\neg }p\}$$

$$L_3=⟨\{p,q\},\{i\}⟩\text{\hspace{0.5em}\hspace{0.5em}and\hspace{0.5em}\hspace{0.5em}}{\mathrm{\Delta }}_3=\{{@}_{i}p,{@}_i\mathrm{\neg }p,{@}_{i}q\}.$$

In this case |$L_1\subseteq L_2\subseteq L_3$| and |$\Delta_1\subseteq\Delta_2\subseteq\Delta_3$|⁠; however,

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}({\mathrm{\Delta }}_1,L_1)\prec \mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}({\mathrm{\Delta }}_2,L_2)$$

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}({\mathrm{\Delta }}_3,L_3)\prec \mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}({\mathrm{\Delta }}_2,L_2).$$

 

Definition 3.26

For |$\Delta_1, \Delta_2\subseteq \mathrm{Form}_{\mathrm{NNF}(@)}(L), \Delta_1$| is |$\mathrm{QH}$|-equivalent to |$\Delta_2$| if, for all |$\mathcal{M}$|⁠, |$\mathcal{M}$| is a |$\mathrm{QH}$| model of |$\Delta_1$| iff |$\mathcal{M}$| is a |$\mathrm{QH}$| model of |$\Delta_2$|⁠.

 

Proposition 3.27

Let |$L$| be a hybrid similarity type, |$\Delta_1,\Delta_2\subseteq \operatorname{\mathrm{Form}_{\mathrm{NNF}(@)} ({\it L}) }$|⁠. If |$\Delta_1$| is |$\mathrm{QH}$|-equivalent to |$\Delta_2$|⁠, then

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}({\mathrm{\Delta }}_1,L)=\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}({\mathrm{\Delta }}_2,L).$$

 

Proof

Since |$\Delta_1$| is |$\mathrm{QH}$|-equivalent to |$\Delta_2$|⁠, any preferred |$\mathrm{QH}$| model |$\mathcal{M}'$| of |$\Delta_1$| is a preferred |$\mathrm{QH}$| model of |$\Delta_2$|⁠.

Therefore, for a fixed domain |$W_n$| we may consider the same preferred model and consequently for all |$n$|⁠, the |$n$|-th element in the sequence |${\rm TheoryInc}(\Delta_1, L)$| and the |$n$|-th element in the sequence |${\rm TheoryInc}(\Delta_2, L)$| are equal. ■

Resembling the definition of extrinsic inconsistency, we introduce the definition of intrinsic inconsistency of a set of formulas |$\Delta$|⁠, for a specific similarity type |$L$| defined with recourse to |$\Delta$|⁠, as follows:

 

Definition 3.28

For a given theory |$\Delta$|⁠, let |$L^\Delta$| be a hybrid similarity type that contains exactly the propositional variables and nominals that occur in |$\Delta$|⁠. We define the intrinsic inconsistency of |$\Delta$|, |${\rm TheoryInc}(\Delta)$|⁠, as:

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta })=\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L^{\mathrm{\Delta }}).$$

So the measure of intrinsic inconsistency of a theory |${\rm TheoryInc}(\Delta)$|⁠, delineates the degree of the theory in its own terms, whereas the extrinsic inconsistency of a theory |${\rm TheoryInc}(\Delta, L)$| delineates the degree of the theory with respect to the hybrid similarity type |$L$|⁠.

 

Example 13

Let |$L=\langle\{p, q, r\}, \{i,j\}\rangle,\Delta=\{@_i p, @_j\neg p, @_i r, @_i\neg r\}$|⁠.

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta },L)=⟨\ast ,\frac{1}{\mathrm{6}},\frac{1}{\mathrm{9}},\frac{1}{\mathrm{12}},...⟩$$

$$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{y}\mathrm{I}\mathrm{n}\mathrm{c}(\mathrm{\Delta })=⟨\ast ,\frac{1}{\mathrm{4}},\frac{1}{\mathrm{6}},\frac{1}{\mathrm{8}},...⟩.$$

When |${\rm TheoryInc}(\Delta_1)\preceq {\rm TheoryInc}(\Delta_2)$|⁠, we say that |$\Delta_1$| has smaller than or equal inconsistency as |$\Delta_2$|⁠.

4 Inconsistency and Bisimulation

We generalize the notion of bisimulation for a hybrid bistructure.

 

Definition 4.1

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type and |$E=(W, R, N, V^+,V^-)$|⁠, |$E'=(W', R', N', V'^+,V'^-)$| be two hybrid bistructures. A relation |$Z\subset W\times W'$| is a paraconsistent bisimulation if |$Z$| is a bisimulation between the hybrid structures |$ {F}=(W, R, N, V^+)$| and |$ {F}'=(W', R', N', V'^+)$| and also a bisimulation between |$ {G}=(W, R, N,V^-)$| and |$ {G}'=(W', R', N', V'^-)$|⁠.

The following proposition reformulates the notion of bisimulation in terms of the representation of bistructures.

 

Proposition 4.2

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type, |$E$|⁠, |$E'$| be two hybrid bistructures and |$\mathcal{M}$| and |$\mathcal{M}'$| their syntactic representations. A relation |$Z\subseteq W\times W'$| is a paraconsistent bisimulation between |$E$| and |$E'$| iff

• for each |$i\in \mathrm{Nom}$|⁠, |$N(i) Z N'(i)$|⁠;

• for every pair |$(w,w')\in Z$| we have:

  • – Atomic conditions:

    • * |$@_w p \in \mathcal{M}$| iff |$@_{w'} p \in \mathcal{M}'$|⁠, for all |$p\in \mathrm{Prop}$|⁠.

    • * |$@_w \neg p \in \mathcal{M}$| iff |$@_{w'} \neg p \in \mathcal{M}'$|⁠, for all |$p\in \mathrm{Prop}$|⁠.

    • * for all |$ i\in \mathrm{Nom} ,\; N(i)=w$| iff |$N'(i)=w'$|⁠.

  • – if |$ @_w \Diamond u \in \mathcal{M}$| for some |$u \in W$|⁠, then there is some |$u'\in W'$| such that |$@_{w'}\Diamond u'\in \mathcal{M}'$| and |$u Z u'$|(Zig),

  • – if |$@_{w'} \Diamond u' \in \mathcal{M}'$| for some |$u' \in W'$|⁠, then there is some |$u\in W$| such that |$@_{w}\Diamond u$| and |$u Z u'$|(Zag).

Two bisimilar bistructures may have different conflict bases. Clearly this is the case when the witness bisimulation is not total or is not surjective. Moreover, these two conditions, together, are not sufficient as it is shown in the following examples:

 

Example 14

The bisimulation represented in Figure 7, although being a total and surjective relation, does not imply the same conflict base in both bistructures.

Figure 7.

Bisimultion 1.

 

Example 15

The bisimulation represented in Figure 8, a surjective function, does not guarantee that the bisimilar bistructures have the same conflict base.

Figure 8.

Bisimulation 2.

 

Example 16

A bisimulation which is a bijective function between bistructures allows us to have always the same conflict base in the bisimilar bistructures. The result is proved below, and an example is represented in Figure 9.

Figure 9.

Bisimulation 3.

Next theorem states that two bisimilar bistructures such that the bisimulation is a bijective bounded morphism have the same conflict base.

 

Theorem 4.3

Let |$L=\langle \mathrm{Prop}, \mathrm{Nom}\rangle$| be a hybrid similarity type, and let |$E=(W, R, N, V^+,V^-)$| and |$E'=(W', R', N', V'^+,V'^-)$| be two hybrid bistructures with |$\mathcal{M}$| and |$\mathcal{M}'$| their representations. If |$E$| and |$E'$| are bisimilar via a bijective function |$Z$|⁠, then |${\rm ModelInc}(\mathcal{M}, L, W) = {\rm ModelInc}(\mathcal{M}', L, W')$|⁠.

 

Proof

A bijective function between |$W$| and |$W'$| means that both have the same cardinality. Moreover, from the atomic conditions in Proposition 4.2, then the conflict bases for each bistructure coincide. ■

5 Conclusions and Further Work

Inconsistency is a pervasive, and unavoidable, topic in data and knowledge management. It manifests itself in several domains ranging from automated reasoning (e.g. in the context of the so-called question-answering systems) to replication of databases and redundancy enforcing of data distributed in the cloud. The recent paradigm of service oriented computing may also become a typical source of inconsistent, or partially consistent data. Main issues addressed in this area concern information integration, data merging and querying mechanisms for inconsistent databases [16], among others.

Almost all previous research was mainly concerned with procedures to detect and remove inconsistencies, rather than with reasoning in the presence of inconsistency. The latter is the topic of this article, as it is also that of [19]. More specifically, we provide a measure of inconsistency for a knowledge base represented by a set of hybrid literals. This allows us to compare between different knowledge bases and evaluate their quality of information thus serving as a guide for an informed choice. This is achieved through the introduction of a QH logic along with the concept of a bistructure. In order to accommodate contradictions, the satisfaction relation is decoupled. Similar to the method of diagrams in hybrid logic, we consider minimal models, w.r.t. contradictions, of a certain set of formulas as sets of quasi-hybrid literals. To compare implementations we define the ratio of inconsistency which may differentiate between minimal models for the same set of formulas. Recently we have used this logic to reason in the healthcare delivery process [13]. Although in such paper there are just discussed small examples, it paves the way for interesting applications of QH logic.

Studying paraconsistency in the context of quantified hybrid logic is a main topic for future research. We are confident that this can be done along the guidelines that drove this work. The representation of a model by literals can also be computed, and the discussion about contradictions in minimal models, although more technical, can be done. Another issue that we would like to address is paraconsistency on modalities, by avoiding the standard duality between |$\Box$| and |$\Diamond$|⁠. This study was initiated by J. Marcos in [23]. A final topic for further research in the context of quantified hybrid logic, is the formulation of an analogue to the Herbrand’s Theorem based on the diagram representation discussed here.

In this work, there is no discussion concerning proof-theoretical aspects of quasi-classical logic. However, it is well-known that one important motivation for quasi-classical logic is the separation of analytic and synthetic stages of proof. First we analyse premises, and then infer new conclusions. The study of this issue in QH logic should be done. The challenge is how to combine the proof-theoretical features of quasi-classical logic with the hybrid ones.

Acknowledgements

We would like to thank João Marcos, whose suggestions greatly improved the presentation of this work. We also acknowledge the very relevant comments given by the anonymous reviewer.

Funding

This work was funded by ERDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT (Portuguese Foundation for Science and Technology) within project POCI-01-0145-FEDER-016692 (DaLi) and the project UID/MAT/04106/2013 at CIDMA. Diana was also supported by the FCT PhD-grant PD/BD/105730/2014. The second author also acknowledges the financial assistance by the project GetFun, reference FP7-PEOPLE-2012-IRSES and the Spanish MEC project FFI2013- 47126-P.