Bílková, Frittella, Kozhemiachenko, and Majer Two-layered logics for
probabilities and belief functions over Belnap–Dunn logic Article 100 2019
10.1017/xxxxx

(Received xx xxx xxx; revised xx xxx xxx; accepted xx xxx xxx)

# Two-layered logics for probabilities and belief functions over Belnap–Dunn
logic

Marta Bílková<EMAIL_ADDRESS>Institute of Computer Science, The Czech
Academy of Sciences, Prague
Sabine Frittella<EMAIL_ADDRESS>INSA Centre Val de Loire, Univ.
Orléans, LIFO EA 4022, France
Daniil Kozhemiachenko<EMAIL_ADDRESS>Univ. Bordeaux,
CNRS, Bordeaux INP, LaBRI, UMR 5800
Ondrej Majer<EMAIL_ADDRESS>Institute of Philosophy, The Czech Academy of
Sciences, Prague

###### Abstract

This paper is an extended version of Bílková et al., 2023b . We discuss two-
layered logics formalising reasoning with probabilities and belief functions
that combine the Łukasiewicz $[0,1]$-valued logic with Baaz $\triangle$
operator and the Belnap–Dunn logic.

We consider two probabilistic logics —
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
(introduced in Bílková et al., (2023)) and
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
(from Bílková et al., 2023b ) — that present two perspectives on the
probabilities in the Belnap–Dunn logic. In
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$,
every event $\phi$ has independent positive and negative measures that denote
the likelihoods of $\phi$ and $\neg\phi$, respectively. In
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$,
the measures of the events are treated as partitions of the sample into four
exhaustive and mutually exclusive parts corresponding to pure belief, pure
disbelief, conflict and uncertainty of an agent in $\phi$.

In addition to that, we discuss two logics for the paraconsistent reasoning
with belief and plausibility functions from Bílková et al., (2023) —
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$.
Both these logics equip events with two measures (positive and negative) with
their main difference being that in
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$,
the negative measure of $\phi$ is defined as the _belief in $\neg\phi$_ while
in
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$,
it is treated independently as _the plausibility of $\neg\phi$_.

We provide a sound and complete Hilbert-style axiomatisation of
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
and establish faithful translations between it and
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$.
We also show that the satisfiability problem in all the logics is
$\mathsf{NP}$-complete.

###### keywords:

two-layered logics; Łukasiewicz logic; non-standard probabilities; non-
standard belief functions; paraconsistent logics

##  1 Introduction

Classical probability and Dempster–Shafer theories study probability measures
and belief functions. These are maps from the set of events of a sample space
$W$ (i.e., from $2^{W}$) to $[0,1]$ that are monotone w.r.t. $\subseteq$ with
the following additional conditions: probability measures satisfy the (finite
or countable) additivity condition:

$\displaystyle\mu\left(\bigcup\limits_{i\in I}E_{i}\right)$
$\displaystyle=\sum\limits_{i\in I}\mu(E_{i})$ ($\forall i,j\in I:i\neq
j\Rightarrow E_{i}\cap E_{j}=\varnothing$)

and belief functions its weaker version (_total monotonicity_ in the
terminology of Zhou, (2013))

$\displaystyle\mathtt{bel}(W)$ $\displaystyle=1$
$\displaystyle\mathtt{bel}\left(\bigcup\limits_{1\leq i\leq k}E_{i}\right)$
$\displaystyle\geq\sum\limits_{\scriptsize{\begin{matrix}J\subseteq\\{1,\ldots,k\\}\\\
J\neq\varnothing\end{matrix}}}(-1)^{|J|+1}\cdot\mathtt{bel}\left(\bigcap\limits_{j\in
J}E_{j}\right)$ $\displaystyle\mathtt{bel}(\varnothing)$ $\displaystyle=0$

Above, the disjointness of $E_{i}$ and $E_{j}$ can be construed as their
incompatibility. Most importantly, if a propositional formula $\phi$ is
associated with an event $\|\phi\|$ (and interpreted as a statement about it),
then

$\mu(\|\phi\wedge\neg\phi\|)=\mathtt{bel}(\|\phi\wedge\neg\phi\|)=0$

(since $\|\phi\|$ and $\|\neg\phi\|$ are incompatible) and
$\|\phi\vee\neg\phi\|$ exhausts the entire sample space, whence

$\mu(\|\phi\vee\neg\phi\|)=\mathtt{bel}(\|\phi\vee\neg\phi\|)=1$

_Paraconsistent_ uncertainty theory, on the other hand, assumes that the
measure of an event represents not the likelihood of it happening but an
agent’s certainty therein which they infer from the information given by the
sources. In this respect, it is close to the classical Dempster–Shafer theory
that can also be considered as a generalisation of the subjective probability
theory.

The main difference between the classical and paraconsistent approaches is the
treatment of negation. Dempster–Shafer theory usually deals with
contradictions _between different sources_. However, it is reasonable to
assume that even a  _single source_ can give contradictory information (or
give no information at all). Thus, a ‘contradictory’ event
$\|\phi\wedge\neg\phi\|$ can have a positive probability or belief assignment
and that $\|\phi\vee\neg\phi\|$ does not necessarily exhaust the sample space.
Thus, a logic describing events should allow them to be both true and false
(if the source gives contradictory information) or neither true nor false
(when the source does not give information). Formally, this means that $\neg$
does not correspond to the complement in the sample space.

###  1.1 Belnap–Dunn logic

As one can see from the previous paragraph, we need a very special kind of
negation: the one that allows for true contradictions (and thus, rejects the
principle of explosion), and, additionally, invalidates the law of excluded
middle. Thus, the following principles are no longer valid

$\displaystyle\mathsf{EFQ}:p\wedge\neg p$ $\displaystyle\models q$
$\displaystyle\mathsf{LEM}:p\models q\vee\neg q$

The logics that lack $\mathsf{EFQ}$ are called _paraconsistent_ , those that
do not have $\mathsf{LEM}$ are _paracomplete_ , and those that fail both
principles are _paradefinite_ or _paranormal_ (cf., e.g., Arieli and Avron,
(2017) for the terminology).

The simplest paradefinite logic to represent reasoning about information
provided by sources is the Belnap–Dunn logic ($\mathsf{BD}$) from Dunn, (1976)
and Belnap, (1977, 2019). Originally, $\mathsf{BD}$ was presented as a four-
valued propositional logic in the $\\{\neg,\wedge,\vee\\}$ language. The
values (which we will henceforth call _Belnapian values_) represent different
accounts a source can give regarding a statement $\phi$:

  * •

$\mathbf{T}$ stands for ‘the source only says that $\phi$ is true’;

  * •

$\mathbf{F}$ stands for ‘the source only says that $\phi$ is false’;

  * •

$\mathbf{B}$ stands for ‘the source says both that $\phi$ is false and that
$\phi$ is true’;

  * •

$\mathbf{N}$ stands for ‘the source does not say that $\phi$ is false nor that
it is true’.

The interpretation of the truth values allows for reformulating $\mathsf{BD}$
semantics in terms of _two classical but independent valuations_. Namely,

| is true when | is false when
---|---|---
$\neg\phi$ |  $\phi$ is false |  $\phi$ is true
$\phi_{1}\wedge\phi_{2}$ |  $\phi_{1}$ and $\phi_{2}$ are true |  $\phi_{1}$ is false or $\phi_{2}$ is false
$\phi_{1}\vee\phi_{2}$ |  $\phi_{1}$ is true or $\phi_{2}$ is true |  $\phi_{1}$ and $\phi_{2}$ are false

It is easy to see that there are no universally true nor universally false
formulas in $\mathsf{BD}$. Thus, $\mathsf{BD}$ satisfies the desiderata
outlined above. Moreover, even if we define $\phi\Rightarrow\chi$ as
$\neg\phi\vee\chi$, it is clear that neither modus ponens, nor the Deduction
theorem will hold for $\Rightarrow$. I.e., $\mathsf{BD}$ lacks the (definable)
implication (cf. (Omori and Wansing,, 2017, §5.1) for a detailed discussion of
the implication in $\mathsf{BD}$). This, however, is not problematic since we
are going to use $\mathsf{BD}$ only to represent events and conditional
statements which are usually formalised with an implication do not correspond
to descriptions of events.

###  1.2 Probabilities and belief functions in $\mathsf{BD}$

The original interpretation of the Belnapian truth values that we gave above
is presented in terms of the information one has. In this approach, however,
the information is assumed to be crisp. Theories of uncertainty over
$\mathsf{BD}$ were introduced to formalise situations where one has access to
graded information. For instance, the first source could tell that $p$ is true
with the likelihood $0.4$ and the second that $p$ is false with probability
$0.7$. If one follows $\mathsf{BD}$ and treats positive and negative evidence
independently, one needs a non-classical notion of uncertainty measures to
represent this information.

To the best of our knowledge, the earliest formalisation of probability theory
in terms of $\mathsf{BD}$ was provided by Mares, (1997). The formalisation is
very similar to the one that we are going to use in this paper but bears one
significant distinction. Namely, (Mares,, 1997, §2) uses _normalised_ measures
(i.e., those where $\mu(W)=1$ and $\mu(\varnothing)=0$). This requirement,
however, is superfluous since $\mathsf{BD}$ lacks universally (in)valid
formulas.

Another formalisation is given in Dunn, (2010). Dunn proposes to divide the
sample space into four exhaustive and mutually exclusive parts depending on
the Belnapian value of $\phi$. An alternative approach was proposed in Klein
et al., (2021). There, the authors propose two equivalent interpretations
based on the two formulations of semantics. The first option is to give $\phi$
two _independent probability measures_ : the one determining the likelihood of
$\phi$ to be true and the other the likelihood of $\phi$ to be false. The
second option follows Dunn and also divides the sample space according to
whether $\phi$ has value $\mathbf{T}$, $\mathbf{B}$, $\mathbf{N}$, or
$\mathbf{F}$ in a given state. Note that in both cases, the probabilities are
interpreted _subjectively_.

The main difference between these two approaches is that in Dunn, (2010), the
probability of $\phi\wedge\phi^{\prime}$ is entirely determined by those of
$\phi$ and $\phi^{\prime}$ which makes it compositional. On the other hand,
the paraconsistent probabilities proposed in Klein et al., (2021) are not
compositional w.r.t. conjunction. In this paper, we choose the latter approach
since it can be argued (cf. Dubois, (2008) for the details) that belief is not
compositional when it comes to contradictory information.

A similar approach to paraconsistent probabilities was proposed by, e.g.,
Bueno-Soler and Carnielli, (2016) and Rodrigues et al., (2021). There,
probabilities are defined over an extension of $\mathsf{BD}$ with classicality
and non-classicality operators. It is worth mentioning that the proposed
axioms of probability are very close to those from Klein et al., (2021): e.g.,
both allow measures $\mathtt{p}$ s.t.
$\mathtt{p}(\phi)+\mathtt{p}(\neg\phi)<1$ (if the information regarding $\phi$
is incomplete) or $\mathtt{p}(\phi)+\mathtt{p}(\neg\phi)>1$ (when the
information is contradictory).

Belief functions over $\mathsf{BD}$ were first defined in Zhou, (2013). There,
they were presented on the ordered sets of states. Each formula $\phi$ in this
approach corresponds to _two_ sets of states: $|\phi|^{+}$ (states where
$\phi$ has value $\mathbf{T}$ or $\mathbf{B}$) and $|\phi|^{-}$ (states where
it is evaluated at $\mathbf{B}$ or $\mathbf{F}$). Moreover, a logic
formalising reasoning with belief functions was presented. A similar treatment
of (non-normalised or _general_ in the terminology of the paper) belief
functions in $\mathsf{BD}$ was given in Bílková et al., (2023). The main
difference between the two interpretations of belief functions was that in
Bílková et al., (2023), two options for interpreting
$\mathtt{bel}(|\phi|^{-})$ were given: the first one was to treat it as the
belief of $\neg\phi$, and the second one — as _the plausibility_ of
$\neg\phi$. Another distinction was in the formalisation: Zhou, (2013)
constructs a logic for reasoning about belief functions following Fagin et
al., (1990): i.e., incorporating the arithmetical operations and inequalities
containing them into the language. In Bílková et al., (2023), a different
approach was utilised: instead of using arithmetic inequalities, the reasoning
about belief functions is conducted in a different logic — a paraconsistent
expansion of the Łukasiewicz logic Ł — that is capable of expressing
arithmetic operations on $[0,1]$.

###  1.3 Two-layered logics for uncertainty

Reasoning about uncertainty can be formalised via modal logics where the
modality is interpreted as a measure of an event. The concrete semantics of
the modality can be defined in two ways. First, using a modal language with
Kripke semantics where the measure is defined on the set of states as done by,
e.g., Gärdenfors, (1975); Delgrande and Renne, (2015); Delgrande et al.,
(2019) for qualitative probabilities, by Dautović et al., (2021) for the
quantitative ones, and by Rodriguez et al., (2022) for the possibility and
necessity measures. Second, employing a two-layered formalism (cf. Fagin et
al., (1990); Fagin and Halpern, (1991), Hájek et al., (1995), Baldi et al.,
(2020), and Bílková et al., (2023); Bílková et al., 2023a ; Bílková et al.,
2023b  for examples). There, the logic is split into two levels: the inner
layer describes events, and the outer layer describes the reasoning with the
measure defined on events. The measure is a _non-nesting_ modality
$\mathtt{M}$, and the outer-layer formulas are built from _‘modal atoms’_ —
formulas of the form $\mathtt{M}\phi$ with $\phi$ being an inner-layer
formula. The outer-layer formulas are then equipped with the semantics of a
fuzzy logic that permits necessary operations (e.g., Łukasiewicz for the
quantitative reasoning and Gödel for the qualitative).

An alternative to the two-layered logics is to use the language of linear
inequalities to reason about measures of events. This is done by Fagin et al.,
(1990) for the classical reasoning about probabilities and by Zhou, (2013) for
the reasoning with the belief functions over $\mathsf{BD}$. In both cases, it
is established that the logics with inequalities and the two-layered logics
are equivalent — cf. Baldi et al., (2020) for the case of classical
probabilities and Bílková et al., (2023) for the reasoning with belief
functions and probabilities over $\mathsf{BD}$.

We choose the two-layered approach. First, it is more modular than the usual
Kripke semantics: as long as the logic of the event description is chosen, we
can define different measures on top of it using different upper-layer logics.
Second, the completeness proof is very simple since one only needs to
translate the axioms of the given measure into the outer-layer logic. Third,
the techniques that are used to establish the decidability of the outer-layer
logic can be applied to the decidability proof of the two-layered logic.
Finally, even though the traditional Kripke semantics is more expressive than
two-layered logics, this expressivity is not necessary in many contexts.
Indeed, people rarely say something like ‘it is probable that it is probable
that $\phi$’. Moreover, it is considerably more difficult to motivate the
assignment of truth values in the nesting case, in particular, when the same
measure is applied both to a propositional and modalised formula as in, e.g.,
$\mathtt{M}(p\wedge\mathtt{M}q)$.

We will also be dealing with the formalisation of the _quantitative_
reasoning. Formally, this means that we assume that the agents can assign
numerical values to their certainty in a given proposition or say something
like ‘I think that rain is twice more likely than snow’. Thus, we need a logic
that can express the paraconsistent counterparts of the additivity condition
as well as basic arithmetic operations. We choose the Łukasiewicz logic (Ł)
for the outer layer since it can define (truncated) addition and subtraction
on $[0,1]$.

###  1.4 Plan of the paper

This paper is an extended version of an earlier conference submission Bílková
et al., 2023b . The novel contribution of this manuscript is the proof of the
$\mathsf{NP}$-completeness of the two-layered logics for belief functions from
Bílková et al., (2023). As such, we continue the study of uncertainty via
paraconsistent logics proposed in Bílková et al., (2020) and continued in
Bílková et al., (2023), Bílková et al., 2023a , and Bílková et al., (2023).
The overarching goal of the project is to study logics that can express the
following properties of beliefs.

  1. 1.

Given two statements $\phi$ and $\chi$, one can be more certain in $\phi$ than
in $\chi$ but still, neither believe in $\phi$ _completely_ nor consider
$\chi$ completely impossible.

  2. 2.

Given two trusted sources, one can still prefer one source to the other.

  3. 3.

One can believe in a contradiction but still not believe in something else.

  4. 4.

Given two statements, it is possible that one cannot always compare their
degrees of certainty in them (if, e.g., these statements have no common
content).

The remainder of the text is structured as follows. In Section 2, we recall
two approaches to probabilities over $\mathsf{BD}$ from Klein et al., (2021).
In Section 3, we provide the semantics and axiomatisations of two-layered
logics for probabilities and establish their $\mathsf{NP}$-completeness. In
Section 4, we recall two treatments of belief functions over $\mathsf{BD}$
that were presented in Bílková et al., (2023). In Section 5, we discuss the
two-layered logics for belief functions and show their
$\mathsf{NP}$-completeness. Finally, we summarise our results and set goals
for future research in Section 6.

##  2 Probabilities over $\mathsf{BD}$

In the previous section, we gave an informal presentation of $\mathsf{BD}$ as
a four-valued logic. Since we are going to use it to describe events, we will
formulate its semantics in terms of sets of states. The language of
$\mathsf{BD}$ is given by the following grammar (with $\mathtt{Prop}$ being a
countable set of propositional variables).

$\mathcal{L}_{\mathsf{BD}}\ni\phi\coloneqq
p\in\mathtt{Prop}\mid\neg\phi\mid(\phi\wedge\phi)\mid(\phi\vee\phi)$

[Notation] In what follows, $\mathtt{Prop}(\phi)$ denotes the set of variables
occurring in $\phi$ and $\mathsf{Lit}(\phi)$ stands for the set of _literals_
(i.e., variables or their negations) occurring in $\phi$. Moreover,
$\mathtt{Sf}(\phi)$ is the set of all subformulas of $\phi$. The _length_
(i.e., the number of symbols) of $\phi$ is denoted with $\mathcal{l}(\phi)$.

We are also going to use two kinds of formulas: the single- and the two-
layered ones. To make the differentiation between them simpler, we use Greek
letters from the end of the alphabet ($\phi$, $\chi$, $\psi$, etc.) to
designate the first kind and the letters from the beginning of the alphabet
($\alpha$, $\beta$, $\gamma$, …) for the second kind.

Furthermore, we use $v$ (with indices) to stand for the valuations of single-
layered formulas and $e$ (with indices) for the two-layered formulas.

######  Definition 2.1 (Set semantics of $\mathsf{BD}$).

Let $\phi,\phi^{\prime}\in\mathcal{L}_{\mathsf{BD}}$, $W\neq\varnothing$, and
$v^{+},v^{-}:\mathtt{Prop}\to 2^{W}$. For a model $\mathfrak{M}=\langle
W,v^{+},v^{-}\rangle$, we define notions of $w\vDash^{+}\phi$ and
$w\vDash^{-}\phi$ for $w\in W$ as follows.

$\displaystyle w\vDash^{+}p$ $\displaystyle\text{ iff }w\in v^{+}(p)$
$\displaystyle w\vDash^{-}p$ $\displaystyle\text{ iff }w\in v^{-}(p)$
$\displaystyle w\vDash^{+}\neg\phi$ $\displaystyle\text{ iff }w\vDash^{-}\phi$
$\displaystyle w\vDash^{-}\neg\phi$ $\displaystyle\text{ iff }w\vDash^{+}\phi$
$\displaystyle w\vDash^{+}\phi\wedge\phi^{\prime}$ $\displaystyle\text{ iff
}w\vDash^{+}\phi\text{ and }w\vDash^{+}\phi^{\prime}$ $\displaystyle
w\vDash^{-}\phi\wedge\phi^{\prime}$ $\displaystyle\text{ iff
}w\vDash^{-}\phi\text{ or }w\vDash^{-}\phi^{\prime}$ $\displaystyle
w\vDash^{+}\phi\vee\phi^{\prime}$ $\displaystyle\text{ iff
}w\vDash^{+}\phi\text{ or }w\vDash^{+}\phi^{\prime}$ $\displaystyle
w\vDash^{-}\phi\vee\phi^{\prime}$ $\displaystyle\text{ iff
}w\vDash^{-}\phi\text{ and }w\vDash^{-}\phi^{\prime}$

We denote the positive and negative extensions of a formula as follows:

$\displaystyle|\phi|^{+}\coloneqq\\{w\in W\mid w\vDash^{+}\phi\\}$
$\displaystyle|\phi|^{-}\coloneqq\\{w\in W\mid w\vDash^{-}\phi\\}.$

A sequent $\phi\vdash\chi$ is _satisfied on $\mathfrak{M}=\langle
W,v^{+},v^{-}\rangle$_ (denoted, $\mathfrak{M}\models[\phi\vdash\chi]$) iff
$|\phi|^{+}\subseteq|\chi|^{+}$. A sequent $\phi\vdash\chi$ is _$\mathsf{BD}$
-valid_ ($\phi\models_{\mathsf{BD}}\chi$) iff it is satisfied on every model.
In this case, we will say that $\phi$ _entails_ $\chi$ _in $\mathsf{BD}$_.

Now, we can use the above semantics to define probabilities on the models. We
adapt the definitions from Klein et al., (2021).

######  Definition 2.2 ($\mathsf{BD}$ models with $\pm$-probabilities).

A _$\mathsf{BD}$ model with a $\pm$-probability_ is a tuple
$\mathfrak{M}_{\pm}=\langle\mathfrak{M},\mu\rangle$ with $\mathfrak{M}$ being
a $\mathsf{BD}$ model and $\mu:2^{W}\rightarrow[0,1]$ satisfying:

$\mathbf{mon}$:

if $X\subseteq Y$, then $\mu(X)\leq\mu(Y)$;

$\mathbf{neg}$:

$\mu(|\phi|^{-})=\mu(|\neg\phi|^{+})$;

$\mathbf{ex}$:

$\mu(|\phi\vee\chi|^{+})=\mu(|\phi|^{+})+\mu(|\chi|^{+})-\mu(|\phi\wedge\chi|^{+})$.

To facilitate the presentation of the four-valued probabilities defined over
$\mathsf{BD}$ models, we introduce additional extensions of $\phi$ defined via
$|\phi|^{+}$ and $|\phi|^{-}$. Let $\mathfrak{M}=\langle W,v^{+},v^{-}\rangle$
be a $\mathsf{BD}$ model, $\phi\in\mathcal{L}_{\mathsf{BD}}$. We set

$\displaystyle|\phi|^{\mathsf{b}}=$
$\displaystyle|\phi|^{+}\setminus|\phi|^{-}$
$\displaystyle|\phi|^{\mathsf{d}}=$
$\displaystyle|\phi|^{-}\setminus|\phi|^{+}$
$\displaystyle|\phi|^{\mathsf{c}}=$ $\displaystyle|\phi|^{+}\cap|\phi|^{-}$
$\displaystyle|\phi|^{\mathsf{u}}=$ $\displaystyle
W\setminus(|\phi|^{+}\cup|\phi|^{-})$

We call these extensions, respectively, _pure belief_ , _pure disbelief_ ,
_conflict_ , and _uncertainty in $\phi$_, following Klein et al., (2021). One
can observe that these extensions correspond to the Belnapian values of
$\phi$:

  * •

_pure belief extension_ of $\phi$ is the set of states where $\phi$ has value
$\mathbf{T}$;

  * •

_pure disbelief extension_ of $\phi$ is the set of states where $\phi$ has
value $\mathbf{F}$;

  * •

_conflict extension_ of $\phi$ is the set of states where $\phi$ has value
$\mathbf{B}$;

  * •

_uncertainty extension_ of $\phi$ is the set of states where $\phi$ has value
$\mathbf{N}$.

######  Definition 2.3 ($\mathsf{BD}$ models with $\mathbf{4}$-probabilities).

A _$\mathsf{BD}$ model with a $\mathbf{4}$-probability_ is a tuple
$\mathfrak{M}_{\mathbf{4}}=\langle\mathfrak{M},\mu_{\mathbf{4}}\rangle$ with
$\mathfrak{M}$ being a $\mathsf{BD}$ model and
$\mu_{\mathbf{4}}:2^{W}\rightarrow[0,1]$ satisfying:

$\mathbf{part}$:

$\mu_{\mathbf{4}}(|\phi|^{\mathsf{b}})+\mu_{\mathbf{4}}(|\phi|^{\mathsf{d}})+\mu_{\mathbf{4}}(|\phi|^{\mathsf{u}})+\mu_{\mathbf{4}}(|\phi|^{\mathsf{c}})=1$;

$\mathbf{neg}$:

$\mu_{\mathbf{4}}(|\neg\phi|^{\mathsf{b}})=\mu_{\mathbf{4}}(|\phi|^{\mathsf{d}})$,
$\mu_{\mathbf{4}}(|\neg\phi|^{\mathsf{c}})=\mu_{\mathbf{4}}(|\phi|^{\mathsf{c}})$;

$\mathbf{contr}$:

$\mu_{\mathbf{4}}(|\phi\wedge\neg\phi|^{\mathsf{b}})=0$,
$\mu_{\mathbf{4}}(|\phi\wedge\neg\phi|^{\mathsf{c}})=\mu_{\mathbf{4}}(|\phi|^{\mathsf{c}})$;

$\mathbf{BCmon}$:

if $\mathfrak{M}\models[\phi\vdash\chi]$, then
$\mu_{\mathbf{4}}(|\phi|^{\mathsf{b}})+\mu_{\mathbf{4}}(|\phi|^{\mathsf{c}})\leq\mu_{\mathbf{4}}(|\chi|^{\mathsf{b}})+\mu_{\mathbf{4}}(|\chi|^{\mathsf{c}})$;

$\mathbf{BCex}$:

$\mu_{\mathbf{4}}(|\phi|^{\mathsf{b}})+\mu_{\mathbf{4}}(|\phi|^{\mathsf{c}})+\mu_{\mathbf{4}}(|\psi|^{\mathsf{b}})+\mu_{\mathbf{4}}(|\psi|^{\mathsf{c}})=\mu_{\mathbf{4}}(|\phi\wedge\psi|^{\mathsf{b}})+\mu_{\mathbf{4}}(|\phi\wedge\psi|^{\mathsf{c}})+\mu_{\mathbf{4}}(|\phi\vee\psi|^{\mathsf{b}})+\mu_{\mathbf{4}}(|\phi\vee\psi|^{\mathsf{c}})$.

[Naming the probabilities] We will utilise the following naming convention:

  * •

we use the term _‘ $\pm$-probability’_ to stand for $\mu$ from Definition 2.2;

  * •

we call $\mu_{\mathbf{4}}$ from Definition 2.3 a  _‘
$\mathbf{4}$-probability’_ or a  _‘four-valued probability’_.

Recall that $\pm$-probabilities are referred to as ‘non-standard’ in Klein et
al., (2021) and Bílková et al., (2023). As this term is too broad (four-valued
probabilities are not ‘standard’ either), we use a different designation.

Let us quickly discuss the measures defined above. First, observe that
$\mu(|\phi|^{+})$ and $\mu(|\phi|^{-})$ are independent from one another.
Thus, $\mu$ gives two measures to each $\phi$, as desired. Second, recall
(Klein et al.,, 2021, Theorems 2–3) that every $\mathbf{4}$-probability on a
$\mathsf{BD}$ model induces a $\pm$-probability and vice versa. In the
following sections, we will define two-layered logics for $\mathsf{BD}$ models
with $\pm$\- and $\mathbf{4}$-probabilities and show that they can be
faithfully embedded into each other. It is instructive to note, moreover, that
while $\pm$\- and $\mathbf{4}$-probabilities can be simulated by the classical
ones, they do behave in a very different way.

######  Example 2.4 (Paraconsistent vs. classical probabilities).

First of all, observe that a $\pm$-probability _can be uniform_. Indeed, for
every $c\in[0,1]$ and every $\mathsf{BD}$-model $\langle
W,v^{+},v^{-}\rangle$, it is easy to check that the assignment $\forall
X\subseteq W:\mu(X)=c$ _is a $\pm$-probability_.

Second, the general import-export condition

$\displaystyle\mu(X\cup Y)$ $\displaystyle=\mu(X)+\mu(Y)-\mu(X\cap Y)$
($\mathsf{IE}$)

that is true for the classical probabilities does not hold in general either.
For consider Fig. 1. One can see that $\mu$ is monotone and that
$\mu(|\phi|^{+})=\mu(|\phi|^{-})=0$ for every
$\phi\in\mathcal{L}_{\mathsf{BD}}$ (whence, $\mu$ is a $\pm$-probability). On
the other hand, it is clear that
$\mu(W)\neq\mu(\\{u_{1}\\})+\mu(\\{u_{2}\\})-\mu(\varnothing)$.

$\textstyle{u_{1}:\xcancel{p}}$$\textstyle{u_{2}:\xcancel{p}}$ Figure 1: A
counterexample to ($\mathsf{IE}$):
$\mu(\\{u_{1}\\})=\mu(\\{u_{2}\\})=\frac{1}{3}$, $\mu(W)=1$, and
$\mu(\varnothing)=0$. All variables have the same values exemplified by $p$.

This, however, is not a problem since for every $\mathsf{BD}$ model with a
$\pm$-probability $\langle W,v^{+},v^{-},\mu\rangle$, there exists a
$\mathsf{BD}$ model $\langle W^{\prime},v^{\prime+},v^{\prime-},\pi\rangle$
with a  _classical_ probability measure $\pi$ s.t.
$\pi(|\phi|^{+})=\mu(|\phi|^{+})$ (Klein et al.,, 2021, Theorem 4).

First of all, for the case of the model shown in Fig. 1, one can either define
$\pi(\\{u_{1}\\})=\pi(\\{u_{2}\\})=\frac{1}{2}$, or add a new state $u_{3}$
where all variables are neither true nor false. For a bit more refined
example, consider Fig. 2 and set $W=\\{w_{1},w_{2}\\}$ and
$W^{\prime}=\\{w^{\prime}_{1},w^{\prime}_{2},w^{\prime}_{3}\\}$. It is clear
that for every $\phi\in\mathcal{L}_{\mathsf{BD}}$,
$\mu(|\phi|^{+})=\pi(|\phi|^{+})=\frac{1}{2}$.

Likewise, $\mu_{\mathbf{4}}$ is not necessarily monotone w.r.t. $\subseteq$
(which is required of the classical probabilities) since not every subset of a
model is represented by an extension of an $\mathcal{L}_{\mathsf{BD}}$
formula. Again, it is not a problem since for every $\mathsf{BD}$ model with
$\mathbf{4}$-probability $\langle W,v^{+},v^{-},\mu_{\mathbf{4}}\rangle$,
there exist a $\mathsf{BD}$ model $\langle
W^{\prime},v^{\prime+},v^{\prime-},\pi\rangle$ with a  _classical_ probability
measure $\pi$ s.t.
$\pi(|\phi|^{\mathsf{x}})=\mu_{\mathbf{4}}(|\phi|^{\mathsf{x}})$ for
$\mathsf{x}\in\\{\mathsf{b},\mathsf{d},\mathsf{c},\mathsf{u}\\}$ (Klein et
al.,, 2021, Theorem 5).

Thus, we will further assume w.l.o.g. that $\mu$ and $\mu_{\mathbf{4}}$ are
_classical probability measures_ on $W$.

$\textstyle{w_{1}:p^{+}}$$\textstyle{w_{2}:p^{\pm}}$$\textstyle{w^{\prime}_{1}:p^{+}}$$\textstyle{w^{\prime}_{2}:p^{\pm}}$$\textstyle{w^{\prime}_{3}:\xcancel{p}}$
Figure 2: The values of all variables coincide with the values of $p$ state-
wise. $\mu(X)=\frac{1}{2}$ for every $X\subseteq W$;
$\pi(\varnothing)=\pi(\\{w^{\prime}_{1}\\})=0$, $\pi(W^{\prime})=1$,
$\pi(X^{\prime})=\frac{1}{2}$ otherwise.

##  3 Logics for paraconsistent probabilities

In this section, we provide two-layered logics that are (weakly) complete
w.r.t. $\mathsf{BD}$ models with $\pm$\- and $\mathbf{4}$-probabilities. Since
conditions on measures contain arithmetic operations on $[0,1]$, we choose an
expansion of Łukasiewicz logic, namely, Łukasiewicz logic with $\triangle$
(${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$),
for the outer layer. Furthermore, $\pm$-probabilities work with both positive
and negative extensions of formulas, whence it is reasonable to use
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
— a paraconsistent expansion of Ł (cf. Bílková et al., (2020) and Bílková et
al., (2021) for details) with two valuations — $v_{1}$ (support of truth) and
$v_{2}$ (support of falsity) — on $[0,1]$.

###  3.1 Languages, semantics, and equivalence

Let us first recall the semantics of
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
and
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$.
To facilitate the presentation, we begin with the definition of the standard
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
algebra on $[0,1]$ that we will then use to define the semantics of both
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
and
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$.

######  Definition 3.1.

The standard
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
algebra is a tuple
$\langle[0,1],{\sim_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}},\triangle_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}},\wedge_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}},\vee_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}},\rightarrow_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}},\odot_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}},\oplus_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}},\ominus_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}\rangle$
with the operations are defined as follows.

$\displaystyle{\sim_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}a$
$\displaystyle\coloneqq 1-a$
$\displaystyle\triangle_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}a$
$\displaystyle\coloneqq\begin{cases}1&\text{if }a=1\\\
0&\text{otherwise}\end{cases}$ $\displaystyle
a\wedge_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}b$
$\displaystyle\coloneqq\min(a,b)$ $\displaystyle
a\vee_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}b$
$\displaystyle\coloneqq\max(a,b)$ $\displaystyle
a\rightarrow_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}b$
$\displaystyle\coloneqq\min(1,1-a+b)$ $\displaystyle
a\odot_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}b$
$\displaystyle\coloneqq\max(0,a+b-1)$ $\displaystyle
a\oplus_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}b$
$\displaystyle\coloneqq\min(1,a+b)$ $\displaystyle
a\ominus_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}b$
$\displaystyle\coloneqq\max(0,a-b)$

######  Definition 3.2
(${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$).

The language of
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
is given via the following grammar

$\mathcal{L}_{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}\ni\phi\coloneqq
p\in\mathtt{Prop}\mid{\sim}\phi\mid\triangle\phi\mid(\phi\wedge\phi)\mid(\phi\vee\phi)\mid(\phi\rightarrow\phi)\mid(\phi\odot\phi)\mid(\phi\oplus\phi)\mid(\phi\ominus\phi)$

We will also write $\phi\leftrightarrow\chi$ as a shorthand for
$(\phi\rightarrow\chi)\odot(\chi\rightarrow\phi)$.

A valuation is a map $v:\mathtt{Prop}\rightarrow[0,1]$ that is extended to the
complex formulas as expected:
$v(\phi\circ\chi)=v(\phi)\circ_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v(\chi)$.

$\phi$ is
_${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
-valid_ iff $v(\phi)=1$ for every $v$. $\Gamma$ _entails_ $\chi$ (denoted
$\Gamma\models_{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}\chi$)
iff for every $v$ s.t. $v(\phi)=1$ for all $\phi\in\Gamma$, it holds that
$v(\chi)=1$ as well.

######  Definition 3.3
(${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$).

The language is constructed using the following grammar.

$\mathcal{L}_{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}}\ni\phi\coloneqq
p\in\mathtt{Prop}\mid\neg\phi\mid{\sim}\phi\mid\triangle\phi\mid(\phi\rightarrow\phi)$

The semantics is given by _two_ valuations $v_{1}$ (support of truth) and
$v_{2}$ (support of falsity) $v_{1},v_{2}:\mathtt{Prop}\rightarrow[0,1]$ that
are extended as follows.

$\displaystyle v_{1}(\neg\phi)$ $\displaystyle=v_{2}(\phi)$ $\displaystyle
v_{2}(\neg\phi)$ $\displaystyle=v_{1}(\phi)$ $\displaystyle v_{1}({\sim}\phi)$
$\displaystyle={\sim_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}v_{1}(\phi)$
$\displaystyle v_{2}({\sim}\phi)$
$\displaystyle={\sim_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}v_{2}(\phi)$
$\displaystyle v_{1}(\triangle\phi)$
$\displaystyle=\triangle_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v_{1}(\phi)$
$\displaystyle v_{2}(\triangle\phi)$
$\displaystyle={\sim_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}\triangle_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}{\sim}_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v_{2}(\phi)$
$\displaystyle v_{1}(\phi\rightarrow\chi)$
$\displaystyle=v_{1}(\phi)\rightarrow_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v_{1}(\chi)$
$\displaystyle v_{2}(\phi\rightarrow\chi)$
$\displaystyle=v_{2}(\chi)\ominus_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v_{2}(\phi)$

We say that $\phi$ is
_${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
-valid_ iff for every $v_{1}$ and $v_{2}$, it holds that $v_{1}(\phi)=1$ and
$v_{2}(\phi)=0$.

When there is no risk of confusion, we will use $v(\phi)=(x,y)$ to stand for
$v_{1}(\phi)=x$ and $v_{2}(\phi)=y$.

######  Remark 3.4.

Note that ${\sim}$ and $\rightarrow$ can be used to define all other
connectives in
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
and
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$.

$\displaystyle\phi\vee\chi$
$\displaystyle\coloneqq(\phi\rightarrow\chi)\rightarrow\chi$
$\displaystyle\phi\wedge\chi$
$\displaystyle\coloneqq{\sim}({\sim}\phi\vee{\sim}\chi)$
$\displaystyle\phi\oplus\chi$
$\displaystyle\coloneqq{\sim}\phi\rightarrow\chi$ $\displaystyle\phi\odot\chi$
$\displaystyle\coloneqq{\sim}(\phi\rightarrow{\sim}\chi)$
$\displaystyle\phi\ominus\chi$ $\displaystyle\coloneqq\phi\odot{\sim}\chi$
$\displaystyle\phi\leftrightarrow\chi$
$\displaystyle\coloneqq(\phi\rightarrow\chi)\odot(\chi\rightarrow\phi)$

We are now ready to present our two-layered logics for paraconsistent
probabilities:
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
— the logic of $\mathbf{4}$-probabilities, and
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
— the logic of $\pm$-probabilities.

######  Definition 3.5
($\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$:
language and semantics).

The language of
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
is constructed via the following grammar:

$\displaystyle\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}\ni\alpha$
$\displaystyle\coloneqq\mathsf{Bl}\phi\mid\mathsf{Db}\phi\mid\mathsf{Cf}\phi\mid\mathsf{Uc}\phi\mid{\sim}\alpha\mid\triangle\alpha\mid(\alpha\rightarrow\alpha)$
($\phi\in\mathcal{L}_{\mathsf{BD}}$)

A
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
model is a tuple $\mathbb{M}=\langle\mathfrak{M},\mu_{\mathbf{4}},e\rangle$
s.t.

  * •

$\langle\mathfrak{M},\mu_{\mathbf{4}}\rangle$ is a $\mathsf{BD}$ model with
$\mathbf{4}$-probability;

  * •

$e$ is a
_${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
valuation induced by $\mu_{\mathbf{4}}$_, i.e.:

    * –

$e(\mathsf{Bl}\phi)=\mu_{\mathbf{4}}(|\phi|^{\mathsf{b}})$,
$e(\mathsf{Db}\phi)=\mu_{\mathbf{4}}(|\phi|^{\mathsf{d}})$,
$e(\mathsf{Cf}\phi)=\mu_{\mathbf{4}}(|\phi|^{\mathsf{c}})$,
$e(\mathsf{Uc}\phi)=\mu_{\mathbf{4}}(|\phi|^{\mathsf{u}})$;

    * –

values of complex
$\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$-formulas
are computed via Definition 3.2.

We say that $\alpha$ is
_$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
valid_ iff $e(\alpha)=1$ in every model. A set of formulas $\Gamma$ _entails_
$\alpha$
($\Gamma\models_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}\alpha$)
iff there is no $\mathbb{M}$ s.t. $e(\gamma)=1$ for every $\gamma\in\Gamma$
but $e(\alpha)\neq 1$.

######  Definition 3.6
($\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$:
language and semantics).

The language of
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
is given by the following grammar

$\displaystyle\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}\ni\alpha$
$\displaystyle\coloneqq\mathsf{Pr}\phi\mid{\sim}\alpha\mid\neg\alpha\mid\triangle\alpha\mid(\alpha\rightarrow\alpha)$
($\phi\in\mathcal{L}_{\mathsf{BD}}$)

A
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
model is a tuple $\mathbb{M}=\langle\mathfrak{M},\mu,e_{1},e_{2}\rangle$ s.t.

  * •

$\langle\mathfrak{M},\mu\rangle$ is a $\mathsf{BD}$ model with
$\pm$-probability;

  * •

$e_{1}$ and $e_{2}$ are
_${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
valuations induced by $\mu$_, i.e.:

    * –

$e_{1}(\mathsf{Pr}\phi)=\mu(|\phi|^{+})$,
$e_{2}(\mathsf{Pr}\phi)=\mu(|\phi|^{-})$;

    * –

the values of complex
$\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$
formulas are computed following Definition 3.3.

We say that $\alpha$ is
_$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
valid_ iff $e(\alpha)=(1,0)$ in every model. A set of formulas $\Gamma$
_entails_ $\alpha$
($\Gamma\models_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}\alpha$)
iff there is no $\mathbb{M}$ s.t. $e(\gamma)=(1,0)$ for all $\gamma\in\Gamma$
but $e(\alpha)\neq(1,0)$.

The following property of
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
will be useful further in the section.

######  Lemma 3.7.

Let
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$.
Then, $\alpha$ is
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
valid iff $e_{1}(\alpha)=1$ in every
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
model.

######  Proof 3.8.

Let $\mathbb{M}=\langle W,v^{+},v^{-},\mu,e_{1},e_{2}\rangle$ be a
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
model s.t. $e_{2}(\alpha)\neq 0$. We construct a model $\mathbb{M}^{*}=\langle
W,(v^{*})^{+},(v^{*})^{-},\mu,e^{*}_{1},e^{*}_{2}\rangle$ where
$e^{*}_{1}(\alpha)\neq 1$. To do this, we define new $\mathsf{BD}$ valuations
$(v^{*})^{+}$ and $(v^{*})^{-}$ on $W$ as follows.

$\displaystyle w\in v^{+}(p),w\notin v^{-}(p)$ $\displaystyle\text{ then
}w\in(v^{*})^{+}(p),w\notin(v^{*})^{-}(p)$ $\displaystyle w\in
v^{+}(p),v^{-}(p)$ $\displaystyle\text{ then
}w\notin(v^{*})^{+}(p),(v^{*})^{-}(p)$ $\displaystyle w\notin
v^{+}(p),v^{-}(p)$ $\displaystyle\text{ then
}w\in(v^{*})^{+}(p),(v^{*})^{-}(p)$ $\displaystyle w\notin v^{+}(p),w\in
v^{-}(p)$ $\displaystyle\text{ then }w\notin(v^{*})^{+}(p),w\in(v^{*})^{-}(p)$

It can be easily checked by induction on $\phi\in\mathcal{L}_{\mathsf{BD}}$
that

$\displaystyle|\phi|^{+}_{\mathbb{M}}$
$\displaystyle=W\setminus|\phi|^{-}_{\mathbb{M}^{*}}$
$\displaystyle|\phi|^{-}_{\mathbb{M}}$
$\displaystyle=W\setminus|\phi|^{+}_{\mathbb{M}^{*}}$ (1)

Now, since we can w.l.o.g. assume that $\mu$ is a (classical) probability
measure on $W$ (recall Example 2.4), we have that

$\displaystyle
e^{*}(\mathsf{Pr}\phi)=(1-\mu(|\phi|^{-}),1-\mu(|\phi|^{+}))=(1-e_{2}(\mathsf{Pr}\phi),1-e_{1}(\mathsf{Pr}\phi))$
(2)

Observe that if $e(\alpha)=(x,y)$, then $e(\neg{\sim}\alpha)=(1-y,1-x)$.
Furthermore, it is straightforward to verify that the following formulas are
valid.

$\displaystyle\neg{\sim}\neg\alpha$
$\displaystyle\leftrightarrow\neg\neg{\sim}\alpha$
$\displaystyle\neg{\sim\sim}\alpha$
$\displaystyle\leftrightarrow{\sim}\neg{\sim}\alpha$
$\displaystyle\neg{\sim}\triangle\alpha$
$\displaystyle\leftrightarrow\triangle\neg{\sim}\alpha$
$\displaystyle\neg{\sim}(\alpha\\!\rightarrow\\!\alpha^{\prime})$
$\displaystyle\leftrightarrow\neg{\sim}\alpha\\!\rightarrow\\!\neg{\sim}\alpha^{\prime}$

From here, it will follow that
$e^{*}(\alpha)=(1-e_{2}(\alpha),1-e_{1}(\alpha))$ for every
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$.

We consider only the last case and show that
$e(\neg{\sim}(\alpha\\!\rightarrow\\!\alpha^{\prime}))=e(\neg{\sim}\alpha\\!\rightarrow\\!\neg{\sim}\alpha^{\prime})$.

$\displaystyle e_{1}(\neg{\sim}(\alpha\\!\rightarrow\\!\alpha^{\prime}))$
$\displaystyle=e_{2}({\sim}(\alpha\\!\rightarrow\\!\alpha^{\prime}))$
$\displaystyle=1-e_{2}(\alpha\\!\rightarrow\\!\alpha^{\prime})$
$\displaystyle=1-\max(0,e_{2}(\alpha^{\prime})-e_{2}(\alpha))$
$\displaystyle=\min(1,1-e_{2}(\alpha^{\prime})+e_{2}(\alpha))$ $\displaystyle
e_{1}(\neg{\sim}\alpha\\!\rightarrow\\!\neg{\sim}\alpha^{\prime})$
$\displaystyle=\min(1,1-e_{1}(\neg{\sim}\alpha)+e_{1}(\neg{\sim}\alpha^{\prime}))$
$\displaystyle=\min(1,1-e_{2}({\sim}\alpha)+e_{2}({\sim}\alpha^{\prime}))$
$\displaystyle=\min(1,1-(1-e_{2}(\alpha))+(1-e_{2}(\alpha^{\prime})))$
$\displaystyle=\min(1,e_{2}(\alpha)+1-e_{2}(\alpha^{\prime}))$ $\displaystyle
e_{2}(\neg{\sim}(\alpha\\!\rightarrow\\!\alpha^{\prime}))$
$\displaystyle=e_{1}({\sim}(\alpha\\!\rightarrow\\!\alpha^{\prime}))$
$\displaystyle=1-e_{1}(\alpha\\!\rightarrow\\!\alpha^{\prime})$
$\displaystyle=1-\min(1,1-e_{1}(\alpha)+e_{1}(\alpha^{\prime}))$
$\displaystyle=\max(0,e_{1}(\alpha)-e_{1}(\alpha^{\prime}))$ $\displaystyle
e_{2}(\neg{\sim}\alpha\\!\rightarrow\\!\neg{\sim}\alpha^{\prime})$
$\displaystyle=\max(0,e_{2}(\neg{\sim}\alpha^{\prime})-e_{2}(\neg{\sim}\alpha))$
$\displaystyle=\max(0,e_{1}({\sim}\alpha^{\prime})-e_{1}({\sim}\alpha))$
$\displaystyle=\max(0,(1-e_{1}(\alpha^{\prime}))-(1-e_{1}(\alpha)))$
$\displaystyle=\max(0,e_{1}(\alpha^{\prime})-e_{1}(\alpha))$

The result follows.

######  Example 3.9 (Values of formulas in models).

Consider Fig. 3 with a classical probability $\mu$. Let us compute the values
of the following (atomic) formulas: $\mathsf{Pr}(p\wedge\neg q)$,
$\mathsf{Db}(p\wedge\neg q)$, and $\mathsf{Bl}(q\vee\neg q)$.

We have $|p\wedge\neg q|^{+}=\\{w_{1}\\}$ and $|p\wedge\neg
p|^{-}=\\{w_{1},w_{3}\\}$. Thus, $\mu(|p\wedge\neg q|^{+})=\frac{1}{3}$ and
$\mu(|p\wedge\neg q|^{-})=\frac{1}{2}$ which gives us
$e(\mathsf{Pr}(p\wedge\neg q))=\left(\frac{1}{3},\frac{1}{2}\right)$.
Moreover, $|p\wedge\neg q|^{\mathsf{d}}=\\{w_{3}\\}$, whence
$\mathsf{Db}(p\wedge\neg q)=\frac{1}{6}$. For $q\vee\neg q$, we have
$|q\vee\neg q|^{\mathsf{b}}=\\{w_{2}\\}$, and thus, $e(\mathsf{Bl}(q\vee\neg
q))=\frac{1}{2}$.

$\textstyle{w_{1}:p^{+},q^{\pm}}$$\textstyle{w_{2}:\xcancel{p},q^{-}}$$\textstyle{w_{3}:p^{-},\xcancel{q}}$
Figure 3: $\mu(\\{w_{1}\\})=\frac{1}{3}$, $\mu(\\{w_{2}\\})=\frac{1}{2}$,
$\mu(\\{w_{3}\\})=\frac{1}{6}$.

Before establishing faithful translations between
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$,
let us recall that in the Introduction, we mentioned that quantitative
statements about uncertainty expressed in the natural language may sound like
‘I think that rain is twice more likely than snow’. We show how to formalise
this statement.

######  Example 3.10 (Formalisation).

$\mathtt{twice}$:

I think that rain is twice more likely than snow.

We are going to translate this statement into
$\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$
and interpret ‘I am certain’ as pure belief. We denote ‘it is going to rain’
with $r$ and ‘it is going to snow’ with $s$. It remains to write down a
formula $\phi_{\mathtt{twice}}$ that has value $1$ iff $e(\mathsf{Bl}r)=2\cdot
e(\mathsf{Bl}s)$. Consider the following formula

$\displaystyle\phi_{\mathtt{twice}}$
$\displaystyle=\triangle((\mathsf{Bl}r\ominus\mathsf{Bl}s)\leftrightarrow\mathsf{Bl}s)$

Note that a more intuitive formalisation —
$\triangle(\mathsf{Bl}r\leftrightarrow(\mathsf{Bl}s\oplus\mathsf{Bl}s))$ —
would not work: $\oplus$ is a  _truncated sum_ , whence it, e.g., does not
exclude the situation with both $\mathsf{Bl}r$ and $\mathsf{Bl}s$ having value
$1$.

It is also clear that desiderata (1), (3), and (4) listed in Section 1.4 are
satisfied by both
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
and
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$.
It is less straightforward, however, to see how we can formalise preferring
one source to another (desideratum (2)). We explain this in the following
remark.

######  Remark 3.11.

To represent different sources, one can consider $\mathsf{BD}$ models with
_several measures_ , each representing a source, and, accordingly, expand the
language with other modalities corresponding to these new measures. We can
state, for example, that one source ($s_{1}$) considers $\phi$ to be more
likely than the other source ($s_{2}$) does. In
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
we can interpret this as the value of $\mathsf{Bl}_{s_{1}}\phi$ being _smaller
than_ the value of $\mathsf{Bl}_{s_{2}}\phi$. This is formalised as follows:

$\displaystyle{\sim}\triangle(\mathsf{Bl}_{s_{2}}\phi\rightarrow\mathsf{Bl}_{s_{1}}\phi)$

Unfortunately, there seems to be no direct way of representing the _degrees of
trust_ the agent assigns to $s_{1}$ and $s_{2}$ using only modalities
interpreted as measures in the Łukasiewicz setting. A traditional way (cf.,
e.g., (Shafer,, 1976, p.252)) of accounting for the degree of trust in a given
source is to multiply the value a mass function gives to $X\subseteq W$ by
some $x\in[0,1]$. Thus, to model this approach, one would need a combination
of Rational Pavelka and Product logics. Another option would be to redefine
$e(\mathsf{Bl}_{s}\phi)=(\mathsf{tr}_{s}\odot_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}\mu(|\phi|^{\mathsf{b}}))$
and similarly for other modalities (with $\mathsf{tr}_{s}\in[0,1]$ standing
for the trust in source $s$). It is unclear, however, how to axiomatise this
logic.

It is possible, though, to make different modalities stand for different types
of measures (e.g., $\mathsf{Bl}_{s_{1}}$ can be generated by a
$\mathbf{4}$-probability while $\mathsf{Bl}_{s_{2}}$ by a belief function).
This represents the _different ways of aggregating the data_ the agent can
have.

We finish the section by establishing faithful embeddings of
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
and
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
into one another. First, we introduce some technical notions that will
simplify the proof. We say that
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$
is _outer- $\neg$-free_ when $\neg$’s appear only inside modal atoms.

######  Definition 3.12.

Let
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$.
$\alpha^{\neg}$ is produced from $\alpha$ by successively applying the
following transformations.

$\displaystyle\neg\mathsf{Pr}\phi$
$\displaystyle\rightsquigarrow\mathsf{Pr}\neg\phi$
$\displaystyle\neg\neg\alpha$ $\displaystyle\rightsquigarrow\alpha$
$\displaystyle\neg{\sim}\alpha$
$\displaystyle\rightsquigarrow{\sim}\neg\alpha$
$\displaystyle\neg(\alpha\rightarrow\alpha^{\prime})$
$\displaystyle\rightsquigarrow{\sim}(\neg\alpha^{\prime}\rightarrow\neg\alpha)$
$\displaystyle\neg\triangle\alpha$
$\displaystyle\rightsquigarrow{\sim}\triangle{\sim}\neg\alpha$

It is easy to check using Definitions 3.3 and 3.6 that
$e(\alpha)=e(\alpha^{\neg})$ in every
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
model.

######  Definition 3.13.

Let
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$
be outer-$\neg$-free, we define
$\alpha^{\mathbf{4}}\in\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$
as follows.

$\displaystyle(\mathsf{Pr}\phi)^{\mathbf{4}}$
$\displaystyle=\mathsf{Bl}\phi\oplus\mathsf{Cf}\phi$
$\displaystyle(\heartsuit\alpha)^{\mathbf{4}}$
$\displaystyle=\heartsuit\alpha^{\mathbf{4}}$
($\heartsuit\in\\{\triangle,{\sim}\\}$)
$\displaystyle(\alpha\rightarrow\alpha^{\prime})^{\mathbf{4}}$
$\displaystyle=\alpha^{\mathbf{4}}\rightarrow\alpha^{\prime\mathbf{4}}$

Let
$\beta\in\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$.
We define $\beta^{\pm}$ as follows.

$\displaystyle(\mathsf{Bl}\phi)^{\pm}$
$\displaystyle=\mathsf{Pr}\phi\ominus\mathsf{Pr}(\phi\wedge\neg\phi)$
$\displaystyle(\mathsf{Cf}\phi)^{\pm}$
$\displaystyle=\mathsf{Pr}(\phi\wedge\neg\phi)$
$\displaystyle(\mathsf{Uc}\phi)^{\pm}$
$\displaystyle={\sim}\mathsf{Pr}(\phi\vee\neg\phi)$
$\displaystyle(\mathsf{Db}\phi)^{\pm}$
$\displaystyle=\mathsf{Pr}\neg\phi\ominus\mathsf{Pr}(\phi\wedge\neg\phi)$
$\displaystyle(\heartsuit\beta)^{\pm}$ $\displaystyle=\heartsuit\beta^{\pm}$
($\heartsuit\in\\{\triangle,{\sim}\\}$)
$\displaystyle(\beta\rightarrow\beta^{\prime})^{\pm}$
$\displaystyle=\beta^{\pm}\rightarrow\beta^{\prime\pm}$

######  Theorem 3.14.

$\alpha\in\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$
is
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
valid iff $(\alpha^{\neg})^{\mathbf{4}}$ is
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
valid.

######  Proof 3.15.

Let w.l.o.g. $\mathbb{M}=\langle W,v^{+},v^{-},\mu,e_{1},e_{2}\rangle$ be a
$\mathsf{BD}$ model with $\pm$-probability where $\mu$ is a _classical_
probability measure and let $e(\alpha)=(x,y)$. We show that in the
$\mathsf{BD}$ model $\mathbb{M}_{\mathbf{4}}=\langle
W,v^{+},v^{-},\mu,e_{1}\rangle$ with _four-probability_ $\mu$ and
$e^{\mathbf{4}}$ induced by $\mu$,
$e^{\mathbf{4}}((\alpha^{\neg})^{\mathbf{4}})=x$. This is sufficient to prove
the result because if $\alpha^{\neg}$ is not
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
valid, then $\alpha$ is not
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
valid either.

We proceed by induction on $\alpha^{\neg}$. For the basis case, we have that

$\displaystyle e_{1}(\mathsf{Pr}\phi)$ $\displaystyle=\mu(|\phi|^{+})$
$\displaystyle=\mu(|\phi|^{\mathsf{b}}\cup|\phi|^{\mathsf{c}})$
$\displaystyle=\mu(|\phi|^{\mathsf{b}})\cup\mu(|\phi|^{\mathsf{c}})$
($|\phi|^{\mathsf{b}}$ and $|\phi|^{\mathsf{c}}$ are disjoint)
$\displaystyle=e_{\mathbf{4}}(\mathsf{Bl}\phi)+e_{\mathbf{4}}(\mathsf{Cf}\phi)$
($e_{\mathbf{4}}$ is induced by $\mu$)
$\displaystyle=e_{\mathbf{4}}(\mathsf{Bl}\phi\oplus\mathsf{Cf}\phi)$
($e_{\mathbf{4}}(\mathsf{Bl}\phi)+e_{\mathbf{4}}(\mathsf{Cf}\phi)\leq 1$)

The cases of connectives can be obtained by an application of the induction
hypothesis.

Conversely, since the support of truth conditions in
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
coincide with the semantics of
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
(cf. Definitions 3.2 and 3.3) and since $\alpha^{\neg}$ is outer-$\neg$-free,
if $e(\alpha^{\neg})<1$ for some
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
model $\mathbb{M}_{\mathbf{4}}=\langle W,v^{+},v^{-},\mu,e\rangle$, then
$e_{1}(\alpha^{\neg})<1$ for $\mathbb{M}=\langle
W,v^{+},v^{-},\mu,e_{1},e_{2}\rangle$ with $e=e_{1}$.

We proceed by induction on $\alpha^{\neg}$ (recall that
$e(\alpha)=e(\alpha^{\neg})$ in all
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
models). If $\alpha=\mathsf{Pr}\phi$, then
$e_{1}(\mathsf{Pr}\phi)=\mu(|\phi|^{+})=\mu(|\phi|^{\mathsf{b}}\cup|\phi|^{\mathsf{c}})$.
But $|\phi|^{\mathsf{b}}$ and $|\phi|^{\mathsf{c}}$ are disjoint, whence
$\mu(|\phi|^{\mathsf{b}}\cup|\phi|^{\mathsf{c}})=\mu(|\phi|^{\mathsf{b}})+\mu(|\phi|^{\mathsf{c}})$,
and since $\mu(|\phi|^{\mathsf{b}})+\mu(|\phi|^{\mathsf{c}})\leq 1$, we have
that
$e_{1}(\mathsf{Bl}\phi\oplus\mathsf{Cf}\phi)=\mu(|\phi|^{\mathsf{b}})+\mu(|\phi|^{\mathsf{c}})=e_{1}(\mathsf{Pr}\phi)$,
as required.

The induction steps are straightforward since the semantic conditions of
support of truth in
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{\triangle}$
coincide with the semantics of
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
(cf. Definitions 3.3 and 3.2).

######  Theorem 3.16.

$\beta\in\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$
is
$\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$
valid iff $\beta^{\pm}$ is
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
valid.

######  Proof 3.17.

Assume w.l.o.g. that $\mathbb{M}=\langle
W,v^{+},v^{-},\mu_{\mathbf{4}},e\rangle$ is a $\mathsf{BD}$ model with a
$\mathbf{4}$-probability where $\mu_{\mathbf{4}}$ is a classical probability
measure and $e(\beta)=x$. It suffices to define a $\mathsf{BD}$ model with
$\pm$-probability $\mathbb{M}^{\pm}=\langle
W,v^{+},v^{-},\mu_{\mathbf{4}},e_{1},e_{2}\rangle$ and show that
$e_{1}(\beta^{\pm})=x$. If $e(\beta)<1$, then $e(\beta^{\pm})<1$ (and thus, is
not valid). If $\beta^{\pm}$ is not valid, we have that $e_{1}(\beta^{\pm})<1$
by Lemma 3.7, whence $e(\beta)<1$, as well.

We proceed by induction on $\beta$. If $\beta=\mathsf{Bl}\phi$, then
$e(\mathsf{Bl}\phi)=\mu_{\mathbf{4}}(|\phi|^{\mathsf{b}})$. Now observe that
$\mu_{\mathbf{4}}(|\phi|^{+})=\mu(|\phi|^{\mathsf{b}}\cup|\phi|^{\mathsf{c}})=\mu_{\mathbf{4}}(|\phi|^{\mathsf{b}})+\mu_{\mathbf{4}}(|\phi|^{\mathsf{c}})$
since $|\phi|^{\mathsf{b}}$ and $|\phi|^{\mathsf{c}}$ are disjoint. But
$\mu_{\mathbf{4}}(|\phi|^{+})\\!=\\!e_{1}(\mathsf{Pr}\phi)$ and
$\mu_{\mathbf{4}}(|\phi|^{\mathsf{c}})\\!=\\!\mu_{\mathbf{4}}(|\phi\\!\wedge\\!\neg\phi|^{+})$
since $|\phi\\!\wedge\\!\neg\phi|^{+}\\!=\\!|\phi|^{\mathsf{c}}$. Thus,
$\mu_{\mathbf{4}}(|\phi|^{\mathsf{b}})=e_{1}(\mathsf{Pr}\phi\ominus\mathsf{Pr}(\phi\wedge\neg\phi))$
as required.

Other basis cases of $\mathsf{Cf}\phi$, $\mathsf{Uc}\phi$, and
$\mathsf{Db}\phi$ can be tackled similarly. The induction steps are
straightforward since the support of truth in
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{\triangle}$
coincides with semantical conditions in
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$.

###  3.2 Axiomatisations

In this section, we present Hilbert-style calculi
$\mathcal{H}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
that axiomatise
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$.
The completeness of
$\mathcal{H}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
w.r.t. finite theories (Ł is not compact, whence there are no finite calculi
for expansions of Ł complete w.r.t. countable theories) was established in
Bílková et al., (2023). Here, we prove the completeness of
$\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$.

To construct the calculi we translate the conditions on measures from
Definitions 2.2 and 2.3 into
$\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$
and
$\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$
formulas. We then use these translated conditions as additional axioms that
extend Hilbert-style calculi for
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
and
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$.

To facilitate the presentation, we recall these Hilbert calculi for
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$.
The axiomatisation of
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
can be obtained by adding $\triangle$ axioms and rules from Baaz, (1996),
(Hájek,, 1998, Definition 2.4.5), or (Běhounek et al.,, 2011, Chapter I,2.2.1)
to the Hilbert-style calculus for Ł from (Metcalfe et al.,, 2008, §6.2).

######  Definition 3.18
($\mathcal{H}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
— the Hilbert-style calculus for
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$).

The calculus contains the following axioms and rules.

$\mathbf{w}$:

$\phi\rightarrow(\chi\rightarrow\phi)$.

$\mathbf{sf}$:

$(\phi\rightarrow\chi)\rightarrow((\chi\rightarrow\psi)\rightarrow(\phi\rightarrow\psi))$.

$\mathbf{waj}$:

$((\phi\rightarrow\chi)\rightarrow\chi)\rightarrow((\chi\rightarrow\phi)\rightarrow\phi)$.

$\mathbf{co}$:

$({\sim}\chi\rightarrow{\sim}\phi)\rightarrow(\phi\rightarrow\chi)$.

$\mathbf{MP}$:

$\dfrac{\phi\quad\phi\rightarrow\chi}{\chi}$.

$\triangle 1$:

$\triangle\phi\vee{\sim}\triangle\phi$.

$\triangle 2$:

$\triangle\phi\rightarrow\phi$.

$\triangle 3$:

$\triangle\phi\rightarrow\triangle\triangle\phi$.

$\triangle 4$:

$\triangle(\phi\vee\chi)\rightarrow\triangle\phi\vee\triangle\chi$.

$\triangle 5$:

$\triangle(\phi\rightarrow\chi)\rightarrow\triangle\phi\rightarrow\triangle\chi$.

$\triangle\mathbf{nec}$:

$\dfrac{\phi}{\triangle\phi}$.

######  Proposition 3.19 (Finite strong completeness of
$\mathcal{H}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$).

Let $\Gamma$ be finite. Then
$\Gamma\models_{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}\phi$
iff
$\Gamma\vdash_{\mathcal{H}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}\phi$.

The calculus for
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
is acquired by adding the axioms for $\neg$.

######  Definition 3.20
($\mathcal{H}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
— Hilbert-style calculus for
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$).

The calculus expands
$\mathcal{H}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
with the following axioms and rules.

$\neg\neg$:

$\neg\neg\phi\leftrightarrow\phi$.

$\neg{\sim}$:

$\neg{\sim}\phi\leftrightarrow{\sim}\neg\phi$.

${\sim}\neg\\!\rightarrow$:

$({\sim}\neg\phi\rightarrow{\sim}\neg\chi)\leftrightarrow{\sim}\neg(\phi\rightarrow\chi)$.

$\neg\triangle$:

$\neg\triangle\phi\leftrightarrow{\sim}\triangle{\sim}\neg\phi$.

$\mathbf{conf}$:

$\dfrac{\phi}{{\sim}\neg\phi}$.

The completeness of
$\mathcal{H}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
was shown in (Bílková et al.,, 2023, Lemma 4.16) (there, the logic is called
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}$).

The calculi for
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
are as follows.

######  Definition 3.21
($\mathcal{H}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
— a Hilbert-style calculus for
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$).

The calculus has the following axioms and rules.

${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$:

${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$-valid
formulas and
$\mathcal{H}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
rules instantiated in
$\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$;

$\pm\mathsf{mon}$:

$\mathsf{Pr}\phi\rightarrow\mathsf{Pr}\chi$ if
$\phi\models_{\mathsf{BD}}\chi$;

$\pm\mathsf{neg}$:

$\mathsf{Pr}\neg\phi\leftrightarrow\neg\mathsf{Pr}\phi$;

$\pm\mathsf{ex}$:

$\mathsf{Pr}(\phi\vee\chi)\leftrightarrow((\mathsf{Pr}\phi\ominus\mathsf{Pr}(\phi\wedge\chi))\oplus\mathsf{Pr}\chi)$.

######  Definition 3.22
($\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
— Hilbert-style calculus for
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$).

The calculus
$\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
consists of the following axioms and rules.

${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$:

${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$-valid
formulas and sound rules instantiated in
$\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$.

$\mathbf{4}\mathsf{equiv}$:

$\mathsf{X}\phi\\!\leftrightarrow\\!\mathsf{X}\chi$ for every
$\phi,\chi\\!\in\\!\mathcal{L}_{\mathsf{BD}}$ s.t.
$\phi\\!\dashv\vdash\\!\chi$ is $\mathsf{BD}$-valid and
$\mathsf{X}\\!\in\\!\\{\mathsf{Bl},\mathsf{Db},\mathsf{Cf},\mathsf{Uc}\\}$.

$\mathbf{4}\mathsf{contr}$:

${\sim}\mathsf{Bl}(\phi\wedge\neg\phi)$;
$\mathsf{Cf}\phi\leftrightarrow\mathsf{Cf}(\phi\wedge\neg\phi)$.

$\mathbf{4}\mathsf{neg}$:

$\mathsf{Bl}\neg\phi\leftrightarrow\mathsf{Db}\phi$;
$\mathsf{Cf}\neg\phi\leftrightarrow\mathsf{Cf}\phi$.

$\mathbf{4}\mathsf{mon}$:

$(\mathsf{Bl}\phi\oplus\mathsf{Cf}\phi)\rightarrow(\mathsf{Bl}\chi\oplus\mathsf{Cf}\chi)$
for every $\phi,\chi\in\mathcal{L}_{\mathsf{BD}}$ s.t. $\phi\vdash\chi$ is
$\mathsf{BD}$-valid.

$\mathbf{4}\mathsf{part1}$:

$\mathsf{Bl}\phi\oplus\mathsf{Db}\phi\oplus\mathsf{Cf}\phi\oplus\mathsf{Uc}\phi$.

$\mathbf{4}\mathsf{part2}$:

$((\mathsf{X}_{1}\phi\oplus\mathsf{X}_{2}\phi\oplus\mathsf{X}_{3}\phi\oplus\mathsf{X}_{4}\phi)\ominus\mathsf{X}_{4}\phi)\leftrightarrow(\mathsf{X}_{1}\phi\oplus\mathsf{X}_{2}\phi\oplus\mathsf{X}_{3}\phi)$
with $\mathsf{X}_{i}\neq\mathsf{X}_{j}$,
$\mathsf{X}_{i}\in\\{\mathsf{Bl},\mathsf{Db},\mathsf{Cf},\mathsf{Uc}\\}$.

$\mathbf{4}\mathsf{ex}$:

$(\mathsf{Bl}(\phi\vee\chi)\oplus\mathsf{Cf}(\phi\vee\chi))\leftrightarrow((\mathsf{Bl}\phi\oplus\mathsf{Cf}\phi)\ominus(\mathsf{Bl}(\phi\wedge\chi)\oplus\mathsf{Cf}(\phi\wedge\chi))\oplus(\mathsf{Bl}\chi\oplus\mathsf{Cf}\chi))$.

As one can see, the axioms in the calculi above are translations of properties
from Definitions 2.2 and 2.3. In
$\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$,
we split $\mathbf{4}\mathbf{part}$ in two axioms to ensure that the values of
$\mathsf{Bl}\phi$, $\mathsf{Db}\phi$, $\mathsf{Cf}\phi$, and $\mathsf{Uc}\phi$
sum up exactly to $1$. Note, moreover, that $\mathbf{4}\mathsf{mon}$ and
$\mathbf{4}\mathsf{ex}$ are translations of $\pm\mathsf{mon}$ and
$\pm\mathsf{ex}$ (cf. Definition 3.13).

In the remainder of this section, we prove the completeness of
$\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
w.r.t. finite theories.

######  Theorem 3.23.

Let
$\Xi\subseteq\mathcal{L}_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}$
be finite. Then
$\Xi\models_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}\alpha$
iff
$\Xi\vdash_{\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}\alpha$.

######  Proof 3.24.

Soundness can be established by the routine check of the validity of the
axioms. E.g., for $\mathbf{4}\mathsf{equiv}$, observe that if $\phi$ and
$\chi$ are equivalent in $\mathsf{BD}$, then $|\phi|^{+}=|\chi|^{+}$ and
$|\phi|^{-}=|\chi|^{-}$, whence $|\phi|^{\mathsf{x}}=|\chi|^{\mathsf{x}}$ for
every $\mathsf{x}\in\\{\mathsf{b},\mathsf{d},\mathsf{c},\mathsf{u}\\}$. Thus,
$e(\mathsf{X}\phi)=e(\mathsf{X}\chi)$ for each
$\mathsf{X}\in\\{\mathsf{Bl},\mathsf{Db},\mathsf{Cf},\mathsf{Uc}\\}$, from
where $\mathsf{X}\phi\leftrightarrow\mathsf{X}\chi$ is valid.
$\mathbf{4}\mathsf{contr}$, $\mathbf{4}\mathsf{neg}$, and
$\mathbf{4}\mathsf{mon}$ are straightforward translations of $\mathbf{contr}$,
$\mathbf{neg}$, and $\mathbf{BCmon}$. $\mathbf{4}\mathsf{ex}$ is the
translation of $\pm\mathsf{ex}$, whence are valid by Theorem 3.14.

Last, consider $\mathbf{4}\mathsf{part1}$ and $\mathbf{4}\mathsf{part2}$. We
have
$\sum\limits_{\mathsf{x}\in\\{\mathsf{b},\mathsf{d},\mathsf{c},\mathsf{u}\\}}\\!\\!\\!\\!|\phi|^{\mathsf{x}}=1$.
Hence,
$\sum\limits_{\mathsf{X}\in\\{\mathsf{Bl},\mathsf{Db},\mathsf{Cf},\mathsf{Uc}\\}}\\!\\!\\!\\!e(\mathsf{X}\phi)=1$.
Thus, we have that $\mathbf{4}\mathsf{part1}$ and $\mathbf{4}\mathsf{part2}$
are valid.

Let us now prove the completeness. We reason by contraposition. Assume that
$\Xi\nvdash_{\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}\alpha$.
Now, observe that
$\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
proofs are, actually,
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
proofs with additional probabilistic axioms. Let $\Xi^{*}$ stand for $\Xi$
extended with probabilistic axioms built over all pairwise non-equivalent
$\mathcal{L}_{\mathsf{BD}}$ formulas constructed from
$\mathtt{Prop}[\Xi\cup\\{\alpha\\}]$. Clearly,
$\Xi^{*}\nvdash_{\mathcal{H}\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}\alpha$
either. Moreover, $\Xi^{*}$ is finite as well since $\mathsf{BD}$ is tabular
(and whence, there exist only finitely many pairwise non-equivalent
$\mathcal{L}_{\mathsf{BD}}$ formulas over a finite set of variables). Now, by
the weak completeness of
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
(Proposition 3.19), there exists an
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
valuation $e$ s.t. $e[\Xi^{*}]=1$ and $e(\alpha)\neq 1$.

It remains to construct a
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$-model
$\mathbb{M}$ falsifying
$\Xi^{*}\models_{\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}}\alpha$
using $e$. We proceed as follows. First, we set
$W=2^{\mathsf{Lit}[\Xi^{*}\cup\\{\alpha\\}]}$, and for every $w\in W$ define
$w\in v^{+}(p)$ iff $p\in w$ and $w\in v^{-}(p)$ iff $\neg p\in w$. We extend
the valuations to $\phi\in\mathcal{L}_{\mathsf{BD}}$ in the usual manner.
Then, for $\mathsf{X}\phi\in\mathtt{Sf}[\Xi^{*}\cup\\{\alpha\\}]$, we set
$\mu_{\mathbf{4}}(|\phi|^{\mathsf{x}})=e(\mathsf{X}\phi)$ according to
modality $\mathsf{X}$.

It remains to extend $\mu_{\mathbf{4}}$ to the whole $2^{W}$. Observe,
however, that any map from $2^{W}$ to $[0,1]$ that extends $\mu_{\mathbf{4}}$
is, in fact, a $\mathbf{4}$-probability. Indeed, all requirements from
Definition 2.3 concern _only the extensions of formulas_. But the model is
finite, $\mathsf{BD}$ is tabular, and $\Xi^{*}$ contains all the necessary
instances of probabilistic axioms and $e[\Xi^{*}]=1$, whence all constraints
on the formulas are satisfied.

###  3.3 Complexity

Let us now establish the complexity of
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$.
Namely, we prove their $\mathsf{NP}$-completeness. Since the mutual embeddings
given in Definition 3.13 result in an at most linear increase in the size of
the formulas, it suffices to consider only one of them. In this section, we
choose to give a non-deterministic polynomial algorithm for
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
since it contains only one modality which will simplify the presentation.
Note, furthermore, that
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
(and thus,
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$)
are $\mathsf{NP}$-hard, thus,
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
are $\mathsf{NP}$-hard as well. Thus, we only need to establish the upper
bound.

For the proof, we adapt constraint tableaux for
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}$
defined in Bílková et al., (2021) and expand them with rules for $\triangle$.
We then adapt the $\mathsf{NP}$-completeness proof of
$\mathsf{FP}({\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}})$
from Hájek and Tulipani, (2001) to establish our result.

######  Definition 3.25 (Constraint tableaux for
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
—
$\mathcal{T}\\!\\!\left({\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}\right)$).

Branches contain _labelled formulas_ of the form $\phi\leqslant_{1}i$,
$\phi\leqslant_{2}i$, $\phi\geqslant_{1}i$, or $\phi\geqslant_{2}i$, and
_numerical constraints_ of the form $i\leq j$ with $i$ and $j$ (labels) being
linear polynomials over $[0,1]$. Each branch can be extended by an application
of a rule below.

$\displaystyle\neg\\!\leqslant_{1}\\!\dfrac{\neg\phi\leqslant_{1}i}{\phi\leqslant_{2}i}$
$\displaystyle\neg\\!\leqslant_{2}\\!\dfrac{\neg\phi\leqslant_{2}i}{\phi\leqslant_{1}i}$
$\displaystyle\neg\\!\geqslant_{1}\\!\dfrac{\neg\phi\geqslant_{1}i}{\phi\geqslant_{2}i}$
$\displaystyle\neg\\!\geqslant_{2}\\!\dfrac{\neg\phi\geqslant_{2}i}{\phi\geqslant_{1}i}$
$\displaystyle{\sim}\\!\leqslant_{1}\\!\dfrac{{\sim}\phi\leqslant_{1}i}{\phi\geqslant_{1}1-i}$
$\displaystyle{\sim}\\!\leqslant_{2}\\!\dfrac{{\sim}\phi\leqslant_{2}i}{\phi\geqslant_{2}1-i}$
$\displaystyle{\sim}\\!\geqslant_{1}\\!\dfrac{{\sim}\phi\geqslant_{1}i}{\phi\leqslant_{1}1-i}$
$\displaystyle{\sim}\\!\geqslant_{2}\\!\dfrac{{\sim}\phi\geqslant_{2}i}{\phi\leqslant_{2}1-i}$
$\displaystyle\triangle\\!\geqslant_{1}\\!\dfrac{\triangle\phi\geqslant_{1}i}{i\leq
0\left|\begin{matrix}\phi\geqslant_{1}j\\\ j\geq 1\end{matrix}\right.}$
$\displaystyle\triangle\\!\leqslant_{1}\\!\dfrac{\triangle\phi\leqslant_{1}i}{i\geq
1\left|\begin{matrix}\phi\leqslant_{1}j\\\ j<1\end{matrix}\right.}$
$\displaystyle\triangle\\!\leqslant_{2}\\!\dfrac{\triangle\phi\leqslant_{2}i}{i\geq
1\left|\begin{matrix}\phi\leqslant j\\\ j\leq 0\end{matrix}\right.}$
$\displaystyle\triangle\\!\geqslant_{2}\\!\dfrac{\triangle\phi\geqslant_{2}i}{i\leq
0\left|\begin{matrix}\phi\geqslant j\\\ j>0\end{matrix}\right.}$
$\displaystyle\rightarrow\leqslant_{1}\dfrac{\phi_{1}\rightarrow\phi_{2}\leqslant_{1}i}{i\\!\geq\\!1\left|\begin{matrix}\phi_{1}\\!\geqslant_{1}\\!1\\!-\\!i\\!+\\!j\\\
\phi_{2}\leqslant_{1}j\\\ j\leq i\end{matrix}\right.}$
$\displaystyle\rightarrow\leqslant_{2}\dfrac{\phi_{1}\\!\rightarrow\\!\phi_{2}\\!\leqslant_{2}\\!i}{\begin{matrix}\phi_{1}\geqslant_{2}j\\\
\phi_{2}\\!\leqslant_{2}\\!i\\!+\\!j\end{matrix}}$
$\displaystyle\rightarrow\geqslant_{1}\dfrac{\phi_{1}\\!\rightarrow\\!\phi_{2}\geqslant_{1}i}{\begin{matrix}\phi_{1}\\!\leqslant_{1}\\!1\\!-\\!i\\!+\\!j\\\
\phi_{2}\geqslant_{1}j\end{matrix}}$
$\displaystyle\rightarrow\geqslant_{2}\dfrac{\phi_{1}\rightarrow\phi_{2}\geqslant_{2}i}{i\\!\leq\\!0\left|\begin{matrix}\phi_{1}\\!\leqslant_{2}\\!j\\\
\phi_{2}\\!\geqslant_{2}\\!i\\!+\\!j\\\ j\leq 1-i\end{matrix}\right.}$

Let $i$’s be linear polynomials that label the formulas in the branch and
$x$’s be variables ranging over $[0,1]$. We define the translation
$\mathcal{t}$ from labelled formulas to linear inequalities as follows:

$\displaystyle\mathcal{t}(\phi\leqslant_{1}i)=x_{\phi}^{L}\leq i;$
$\displaystyle\mathcal{t}(\phi\geqslant_{1}i)=x_{\phi}^{L}\geq i;$
$\displaystyle\mathcal{t}(\phi\leqslant_{2}i)=x_{\phi}^{R}\leq i;$
$\displaystyle\mathcal{t}(\phi\geqslant_{2}i)=x_{\phi}^{R}\geq i$

Let
$\triangledown\in\\{\leqslant_{1},\geqslant_{1},\leqslant_{2},\geqslant_{2}\\}$.
A tableau branch

$\mathcal{B}=\\{\phi_{1}\triangledown i_{1},\ldots,\phi_{m}\triangledown
i_{m},k_{1}\leq l_{1},\ldots,k_{q}\leq l_{q}\\}$

is _closed_ if the system of inequalities

$\mathcal{B}^{\mathcal{t}}=\\{\mathcal{t}(\phi_{1}\triangledown
i_{1}),\ldots,\mathcal{t}(\phi_{m}\triangledown i_{m}),k_{1}\leq
l_{1},\ldots,k_{q}\leq l_{q}\\}$

does not have solutions. Otherwise, $\mathcal{B}$ is _open_. If no rule
application adds new entries to $\mathcal{B}$, it is called _complete_. A
tableau is _closed_ if all its branches are closed. $\phi$ has a
_$\mathcal{T}\\!\\!\left({\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}\right)$
proof_ if the tableau beginning with $\\{\phi\leqslant_{1}c,c<1\\}$ is closed.

######  Remark 3.26.

Note that our tableaux rules are _necessarily branching_ in contrast to the
rules proposed by Hähnle, (1992, 1994). This is because all connectives of Ł
are continuous. On the other hand, $\triangle$ is not continuous, hence, there
cannot be a non-branching rule for it.

######  Definition 3.27 (Satisfying valuation of a branch).

Let $v_{1}$ and $v_{2}$ be
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
valuations. $v_{1}$  _satisfies_ a labelled formula $\phi\leqslant_{1}i$
($v_{2}$ satisfies $\phi\geqslant_{2}i$) iff $v_{\mathrm{1}}(\phi)\leq i$
(resp., $v_{2}(\phi)\geq i$). $v_{1}$  _satisfies_ a branch $\mathcal{B}$ iff
$v_{1}$  _satisfies_ any labelled formula in $\mathcal{B}$ (and similarly for
$v_{2}$). A branch $\mathcal{B}$ is _satisfiable_ iff there is a pair of
valuations $\langle v_{1},v_{2}\rangle$ that satisfies it.

######  Theorem 3.28 (Completeness of tableaux).

  1. 1.

$\phi$ is
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
valid iff it has a
$\mathcal{T}\\!\\!\left({\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}\right)$
proof.

  2. 2.

$\phi$ is
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
valid iff it has a
$\mathcal{T}\\!\\!\left({\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}\right)$
proof.

######  Proof 3.29.

The proof follows (Bílková et al.,, 2021, Theorem 1). For soundness, we show
that if $\langle v_{1},v_{2}\rangle$ satisfies the premise of a rule, then it
also satisfies one of its conclusions. We consider the case of
$\triangle\\!\geqslant_{1}$ (the rules for other connectives are tackled in
Bílková et al., (2021); the remaining rules for $\triangle$ can be dealt with
analogously).

Let $\triangle\phi\geqslant_{1}i$ be satisfied by $\langle
v_{1},v_{2}\rangle$. Then, $v_{1}(\triangle\phi)\geqslant i$. We have two
cases: (i) $i=0$ and (ii) $i>0$. In the first case, the left conclusion is
satisfied. In the second case, $v_{1}(\triangle\phi)=1$. Hence,
$v_{1}(\phi)=1$, i.e., the right conclusion is satisfied.

For completeness, note from (Bílková et al.,, 2021, Proposition 1) that $\phi$
is
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$-valid
iff $v_{1}(\phi)=1$ for every $v$. Let us now show that every complete open
branch can be satisfied. Assume that $\mathcal{B}$ is a complete open branch.
We construct the satisfying valuation as follows. Let
$\triangledown\\!\in\\!\\{\leqslant_{1},\geqslant_{1},\leqslant_{2},\geqslant_{2}\\}$
and $p_{1},\ldots,p_{m}$ be the propositional variables appearing in the
atomic labelled formulas in $\mathcal{B}$.

Let $\\{p_{1}\triangledown j_{1},\ldots,p_{m}\triangledown j_{n}\\}$ and
$\\{k_{1}\leq l_{1},\ldots,k_{q}\leq l_{q}\\}$ be the sets of all atomic
labelled formulas and all numerical constraints in $\mathcal{B}$. Notice that
one variable might appear in many atomic labelled formulas, hence we might
have $m\neq n$. Since $\mathcal{B}$ is complete and open, the following system
of linear inequalities over the set of variables
$\\{x_{p_{1}}^{L},x_{p_{1}}^{R},\ldots,x_{p_{m}}^{L},x_{p_{m}}^{R}\\}$ must
have at least one solution under the constraints listed:

$\mathcal{t}(p_{1}\triangledown i_{1}),\ldots,\mathcal{t}(p_{m}\triangledown
i_{n}),k_{1}\leq l_{1},\ldots,k_{q}\leq l_{q}$

Let $c=(c^{L}_{1},c^{R}_{1},\ldots,c^{L}_{m},c^{R}_{m})$ be a solution to the
above system of inequalities such that $c^{L}_{j}$ ($c^{R}_{j}$) is the value
of $x_{p_{j}}^{L}$ ($x_{p_{j}}^{R}$). Define valuations as follows:
$v_{1}(p_{j})=c^{L}_{j}$ and $v_{2}(p_{j})=c^{R}_{j}$.

It remains to show by induction on $\phi$ that all formulas present at
$\mathcal{B}$ are satisfied by $v_{1}$ and $v_{2}$. The basis case of
variables holds by the construction of $v_{1}$ and $v_{2}$. We consider the
case of $\triangle\phi\geqslant_{1}i$ (the cases of other variables can be
dealt with similarly).

Assume that $\triangle\phi\geqslant_{1}i\in\mathcal{B}$. Since $\mathcal{B}$
is complete and open, we have that either (i) $i\leq 0\in\mathcal{B}$ or (ii)
$\\{\phi\geqslant_{1}j,j\geq 1\\}\subseteq\mathcal{B}$. In the first case,
since there is a solution for $\mathcal{B}^{\mathcal{t}}$, we have that $i=0$,
and thus $\triangle\phi\geqslant_{1}i$ is satisfied by any $v_{1}$. In the
second case, we have that $\\{\phi\geqslant_{1}j,j\geq 1\\}$ is satisfied by
the induction hypothesis, whence $v_{1}(\phi)=1$, and thus,
$v_{1}(\triangle\phi)=1$, as required.

######  Definition 3.30 (Mixed-integer problem).

Let $\mathbf{x}=(x_{1},\ldots,x_{k})\in\mathbb{R}^{k}$ and
$\mathbf{y}=(y_{1},\ldots,y_{m})\in\mathbb{Z}^{m}$ be variables, $A$ and $B$
be integer matrices and $h$ an integer vector, and $f(\mathbf{x},\mathbf{y})$
be a $k+m$-place linear function.

  1. 1.

_A general MIP_ is to find $\mathbf{x}$ and $\mathbf{y}$ s.t.
$f(\mathbf{x},\mathbf{y})=\min\\{f(\mathbf{x},\mathbf{y}):A\mathbf{x}+B\mathbf{y}\geq
h\\}$.

  2. 2.

_A bounded MIP (bMIP)_ is to find all solutions that belong to $[0,1]$.

######  Proposition 3.31.

Bounded MIP is $\mathsf{NP}$-complete.

######  Remark 3.32.

The proof of Ł $\mathsf{NP}$-completeness by Hähnle, (1992, 1994) uses the
reduction of a Łukasiewicz formula $\phi$ to _one_ instance of a bMIP of the
size $O(\mathcal{l}(\phi))$. This is because the rules are _linear_. In our
case (cf. Remark 3.26), we cannot avoid branching. This, however, does not
affect the complexity of
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
and
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$:
indeed, bMIP is in $\mathsf{NP}$, and we can just non-deterministically guess
one branch of our tableau and then guess the solution. It is easy to see that
the lengths of branches are polynomial in $\mathcal{l}(\phi)$, and thus, we
can _verify the guessed solution_ in polynomial time, as required. If the
solution is correct, the branch is open. Thus,
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}$
and
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
are also $\mathsf{NP}$-complete.

Let us now proceed to the proof of $\mathsf{NP}$-completeness of
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$.
First, we show that we can _completely remove_ $\neg$’s from
$\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$
formulas while preserving their satisfiability.

######  Lemma 3.33.

For any outer-$\neg$-free
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$,
there exists $\alpha^{*}$ where $\neg$ does not occur at all s.t. $\alpha$ is
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-satisfiable
iff $\alpha^{*}$ is
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-satisfiable.

######  Proof 3.34.

We construct $\alpha^{*}$ as follows. First, we take every modal atom
$\mathsf{Pr}\phi$ and replace $\phi$ with its $\neg$ $\mathsf{NNF}$. Second,
we replace every literal $\neg p$ occurring in
$\mathsf{Pr}(\mathsf{NNF}(\phi))$ with $p^{*}$. Outer-layer connectives remain
the same. Observe, that this transformation increases the number of symbols in
$\alpha$ _at most linearly_. It remains to check that satisfiability is
preserved.

Let $e(\alpha)=(1,0)$ at some
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-model.
By Lemma 3.7, this is equivalent to $e_{1}(\alpha)=1$ in some
$\mathbb{M}=\langle W,v^{+},v^{-},\mu,e_{1},e_{2}\rangle$. Now, let
$\mathbb{M}^{*}=\langle
W,{v^{*}}^{+},{v^{*}}^{-},\mu,e^{*}_{1},e^{*}_{2}\rangle$ and, in particular,
$v^{-}(p)={v^{*}}^{+}(p^{*})$. It suffices to show that
$e_{1}(\alpha)=e^{*}_{1}(\alpha^{*})$.

We proceed by induction on $\alpha$. Let $\alpha=\mathsf{Pr}\phi$ for some
$\phi\in\mathcal{L}_{\mathsf{BD}}$. We have that
$e_{1}(\alpha)=\mu(|\phi|^{+})=\mu(|\mathsf{NNF}(\phi)|^{+})$. We check that
$|\mathsf{NNF}(\phi)|^{+}=|\mathsf{NNF}(\phi)^{*}|^{+}$ by induction on
$\mathsf{NNF}(\phi)$. The basis cases of variables and literals hold by the
construction of $\mathbb{M}^{*}$. The cases of $\wedge$ and $\vee$ hold by the
induction hypothesis. It follows now that
$|\mathsf{NNF}(\phi)|^{+}=|\mathsf{NNF}(\phi)^{*}|$ and thus,
$e_{1}(\mathsf{Pr}\phi)=e^{*}_{1}(\mathsf{Pr}(\mathsf{NNF}(\phi)^{*}))$. The
cases of
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
connectives can be proven by a straightforward application of the induction
hypothesis.

For the converse, assume that $\alpha^{*}$ is
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-satisfiable.
Hence, $e_{1}(\alpha^{*})=1$ in some model $\mathbb{M}=\langle
W,v^{+},v^{-},\mu,e_{1},e_{2}\rangle$. We define $\mathbb{M}^{\prime}=\langle
W,v^{\prime+},v^{\prime-},\mu,e^{\prime}_{1},e^{\prime}_{2}\rangle$ with
$v^{\prime-}(p)=v^{+}(p^{*})$ and $v^{\prime+}(p)=v^{+}(p)$. We can now show
that $e_{1}(\alpha)=e^{*}_{1}(\alpha^{*})$ as in the previous case. The result
follows.

We can now apply this lemma to adapt the proof of the
$\mathsf{NP}$-completeness of
$\mathsf{FP}({\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}})$.

######  Theorem 3.35.

Satisfiability of
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
is $\mathsf{NP}$-complete.

######  Proof 3.36.

Recall that
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathbf{4}\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}_{\triangle}}$
can be linearly embedded into one another (Theorems 3.14 and 3.16). Thus, it
remains to provide a non-deterministic polynomial algorithm for one of these
logics. We choose
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
since it has only one modality.

Let
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$
be over modal atoms $\mathsf{Pr}\phi_{1}$, …, $\mathsf{Pr}\phi_{n}$. By Lemma
3.33, we can w.l.o.g. assume that $\alpha$ does not contain $\neg$. We show
how to construct a satisfying
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-valuation
for $\alpha$.

First, we replace every modal atom $\mathsf{Pr}\phi_{i}$ with a fresh variable
$q_{\phi_{i}}$. Denote the new formula $\alpha^{-}$. It is clear that
$\mathcal{l}(\alpha^{-})$ is at most linearly greater than
$\mathcal{l}(\alpha)$. We construct a
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
tableau beginning with $\\{\alpha^{-}\geqslant_{1}c,c\geq 1\\}$. As
$\alpha^{-}$ does not contain $\neg$, every branch gives us an instance of a
bMIP (recall Definition 3.30) equivalent to the
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$-satisfiability
of $\alpha^{-}$: $\alpha^{-}$ is
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$-satisfiable
iff at least one instance of a bMIP has a solution. Clearly, if $\alpha^{-}$
is not
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$-satisfiable,
it is not
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-satisfiable
either.

Now let $\mathfrak{Br}=\\{\mathcal{B}_{1},\ldots,\mathcal{B}_{w}\\}$ be the
set of all open branches in the
$\mathcal{T}\\!\\!\left({\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}\right)$
tableau for $\alpha^{-}$. We guess a $\mathcal{B}\in\mathfrak{Br}$ and
consider the following instance of bMIP:

$\displaystyle z_{1}\triangledown t_{1},\ldots,z_{n}\triangledown
t_{n},k_{1}\leq k^{\prime}_{1},\ldots,k_{r}\leq k^{\prime}_{r},m_{1}\geq
1,\ldots,m_{s}\geq 1,m^{\prime}_{1}\leq 0,\ldots,m^{\prime}_{t}\leq 0$
($[\mathrm{MIP}(1)]^{\mathcal{B}}$)

Here, $z_{i}$’s correspond to the values of $q_{\phi_{i}}$’s in $\alpha^{-}$,
and $t_{i}$’s are linear polynomials that label $q_{\phi_{i}}$’s. Numerical
constraints give us $k$’s, $k^{\prime}$’s, $m$’s and $m^{\prime}$’s. Denote
the number of inequalities and the number of variables in
$[\mathrm{MIP}(1)]^{\mathcal{B}}$ with $l_{1}$ and $l_{2}$, respectively. It
is clear that $l_{1}=O(\mathcal{l}(\alpha^{-}))$ and
$l_{2}=O(\mathcal{l}(\alpha^{-}))$.

We need to check whether $z_{i}$’s are coherent as probabilities of
$\phi_{i}$’s. Recall again that because of (Klein et al.,, 2021, Theorem 4),
we can assume that the probabilities are _classical_. Moreover, we can assume
that there are $n$ propositional variables in $\alpha$ (we can always add new
superfluous variables or modal atoms to $\alpha$ to make their numbers equal).

Now, introduce $2^{n}$ variables $u_{v}$ indexed by $n$-letter words over
$\\{0,1\\}$. These denote whether the variables of $\phi_{i}$’s are true under
$v^{+}$ and thus, correspond to subsets of $\mathtt{Prop}(\alpha)$. E.g., if
$\mathtt{Prop}(\alpha)=\\{p_{1},p_{2},p_{3},p_{4}\\}$, then $u_{1001}$ encodes
$\\{p_{1},p_{4}\\}$. Note that $\neg$ does not occur in $\alpha^{-}$ and thus
we care only about $e_{1}$ and $v^{+}$. Furthermore, while $n$ is the number
of $\phi_{i}$’s, we can add extra modal atoms or variables to make it also the
number of variables. We let $a_{i,v}=1$ when $\phi_{i}$ is true under $v^{+}$
and $a_{i,v}=0$ otherwise. Now add new equalities to
$[\mathrm{MIP}(1)]^{\mathcal{B}}$, namely

$\displaystyle\sum_{v}u_{v}$ $\displaystyle=1$
$\displaystyle\sum_{v}(a_{i,v}\cdot u_{v})$ $\displaystyle=z_{i}$
($[\mathrm{MIP}(2\exp)]^{\mathcal{B}}$)

The new problem —
$[\mathrm{MIP}(1)]^{\mathcal{B}}$$\cup$$[\mathrm{MIP}(2\exp)]^{\mathcal{B}}$ —
has a solution over $[0,1]$ iff $\alpha$ is
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-satisfiable
since $[\mathrm{MIP}(2\exp)]^{\mathcal{B}}$ encodes a measure on
$\mathtt{Prop}(\alpha)$ while the existence of a solution for
$[\mathrm{MIP}(1)]^{\mathcal{B}}$ ensures that $\alpha$ is
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$-satisfiable.
Furthermore, although there are $l_{2}+2^{n}+n$ variables in
$[\mathrm{MIP}(1)]^{\mathcal{B}}$$\cup$$[\mathrm{MIP}(2\exp)]^{\mathcal{B}}$,
it has no more than $l_{1}+n+1$ (in)equalities. Thus by (Fagin et al.,, 1990,
Lemma 2.5), it has a solution with at most $l_{1}+n+1$ non-zero entries. We
guess a list $L$ of at most $l_{1}+n+1$ words $v$ (its size is
$n\cdot(l_{1}+n+1)$). We can now compute the values of $a_{i,v}$’s for $i\leq
n$ and $v\in L$ and obtain a new bMIP

$\displaystyle\sum_{v\in L}u_{v}$ $\displaystyle=1$ $\displaystyle\sum_{v\in
L}(a_{i,v}\cdot u_{v})$ $\displaystyle=z_{i}$
($[\mathrm{MIP}(2\mathrm{poly})]^{\mathcal{B}}$)

It is clear that
$[\mathrm{MIP}(1)]^{\mathcal{B}}$$\cup$$[\mathrm{MIP}(2\mathrm{poly})]^{\mathcal{B}}$
is of polynomial size w.r.t. $\mathcal{l}(\alpha^{-})$ and thus, can be solved
in the nondeterministic polynomial time. Moreover,
$[\mathrm{MIP}(1)]^{\mathcal{B}}$$\cup$$[\mathrm{MIP}(2\mathrm{poly})]^{\mathcal{B}}$
has a solution iff the values of $\mathsf{Pr}\phi_{i}$’s occurring on
$\mathcal{B}$ are coherent as probabilities. If there is no solution for
$[\mathrm{MIP}(1)]^{\mathcal{B}}$$\cup$$[\mathrm{MIP}(2\mathrm{poly})]^{\mathcal{B}}$,
we guess another open branch from the tableau and repeat the procedure. If
there is no open branch $\mathcal{B}^{\prime}\in\mathfrak{Br}$ s.t. its
corresponding system of inequalities
$[\mathrm{MIP}(1)]^{\mathcal{B}^{\prime}}\cup[\mathrm{MIP}(2\mathrm{poly})]^{\mathcal{B}^{\prime}}$
has a solution, then $\alpha^{-}$ is
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-unsatisfiable,
and hence, $\alpha$ is not
$\mathsf{Pr}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$-satisfiable
either by Lemma 3.33.

##  4 Belief and plausibility functions over $\mathsf{BD}$

In this section, we introduce $\mathsf{BD}$-models with belief and
plausibility functions. We adapt the definitions from Zhou, (2013) and Bílková
et al., (2023).

######  Definition 4.1 (Belief function).

A  _belief function_ on $W\neq\varnothing$ is a map
$\mathtt{bel}:2^{W}\rightarrow[0,1]$ s.t.

  * •

$\mathtt{bel}$ is monotone w.r.t. $\subseteq$: if $X\subseteq Y$, then
$\mathtt{bel}(X)\leq\mathtt{bel}(Y)$;

  * •

for every $X_{1},\ldots,X_{k}\subseteq W$, it holds that

$\displaystyle\mathtt{bel}\left(\bigcup\limits_{1\leq i\leq k}X_{i}\right)$
$\displaystyle\geq\sum\limits_{\scriptsize{\begin{matrix}J\subseteq\\{1,\ldots,k\\}\\\
J\neq\varnothing\end{matrix}}}(-1)^{|J|+1}\cdot\mathtt{bel}\left(\bigcap\limits_{j\in
J}X_{j}\right)$

  * •

$\mathtt{bel}(\varnothing)=0$ and $\mathtt{bel}(W)=1$.

######  Definition 4.2 (Plausibility function).

A  _plausibility function_ on $W\\!\neq\\!\varnothing$ is a map
$\mathtt{pl}\\!:\\!2^{W}\\!\rightarrow\\![0,1]$ s.t.

  * •

$\mathtt{pl}$ is monotone w.r.t. $\subseteq$;

  * •

for every $X_{1},\ldots,X_{k}\subseteq W$, it holds that

$\displaystyle\mathtt{pl}\left(\bigcap\limits_{1\leq i\leq
k}X_{i}\right)\leq\sum\limits_{\scriptsize{\begin{matrix}J\subseteq\\{1,\ldots,k\\}\\\
J\neq\varnothing\end{matrix}}}(-1)^{|J|+1}\cdot\mathtt{pl}\left(\bigcup\limits_{j\in
J}X_{j}\right)$

  * •

$\mathtt{pl}(\varnothing)=0$ and $\mathtt{pl}(W)=1$.

Recall that every plausibility function $\mathtt{pl}$ on $W$ gives rise to a
belief function $\mathtt{bel}_{\mathtt{pl}}$ and vice versa: given a belief
function $\mathtt{bel}$ on $W$, one can construct a plausibility function
$\mathtt{pl}_{\mathtt{bel}}$.

$\displaystyle\mathtt{pl}_{\mathtt{bel}}(X)$
$\displaystyle=1-\mathtt{bel}(W\setminus X)$
$\displaystyle\mathtt{bel}_{\mathtt{pl}}(X)$
$\displaystyle=1-\mathtt{pl}(W\setminus X)$ (3)

Moreover, it was shown in (Bílková et al.,, 2023, Lemmas 2.10 and 2.11) that a
similar statement holds for $\mathsf{BD}$-models. I.e., belief and
plausibility functions can be defined via one another even without set-
theoretic complements.

$\displaystyle\mathtt{pl}_{\mathtt{bel}}(|\phi|^{+})$
$\displaystyle=1-\mathtt{bel}(|\phi|^{-})$
$\displaystyle\mathtt{bel}_{\mathtt{pl}}(|\phi|^{+})$
$\displaystyle=1-\mathtt{pl}(|\phi|^{-})$ (4)

In what follows, we will be using two kinds of $\mathsf{BD}$ models with
belief functions introduced in Bílková et al., (2023): in the first one,
belief and plausibility will be interdefinable via (4); in the second one, we
will assume them to be independent.

######  Definition 4.3 ($\mathsf{BD}$ $\mathtt{bel}$-models).

A $\mathsf{BD}$ $\mathtt{bel}$-model is a tuple
$\mathfrak{M}_{\mathtt{bel}}=\langle\mathfrak{M},\mathtt{bel}\rangle$ with
$\mathfrak{M}$ being a $\mathsf{BD}$ model (recall Definition 2.1) and
$\mathtt{bel}$ a belief function on $W$.

######  Definition 4.4 ($\mathsf{BD}$ $\mathtt{bel}/\mathtt{pl}$-models).

A $\mathsf{BD}$ $\mathtt{bel}/\mathtt{pl}$-model is a tuple
$\mathfrak{M}_{\mathtt{bel}/\mathtt{pl}}=\langle\mathfrak{M},\mathtt{bel},\mathtt{pl}\rangle$
with $\mathfrak{M}$ being a $\mathsf{BD}$ model (recall Definition 2.1),
$\mathtt{bel}$ a belief function on $W$, and $\mathtt{pl}$ a plausibility
function on $W$.

Observe from Definitions 4.1 and 4.2 that the traditional axiomatisation of
belief and plausibility functions is infinite. In the classical case, this can
be circumvented following Godo et al., (2001, 2003) if we define belief in
$\phi$ as _the probability of $\Box\phi$_ (with $\Box$ being the $\mathbf{S5}$
modality). Then, we can use (3) to define the plausibility of $\phi$ as _the
probability of $\lozenge\phi$_ since $\lozenge\phi\equiv{\sim}\Box{\sim}\phi$
(here, $\equiv$ is the classical equivalence and ${\sim}$ is the classical
negation). In the remainder of the section, we show that the same can be done
in $\mathsf{BD}$.

Let us first recall the classical result.

######  Definition 4.5.

A _classical uncertainty model_ is a tuple $\mathfrak{M}=\langle
W,v,\mu\rangle$ with $W\neq\varnothing$, $\mu:2^{W}\rightarrow[0,1]$, and
$v:\mathtt{Prop}\rightarrow 2^{W}$ extended to the satisfaction relation
$\mathfrak{M},w\vDash\phi$ as follows.

$\displaystyle\mathfrak{M},w\vDash p$ $\displaystyle\text{ iff }w\in v(p)$
$\displaystyle\mathfrak{M},w\vDash{\sim}\phi$ $\displaystyle\text{ iff
}\mathfrak{M},w\nvDash\phi$ $\displaystyle\mathfrak{M},w\vDash\phi\wedge\chi$
$\displaystyle\text{ iff }\mathfrak{M},w\vDash\phi\text{ and
}\mathfrak{M},w\vDash\chi$

If $\mu$ is a belief function, plausibility, probability, etc., we call
$\mathfrak{M}$ _belief_ , _plausibility_ , _probabilistic_ , etc. model.

The _extension_ of a formula $\phi$ is defined as
$\|\phi\|=\\{w:\mathfrak{M},w\vDash\phi\\}$.

######  Definition 4.6 (Classical probabilistic Kripke model).

A _classical probabilistic Kripke model_ is a tuple $\mathfrak{M}=\langle
W,R,v,\pi\rangle$ with $W\neq\varnothing$, $R$ being an equivalence relation
on $W$, $\pi$ being a classical probability measure on $W$ and
$v:\mathtt{Prop}\rightarrow 2^{W}$ extended to the satisfaction relation
$\mathfrak{M},w\vDash\phi$ as follows.

$\displaystyle\mathfrak{M},w\vDash p$ $\displaystyle\text{ iff }w\in v(p)$
$\displaystyle\mathfrak{M},w\vDash{\sim}\phi$ $\displaystyle\text{ iff
}\mathfrak{M},w\nvDash\phi$ $\displaystyle\mathfrak{M},w\vDash\phi\wedge\chi$
$\displaystyle\text{ iff }\mathfrak{M},w\vDash\phi\text{ and
}\mathfrak{M},w\vDash\chi$ $\displaystyle\mathfrak{M},w\vDash\Box\phi$
$\displaystyle\text{ iff }\forall
w^{\prime}:wRw^{\prime}\Rightarrow\mathfrak{M},w^{\prime}\vDash\phi$
$\displaystyle\mathfrak{M},w\vDash\lozenge\phi$ $\displaystyle\text{ iff
}\exists w^{\prime}:wRw^{\prime}~{}\&~{}\mathfrak{M},w^{\prime}\vDash\phi$

######  Theorem 4.7 ((Godo et al.,, 2001, Theorem 1)).

Let $\phi$ be a _propositional classical formula_ and let
$\mathfrak{M}_{\mathtt{bel}}=\langle W,v,\mathtt{bel}\rangle$ and
$\mathfrak{M}=\langle W,v,\mathtt{pl}\rangle$ be, respectively, a belief and
plausibility models, then:

  1. (i)

there is a classical probabilistic model $\mathfrak{M}_{\Box}\\!=\\!\langle
W_{\Box},\\!R_{\Box},\\!v_{\Box},\\!\pi_{\Box}\rangle$ s.t.
$\pi_{\Box}(\|\Box\phi\|)\\!=\\!\mathtt{bel}(\|\phi\|)$;

  2. (ii)

there is a classical probabilistic model $\mathfrak{M}_{\lozenge}=\langle
W_{\lozenge},R_{\lozenge},v_{\lozenge},\pi_{\lozenge}\rangle$ s.t.
$\pi_{\lozenge}(\|\lozenge\phi\|)=\mathtt{pl}(\|\phi\|)$.

We draw the attention of our readers to the fact that $\Box$ and $\lozenge$ do
not have to be $\mathbf{S5}$: it suffices that the underlying modal logic be
normal. Moreover, originally, only (i) is proven in Godo et al., (2001, 2003).
Observe, however, that (ii) can be obtained from (i) by (3) since

$\displaystyle\pi(\|\lozenge\phi\|)$
$\displaystyle=\pi(\|{\sim}\Box{\sim}\phi\|)$
$\displaystyle=1-\pi(\|\Box{\sim}\phi\|)$
$\displaystyle=1-\mathtt{bel}(\|{\sim}\phi\|)$
$\displaystyle=1-\mathtt{bel}(W\setminus\|\phi\|)$
$\displaystyle=\mathtt{pl}_{\mathtt{bel}}(\|\phi\|)$

Let us now introduce probabilistic models for modal $\mathsf{BD}$ formulas. We
borrow the definition of modalities in $\mathsf{BD}$ from Odintsov and
Wansing, (2017).

######  Definition 4.8 ($\mathsf{BD}$ probabilistic Kripke models).

A _$\mathsf{BD}$ probabilistic Kripke model_ is a tuple $\mathfrak{M}=\langle
W,R,v^{+},v^{-},\pi\rangle$ with $W\neq\varnothing$, $R$ being an equivalence
relation on $W$, $\pi$ being _a classical probability measure_ on $W$ and
$v^{+},v^{-}:\mathtt{Prop}\rightarrow 2^{W}$ extended to
$\mathfrak{M},w\vDash^{+}\phi$ and $\mathfrak{M},w\vDash^{-}\phi$ as in
Definition 2.1 for propositional connectives and as below for modalities.

$\displaystyle w\vDash^{+}\Box\phi$ $\displaystyle\text{ iff }\forall
w^{\prime}:wRw^{\prime}\Rightarrow w^{\prime}\vDash^{+}\phi$ $\displaystyle
w\vDash^{+}\lozenge\phi$ $\displaystyle\text{ iff }\exists
w^{\prime}:wRw^{\prime}~{}\&~{}w^{\prime}\vDash^{+}\phi$ $\displaystyle
w\vDash^{-}\Box\phi$ $\displaystyle\text{ iff }\exists
w^{\prime}:wRw^{\prime}~{}\&~{}w^{\prime}\vDash^{-}\phi$ $\displaystyle
w\vDash^{-}\lozenge\phi$ $\displaystyle\text{ iff }\forall
w^{\prime}:wRw^{\prime}\Rightarrow w^{\prime}\vDash^{-}\phi$

Positive and negative extensions of $\phi$ are as in Definition 2.1.

######  Remark 4.9.

Since $\vDash^{+}$ conditions for $\Box$ and $\lozenge$ in the classical logic
and in $\mathsf{BD}$ coincide, it is clear (cf. Hájek, (1996) for details)
that given a probability $\pi$ on a Kripke model $\mathfrak{M}$, there are a
belief and plausibility functions $\mathtt{bel}$ and $\mathtt{pl}$ on
$\mathfrak{M}$ s.t. $\mathtt{bel}(|\phi|^{+})=\pi(|\Box\phi|^{+})$ and
$\mathtt{pl}(|\phi|^{+})=\pi(|\lozenge\phi|^{+})$ for every
$\phi\in\mathcal{L}_{\mathsf{BD}}$.

######  Theorem 4.10.

Let $\phi\in\mathcal{L}_{\mathsf{BD}}$ and consider a $\mathsf{BD}$
$\mathtt{bel}$-model
$\mathfrak{M}_{\mathtt{bel}}=\langle\mathfrak{M},\mathtt{bel}\rangle$ and a
$\mathsf{BD}$ $\mathtt{bel}/\mathtt{pl}$-model
$\mathfrak{M}^{\prime}_{\mathtt{bel}/\mathtt{pl}}=\langle\mathfrak{M}^{\prime},\mathtt{bel}^{\prime},\mathtt{pl}^{\prime}\rangle$.
Then, there exist

  1. 1.

a $\mathsf{BD}$ probabilistic Kripke model $\mathfrak{M}_{\Box}=\langle
W_{\Box},R_{\Box},v^{+}_{\Box},v^{-}_{\Box},\pi_{\Box}\rangle$ with
$\mathtt{bel}(|\phi|^{+})=\pi_{\Box}(|\Box\phi|^{+})$;

  2. 2.

a $\mathsf{BD}$ probabilistic Kripke model
$\mathfrak{M}_{\Box,\lozenge}=\langle
W_{\Box,\lozenge},R_{1},R_{2},v^{+}_{\Box,\lozenge},v^{-}_{\Box,\lozenge},\pi_{\Box,\lozenge}\rangle$
with
$\mathtt{bel}^{\prime}(|\phi|^{+})=\pi_{\Box,\lozenge}(|\Box_{1}\phi|^{+})$
and
$\mathtt{pl}^{\prime}(|\phi|^{+})=\pi_{\Box,\lozenge}(|\lozenge_{2}\phi|^{+})$
(here, $\Box_{1}$ and $\lozenge_{2}$ are associated to $R_{1}$ and $R_{2}$,
respectively).

######  Proof 4.11.

We prove (1) as (2) can be dealt with in the same manner. Let w.l.o.g. $\phi$
be in $\mathsf{NNF}$ and denote $\phi^{*}$ the result of replacing every
negated variable $\neg p$ occurring in $\phi$ with a fresh variable $p^{*}$.
Consider $\mathfrak{M}_{\mathtt{bel}}=\langle
W,v^{+},v^{-},\mathtt{bel}\rangle$ and $\mathfrak{M}^{*}_{\mathtt{bel}}$ (cf.
the proof of Lemma 3.33). It is easy to see that
$\mathtt{bel}(|\phi|^{+})=\mathtt{bel}(|\phi^{*}|^{+})$.

Now define a _classical_ belief model
$\mathfrak{M}^{\mathsf{cl}}_{\mathtt{bel}}=\langle
W,v^{\mathsf{cl}},\mathtt{bel}\rangle$ with $v^{\mathsf{cl}}(q)=v^{+}(q)$ for
every $q\in\mathtt{Prop}$. Clearly,
$\mathtt{bel}(|\phi^{*}|^{+})=\mathtt{bel}(\|\phi^{*}\|)$ for all
$\phi^{*}$’s. Thus, by Theorem 4.7, we have that there is a classical Kripke
probabilistic model $\mathfrak{M}_{\Box}\\!=\\!\langle
W_{\Box},\\!R_{\Box},\\!v_{\Box},\\!\pi_{\Box}\rangle$ s.t.
$\pi_{\Box}(\|\Box\phi^{*}\|)\\!=\\!\mathtt{bel}(\|\phi^{*}\|)$. It remains to
construct a suitable $\mathsf{BD}$ probabilistic Kripke model.

We define $\mathfrak{M}^{\mathsf{BD}}_{\Box}=\langle
W_{\Box},R_{\Box},v^{+}_{\Box},v^{-}_{\Box},\pi_{\Box}\rangle$ with
$v^{+}_{\Box}(p)=v_{\Box}(p)$ and $v^{-}_{\Box}(p)=v_{\Box}(p^{*})$. One can
show by induction on $\phi^{*}$ that $\|\phi^{*}\|=|\phi|^{+}$, and thus
$\|\Box\phi^{*}\|=|\Box\phi|^{+}$: indeed, cf. semantical conditions for
$\Box$ in Definitions 4.6 and 4.8. Hence,
$\pi_{\Box}(\|\Box\phi^{*}\|)=\pi_{\Box}(|\Box\phi|^{+})$, as required.

##  5 Logics for belief and plausibility functions over $\mathsf{BD}$

In this section, we recall two-layered logics
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$
for reasoning with belief and plausibility functions over $\mathsf{BD}$ that
were presented in Bílková et al., (2023). We then combine the technique of
Hájek and Tulipani, (2001) with the results of Godo et al., (2001, 2003) and
Theorem 4.10 to obtain the $\mathsf{NP}$-completeness of
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$.

###  5.1 Languages and semantics

######  Definition 5.1
($\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$:
language and semantics).

The language of
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
is constructed using the grammar below.

$\displaystyle\mathcal{L}_{\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}\ni\alpha$
$\displaystyle\coloneqq\mathsf{B}\phi~{}(\phi\in\mathcal{L}_{\mathsf{BD}})\mid\neg\alpha\mid\alpha\rightarrow\alpha\mid{\sim}\alpha\mid\triangle\alpha$

A
_$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
model_ is a tuple
$\mathbb{M}_{\mathtt{bel}}=\langle\mathfrak{M},\mathtt{bel},e_{1},e_{2}\rangle$
with

  * •

$\langle\mathfrak{M},\mathtt{bel}\rangle$ being a $\mathsf{BD}$
$\mathtt{bel}$-model (cf. Definition 4.3);

  * •

$e_{1}$ and $e_{2}$ being
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
valuations induced by $\mathtt{bel}$:

    * –

$e_{1}(\mathsf{B}\phi)=\mathtt{bel}(|\phi|^{+})$,
$e_{2}(\mathsf{B}\phi)=\mathtt{bel}(|\phi|^{-})$;

    * –

values of complex
$\mathcal{L}_{\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$-formulas
are computed via Definition 3.3.

We say that $\alpha$ is
_$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
-valid_ iff $e_{1}(\alpha)=1$ and $e_{2}(\alpha)=0$ in all models. A set of
formulas $\Gamma$ _entails_ $\alpha$
($\Gamma\models_{\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}\alpha$)
iff there is no $\mathbb{M}_{\mathtt{bel}}$ s.t. $e(\gamma)=(1,0)$ for all
$\gamma\in\Gamma$ but $e(\alpha)\neq(1,0)$.

######  Remark 5.2.

Note that we cannot utilise the technique from Lemma 3.7 to reduce
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
validity to checking whether $e_{1}(\alpha)=1$ in every model. This is because
belief functions are _not additive_. Thus, even though we can construct
$(v^{*})^{+}$ and $(v^{*})^{-}$ s.t. (1) holds, we cannot use it to infer the
following counterpart of (2):

$\displaystyle
e^{*}(\mathsf{B}\phi)=(1-\mathtt{bel}(|\phi|^{-}),1-\mathtt{bel}(|\phi|^{+}))=(1-e_{2}(\mathsf{B}\phi),1-e_{1}(\mathsf{Pr}\phi))$
(5)

Indeed, (5) does not hold in general since it is not necessarily the case that
$\mathtt{bel}(W\setminus X)=1-\mathtt{bel}(X)$ for $X\subseteq W$.

$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$
uses a different paraconsistent expansion of Łukasiewicz logic
($\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}$
) that is inspired by Nelson’s paraconsistent logic from Nelson, (1949). The
logic was introduced in Bílková et al., (2021) and further investigated in
Bílková et al., (2023). We recall its language and semantics below.

######  Definition 5.3
($\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}$:
language and semantics).

The language is constructed via the following grammar.

$\mathcal{L}_{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}\ni\phi\coloneqq
p\mid{\sim_{\mathsf{N}}}\phi\mid\neg\phi\mid(\phi\wedge\phi)\mid(\phi\rightarrowtriangle\phi)$

The support of truth and support of falsity conditions are given by the
following extensions of $v_{1},v_{2}:\mathtt{Prop}\rightarrow[0,1]$
($\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}$
valuations) to the complex formulas.

$\displaystyle v_{1}(\neg\phi)$ $\displaystyle=v_{2}(\phi)$ $\displaystyle
v_{2}(\neg\phi)$ $\displaystyle=v_{1}(\phi)$ $\displaystyle
v_{1}({\sim_{\mathsf{N}}}\phi)$
$\displaystyle={\sim_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}v_{1}(\phi)$
$\displaystyle v_{2}({\sim_{\mathsf{N}}}\phi)$ $\displaystyle=v_{1}(\phi)$
$\displaystyle v_{1}(\phi\wedge\chi)$
$\displaystyle=v_{1}(\phi)\wedge_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v_{1}(\chi)$
$\displaystyle v_{2}(\phi\wedge\chi)$
$\displaystyle=v_{2}(\phi)\vee_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v_{2}(\chi)$
$\displaystyle v_{1}(\phi\rightarrowtriangle\chi)$
$\displaystyle=v_{1}(\phi)\rightarrow_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v_{1}(\chi)$
$\displaystyle v_{2}(\phi\rightarrowtriangle\chi)$
$\displaystyle=v_{1}(\phi)\odot_{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}v_{2}(\chi)$

We say that $\phi$ is
_$\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}$
-valid_ iff $v_{1}(\phi)=1$ for every $v_{1}$. $\Gamma$ _entails_ $\chi$
($\Gamma\models_{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}\chi$)
iff there is no $v_{1}$ s.t. $v_{1}(\phi)=1$ for every $\phi\in\Gamma$ and
$v_{1}(\chi)\neq 1$.

######  Definition 5.4
($\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$:
language and semantics).

The language is given by the grammar below.

$\displaystyle\mathcal{L}_{\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}}\ni\alpha$
$\displaystyle\coloneqq\mathsf{B}\phi~{}(\phi\in\mathcal{L}_{\mathsf{BD}})\mid\mathsf{Pl}\phi\mid\neg\alpha\mid\alpha\wedge\alpha\mid\alpha\rightarrowtriangle\alpha\mid{\sim_{\mathsf{N}}}\alpha$

A
_$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$
model_ is a tuple
$\mathbb{M}_{\mathtt{bel}/\mathtt{pl}}=\langle\mathfrak{M},\mathtt{bel},\mathtt{pl},e_{1},e_{2}\rangle$
with

  * •

$\langle\mathfrak{M},\mathtt{bel},\mathtt{pl}\rangle$ being a $\mathsf{BD}$
$\mathtt{bel}/\mathtt{pl}$-model (cf. Definition 4.4);

  * •

$e_{1}$ and $e_{2}$ being
$\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}$
valuations induced by $\mathtt{bel}$ and $\mathtt{pl}$:

    * –

$e_{1}(\mathsf{B}\phi)=\mathtt{bel}(|\phi|^{+})$,
$e_{2}(\mathsf{B}\phi)=\mathtt{pl}(|\phi|^{-})$,
$e_{1}(\mathsf{Pl}\phi)=\mathtt{pl}(|\phi|^{+})$,
$e_{2}(\mathsf{Pl}\phi)=\mathtt{bel}(|\phi|^{-})$;

    * –

values of complex
$\mathcal{L}_{\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}}$-formulas
are computed via Definition 5.3.

We say that $\alpha$ is
_$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$
-valid_ iff $e_{1}(\alpha)=1$ for every
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$
model. $\Gamma$ _entails_ $\alpha$
($\Gamma\models_{\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}}\alpha$)
iff there is no model s.t. $e_{1}(\gamma)=1$ for every $\gamma\in\Gamma$ and
$e_{1}(\alpha)\neq 1$.

Note that using (4), we can define a plausibility operator
$\mathsf{Pl}_{\mathsf{B}}$ in
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
as $\mathsf{Pl}_{\mathsf{B}}\phi\coloneqq{\sim}\mathsf{B}\neg\phi$. The main
difference between it and $\mathsf{Pl}$ in
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$
is that the latter is _independent of belief_. We refer readers to Bílková et
al., (2023) for a more detailed discussion of differences between
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$.

In the previous section, we showed (Theorem 4.10) that belief and plausibility
in $\mathsf{BD}$ can be represented as probabilities of modal formulas. We are
going to introduce two logics —
$\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$ and
$\mathsf{Pr}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}_{\mathbf{S5}}$
— that deal with those and show that
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$
can be embedded into them.

To simplify the presentation, we first construct three modal languages. There,
all variables are in the scope of modalities, and modalities do not nest nor
are mixed in one formula (i.e., we forbid formulas such as
$\Box_{1}p\wedge\lozenge_{2}q$).

######  Definition 5.5.

The first language is as follows.

$\displaystyle\mathcal{L}_{\mathsf{BD}^{1}_{\Box}}\ni\sigma$
$\displaystyle\coloneqq\heartsuit\phi~{}(\heartsuit\in\\{\Box,\lozenge\\},\phi\in\mathcal{L}_{\mathsf{BD}})\mid\neg\sigma\mid\sigma\wedge\sigma\mid\sigma\vee\sigma$

The second and third languages are built in the same way but have explicit
indexing of modalities.

$\displaystyle\mathcal{L}_{\mathsf{BD}^{1}_{\Box_{1}}}\ni\sigma$
$\displaystyle\coloneqq\heartsuit_{1}\phi~{}(\heartsuit\in\\{\Box,\lozenge\\},\phi\in\mathcal{L}_{\mathsf{BD}})\mid\neg\sigma\mid\sigma\wedge\sigma\mid\sigma\vee\sigma$
$\displaystyle\mathcal{L}_{\mathsf{BD}^{1}_{\Box_{2}}}\ni\tau$
$\displaystyle\coloneqq\heartsuit_{2}\phi~{}(\heartsuit\in\\{\Box,\lozenge\\},\phi\in\mathcal{L}_{\mathsf{BD}})\mid\neg\tau\mid\tau\wedge\tau\mid\tau\vee\tau$

######  Definition 5.6 ($\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$:
language and semantics).

The language is constructed as follows.

$\displaystyle\mathcal{L}_{\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}}\ni\alpha$
$\displaystyle\coloneqq\mathsf{Pr}\sigma~{}(\sigma\in\mathcal{L}_{\mathsf{BD}^{1}_{\Box}})\mid{\sim}\alpha\mid\neg\alpha\mid\triangle\alpha\mid(\alpha\rightarrow\alpha)$

A _$\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$ model_ is a tuple
$\mathbb{M}_{\pi}=\langle\mathfrak{M},\pi,e_{1},e_{2}\rangle$ s.t.

  * •

$\langle\mathfrak{M},\pi\rangle$ is a $\mathsf{BD}$ probabilistic Kripke
model;

  * •

$e_{1}$ and $e_{2}$ are
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
valuations induced by $\pi$:

    * –

$e_{1}(\mathsf{Pr}\sigma)=\pi(|\sigma|^{+})$,
$e_{2}(\mathsf{Pr}\sigma)=\pi(|\sigma|^{-})$;

    * –

values of complex
$\mathcal{L}_{\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}}$-formulas
are computed via Definition 3.3.

We say that $\alpha$ is _$\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$
-valid_ iff $e_{1}(\alpha)=1$ and $e_{2}(\alpha)=0$ in all models. A set of
formulas $\Gamma$ _entails_ $\alpha$
($\Gamma\models_{\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}}\alpha$)
iff there is no $\mathbb{M}_{\pi}$ s.t. $e(\gamma)=(1,0)$ for all
$\gamma\in\Gamma$ but $e(\alpha)\neq(1,0)$.

The next statements can be proven in the same manner as Lemma 3.7 and 3.33.

######  Lemma 5.7.

Let
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}}$.
Then $\alpha$ is $\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$ valid
iff $e_{1}(\alpha)=1$ in all
$\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$ models.

######  Lemma 5.8.

Let
$\alpha\in\mathcal{L}_{\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}}$.
Then there is $\alpha^{*}$ where $\neg$ does not occur at all s.t.
$\alpha^{*}$ is
$\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$-satisfiable iff $\alpha$
is $\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$-satisfiable.

######  Definition 5.9
($\mathsf{Pr}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}_{\mathbf{S5}}$:
language and semantics).

The language is generated by the following grammar.

$\displaystyle\mathcal{L}_{\mathsf{Pr}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}_{\mathbf{S5}}}\ni\alpha$
$\displaystyle\coloneqq\mathsf{Pr}_{1}\sigma~{}(\sigma\in\mathcal{L}_{\mathsf{BD}^{1}_{\Box_{1}}})\mid\mathsf{Pr}_{2}\tau~{}(\tau\in\mathcal{L}_{\mathsf{BD}^{1}_{\Box_{2}}})\mid\neg\alpha\mid\alpha\wedge\alpha\mid\alpha\rightarrowtriangle\alpha\mid{\sim_{\mathsf{N}}}\alpha$

A
_$\mathsf{Pr}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}_{\mathbf{S5}}$
model is a tuple_
$\mathbb{M}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}_{\pi_{1},\pi_{2}}=\langle
W,R_{1},R_{2},v^{+},v^{-},\pi_{1},\pi_{2},e_{1},e_{2}\rangle$ s.t.

  * •

$\langle W,R_{1},R_{2},v^{+},v^{-},\pi_{1},\pi_{2}\rangle$ is a $\mathsf{BD}$
probabilistic Kripke model with two relations and two measures;

  * •

$e_{1}$ and $e_{2}$ are
$\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}$
valuations induced by $\pi_{1}$ and $\pi_{2}$:

    * –

$e_{1}(\mathsf{Pr}_{1}\sigma)=\pi_{1}(|\sigma|^{+})$,
$e_{2}(\mathsf{Pr}_{1}\sigma)=\pi_{1}(|\sigma|^{-})$;

    * –

$e_{1}(\mathsf{Pr}_{2}\tau)=\pi_{2}(|\tau|^{+})$,
$e_{2}(\mathsf{Pr}_{2}\tau)=\pi_{2}(|\tau|^{-})$;

    * –

values of complex
$\mathcal{L}_{\mathsf{Pr}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}_{\mathbf{S5}}}$-formulas
are computed via Definition 5.3.

###  5.2 Embedding of belief logics into probabilistic logics

Theorem 4.10 shows that beliefs can be represented as probabilities of modal
formulas. In this section, we use this result to prove that we can faithfully
embed
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
and
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$
into $\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$ and
$\mathsf{Pr}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}_{\mathbf{S5}}$.
To simplify the presentation, observe that all
$\mathcal{L}_{\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$\-
and
$\mathcal{L}_{\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}}$-formulas
can be transformed into an outer-$\neg$-free form since
${\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}_{(\triangle,\rightarrow)}$
and
$\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}$
permit $\mathsf{NNF}$’s and since the following holds.

$\displaystyle e(\neg\mathsf{B}\phi)$ $\displaystyle=e(\mathsf{B}\neg\phi)$
(in
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$)
$\displaystyle e(\neg\mathsf{B}\phi)$ $\displaystyle=e(\mathsf{Pl}\neg\phi)$
$\displaystyle e(\neg\mathsf{Pl}\phi)$ $\displaystyle=e(\mathsf{B}\neg\phi)$
(in
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}}$)

######  Definition 5.10 (Embedding of
$\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}$
into $\mathsf{Pr}^{(\triangle,\rightarrow)}_{\mathbf{S5}}$).

Let
$\alpha\in\mathcal{L}_{\mathsf{Bel}^{{\mathchoice{\mbox{\sf\L}}{\mbox{\sf\L}}{\mbox{\sf\scriptsize\L}}{\mbox{\sf\tiny\L}}}^{2}}_{\triangle}}$
be outer-$\neg$-free, we define $\alpha^{\boxplus}$ and $\alpha^{\boxminus}$
as follows.

$\displaystyle(\mathsf{B}\phi)^{\boxplus}$
$\displaystyle=\mathsf{Pr}(\Box\phi)$
$\displaystyle(\mathsf{B}\phi)^{\boxminus}$
$\displaystyle=\mathsf{Pr}(\Box\neg\phi)$
$\displaystyle(\triangle\beta)^{\boxplus}$
$\displaystyle=\triangle(\beta^{\boxplus})$
$\displaystyle(\triangle\beta)^{\boxminus}$
$\displaystyle={\sim}\triangle{\sim}(\beta^{\boxminus})$
$\displaystyle({\sim}\beta)^{\boxplus}$
$\displaystyle={\sim}(\beta^{\boxplus})$
$\displaystyle({\sim}\beta)^{\boxminus}$
$\displaystyle={\sim}(\beta^{\boxminus})$
$\displaystyle(\beta\rightarrow\gamma)^{\boxplus}$
$\displaystyle=\beta^{\boxplus}\rightarrow\gamma^{\boxplus}$
$\displaystyle(\beta\rightarrow\gamma)^{\boxminus}$