$\displaystyle\neg(a_{1},a_{2})$ $\displaystyle=(a_{2},a_{1})$

$(0,0)$$(1,0)$$(0,1)$$(1,1)$

We put the singleton $\\{(1,0)\\}$ to be the set of designated values and
denote the resulting matrix
$([0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\\{(1,0)\\})$.
Observe, that we can understand the $\neg$-negation geometrically as the
symmetry along the horizontal line, while the ${\sim}$-negation
${\sim}(x,y)=(1-y,1-x)$ geometrically denotes the symmetry along the middle
point $(0.5,0.5)$.

The semantical consequence of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
is defined as $\\{(1,0)\\}$ preservation over all valuations
$v:\mathtt{Prop}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\to[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
(extended to the whole language
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$
as expected):

$\Gamma\vDash_{[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha\
\ \mbox{ iff }\ \ \forall v(v[\Gamma]\subseteq\\{(1,0)\\}\Rightarrow
v(\alpha)=(1,0)).$

######  Convention 4.1.

Given a valuation $v$ s.t. $v(\phi)=(x,y)$, we will further write
$v_{1}(\phi)=x$ and $v_{2}(\phi)=y$ when dealing with the coordinates of $v$.

######  Remark 4.1.

The matrix
$([0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\\{(1,0)\\})$
can be equivalently seen as the product MV algebra
$[0,1]_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\times[0,1]_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{op}$,
where
$[0,1]_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
is the standard MV algebra and
$[0,1]_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{op}$
is its dual: the operations and order of the standard MV algebra
$([0,1],\wedge,\vee,\rightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\&_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\ominus_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\oplus_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},{\sim_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}})$,
are turned upside down and dualized in the dual algebra as
$([0,1]^{op},\vee,\wedge,\ominus_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\oplus_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\rightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\&_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},{\sim_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}})$.
The natural dual of the globalisation Baaz delta operator
$\triangle_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
(”definitely true”) is then the operator
${\sim_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\triangle_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}{\sim_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$,
which results in $0$ if its argument is $0$, and in $1$ otherwise.

######  Remark 4.2 (The two-dimensional delta operators).

Observe that $\triangle(a_{1},a_{2})$ can only result in the four values
$(1,0),(1,1),(0,0),(0,1)$ in
$[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$:
$\triangle(a_{1},a_{2})=(1,0)$ if and only if $((a_{1},a_{2})=(1,0))$,
$\triangle(a_{1},a_{2})=(1,1)$ if and only if $a_{1}=1,a_{2}\neq 0$,
$\triangle(a_{1},a_{2})=(0,0)$ if and only if $a_{1}\neq 1,a_{2}=0$, and
$\triangle(a_{1},a_{2})=(0,1)$ else. Defining the following operator

${\triangle^{\top}}\alpha\coloneqq\triangle\alpha\wedge{\sim}\neg\triangle\alpha,$

we obtain the $(1,0)$-detecting operator in
$[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$:
it has value $(1,0)$ iff the argument has the value $(1,0)$, and is $(0,1)$
everywhere else.

It is well known that the Łukasiewicz language expanded with $\triangle$ can
define the Gödel implication (cf. [10, CH.I, 2.2.1]) as
$\alpha\rightarrow_{G}\beta\coloneqq\triangle(\alpha\rightarrow\beta)\vee\beta$.
Similarly, co-implication can be defined as
$\beta\Yleft_{G}\alpha\coloneqq\beta\wedge{\sim}\triangle(\beta\rightarrow\alpha)$.
Thus in
$[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$,

$\displaystyle\triangle(a\rightarrow b)\vee b$
$\displaystyle=(\triangle(a_{1}\rightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}b_{1})\vee
b_{1},{\sim}\triangle{\sim}(b_{2}\ominus_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}a_{2})\wedge
b_{2})$
$\displaystyle=(\triangle(a_{1}\rightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}b_{1})\vee
b_{1},{\sim}\triangle(b_{2}\rightarrow a_{2})\wedge b_{2})$
$\displaystyle=(a_{1}\rightarrow_{G}b_{1},b_{2}\Yleft_{G}a_{2})$

defines the implication (and consequently also other connectives) of the two-
dimensional bi-Gödel logic $\mathsf{G}_{(1,0)}^{2}(\rightarrow)$ introduced in
[8] to reason about comparative uncertainty.

It is worth observing, that due to ${\triangle^{\top}}$, we can express both
the order and the strict order of the
$[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$:
First, $a\rightarrow b$ is designated if and only if $a\leq b$, thus
${\triangle^{\top}}(a\rightarrow b)$ is $(1,0)$ if $a\leq b$, and it is
$(0,1)$ otherwise. Next, the formula ${\triangle^{\top}}(a\rightarrow
b)\wedge{\sim}{\triangle^{\top}}(b\rightarrow a)$ is $(1,0)$ if $a<b$, and it
is $(0,1)$ otherwise.

######  Definition 4.12 (Axiomatisation of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$).

The logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
is axiomatised by the following axioms and rules:

(w) | $\alpha\rightarrow(\beta\rightarrow\alpha)$ | ($\triangle$1) | $\triangle\alpha\vee{\sim}\triangle\alpha$
---|---|---|---
(sf) | $(\alpha\rightarrow\beta)\rightarrow((\beta\rightarrow\gamma)\rightarrow(\alpha\rightarrow\gamma))$ | ($\triangle$2) | $\triangle\alpha\rightarrow\alpha$
(waj) | $((\alpha\rightarrow\beta)\rightarrow\beta)\rightarrow((\beta\rightarrow\alpha)\rightarrow\alpha)$ | ($\triangle$3) | $\triangle\alpha\rightarrow\triangle\triangle\alpha$
(co) | $({\sim}\beta\rightarrow{\sim}\alpha)\rightarrow(\alpha\rightarrow\beta)$ | ($\triangle$4) | $\triangle(\alpha\vee\beta)\rightarrow\triangle\alpha\vee\triangle\beta$
(dn$\neg$) | $\neg\neg\alpha\leftrightarrow\alpha$ | ($\triangle$5) | $\triangle(\alpha\rightarrow\beta)\rightarrow\triangle\alpha\rightarrow\triangle\beta$
($\neg{\sim}$) | $\neg{\sim}\alpha\leftrightarrow{\sim}\neg\alpha$ | ($\neg\triangle$) | $\neg\triangle\alpha\leftrightarrow{\sim}\triangle{\sim}\neg\alpha$
(K${\sim}\neg$) | $({\sim}\neg\alpha\rightarrow{\sim}\neg\beta)\leftrightarrow{\sim}\neg(\alpha\rightarrow\beta)$ | (Nec) | $\alpha\vdash\triangle\alpha$
($\vee$) | $\alpha\vee\beta\leftrightarrow((\alpha\rightarrow\beta)\rightarrow\beta)$ | (Conf) | $\alpha\vdash{\sim}\neg\alpha$
(MP) | $\alpha,\alpha\rightarrow\beta\vdash\beta$ |  |

The axioms of weakening, suffixing, Wajsberg’s axiom, and (converse)
contraposition (w, sf, waj, co) together with the rule (MP) completely
axiomatise Łukasiewicz logic in the language $\\{\rightarrow,{\sim}\\}$ (cf.
[28]). Axiom ($\vee$) is the definition of disjunction, which we need to
formulate two of the the $\triangle$ axioms.

The delta axioms ($\triangle$1–5) and the (Nec) rule above, except the
additional ($\neg\triangle$) axiom, present the usual complete axiomatisation
of Baaz Delta operator over Łukasiewicz logic (cf. [28, Def. 2.4.5] or [10, CH
I,2.2.1]).

First, observe that the $\neg$ negations can provably be pushed to the atomic
formulas, and we can thus consider formulas, up to provable equivalence, in a
_negation normal form (NNF)_ , i.e. formulas built using
$\\{\rightarrow,\sim,\triangle\\}$ from _literals_ of the form $p,\neg p$:

######  Lemma 4.13 (NNF).

For each formula $\alpha$ in
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$
there is a formula in $\neg$-negation normal form $\alpha^{\star}$ such that

$\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\alpha\leftrightarrow\alpha^{\star}.$

###### Proof.

We have the axiom ($\neg\triangle$), and we have
$\neg{\sim}\alpha\leftrightarrow{\sim}\neg\alpha$ and
$\neg(\alpha\rightarrow\beta)\leftrightarrow{\sim}{\sim}\neg(\alpha\rightarrow\beta)\leftrightarrow{\sim}({\sim}\neg\alpha\rightarrow{\sim}\neg\beta)$
provable. A procedure can therefore be defined which turns each $\alpha$ into
$\alpha^{\star}$ in nnf, so that we can prove, by induction, that
$({\sim}\alpha)^{\star}\leftrightarrow{\sim}\alpha^{\star}$,
$(\triangle\alpha)^{\star}\leftrightarrow\triangle\alpha^{\star}$, and
$(\alpha\rightarrow\beta)^{\star}\leftrightarrow{\sim}({\sim}\alpha^{\star}\rightarrow{\sim}\beta^{\star})$.
∎

######  Remark 4.3 (The conflation).

The composition of the two negations ${\sim}\neg$ works semantically as
follows: ${\sim}\neg(a_{1},a_{2})=(1-a_{2},1-a_{1})$, and we can geometrically
understand it on the
$[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
algebra as the symmetry along the vertical line. Such operation is often
referred to as _conflation_ (cf., e.g. [24, 37]), and it is a form of an
involutive information negation (indeed, we have provably
${\sim}\neg{\sim}\neg\alpha\leftrightarrow\alpha$).

One can easily prove in the calculus above that conflation distributes with
all the Łukasiewicz connectives
$\\{\rightarrow,{\sim},\triangle,\&,\wedge,\vee,\oplus,\ominus\\}$ (it
suffices to use $(K{\sim}\neg,\neg{\sim})$ and $(\neg\triangle)$ axioms,
together with the definitions of the derived connectives).

######  Remark 4.4 (The $\triangle$ and ${\triangle^{\top}}$ operators).

Observe that the $\triangle$ operator has some useful additional properties
(we list only those we will need later: proofs of most of them in Ł can be
found e.g., in [28, Lemma 2.4.11], and they can also similarly be proven in
the calculus above):

$\displaystyle\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\triangle\alpha\leftrightarrow\triangle(\alpha\&\alpha)\leftrightarrow\triangle\alpha\&\triangle\alpha$
$\displaystyle\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\triangle(\alpha\&\beta)\leftrightarrow\triangle\alpha\&\triangle\beta\leftrightarrow\triangle(\alpha\wedge\beta)$
$\displaystyle\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}(\triangle\alpha\rightarrow(\triangle\alpha\rightarrow\beta))\rightarrow(\triangle\alpha\rightarrow\beta)$

The last formula is a form of the contraction principle for
$\triangle$-formulas, and its provability follows immediately from the
$(\triangle 1)$ and $(\vee)$ axioms.

Observing that
${\triangle^{\top}}\alpha\coloneqq\triangle\alpha\wedge{\sim}\neg\triangle\alpha$
and thus, by the above principles and conflation distribution over
$\triangle$, provably
${\triangle^{\top}}\alpha\leftrightarrow\triangle(\alpha\wedge{\sim}\neg\alpha)$,
one can consequently prove all the above principles for
${\triangle^{\top}}$-formulas as well. Namely, the contraction principle
$({\triangle^{\top}}\alpha\rightarrow({\triangle^{\top}}\alpha\rightarrow\beta))\rightarrow({\triangle^{\top}}\alpha\rightarrow\beta)$
is provable. Moreover, the $(\triangle 1-2,\triangle 4-5)$ axioms and the
(Nec) rule with $\triangle$ replaced by ${\triangle^{\top}}$ remain both sound
and derivable. It is worth noting that it is _not_ the case for the remaining
$(\triangle 3)$ axiom. As an additional principle we can prove that
${\triangle^{\top}}$-formulas are fixpoints of conflation:
${\sim}\neg{\triangle^{\top}}\alpha\leftrightarrow{\triangle^{\top}}\alpha$.

Applying the insights remarked on above, we can prove that the logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
has the following ${\triangle^{\top}}$-deduction theorem (cf. [28, Th. 2.4.14]
or [10, Ch.I, Th. 2.2.1]):

######  Lemma 4.14 (DT${\triangle^{\top}}$).

$\Gamma,\alpha\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\beta\
\ \mbox{iff}\ \
\Gamma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}{\triangle^{\top}}\alpha\rightarrow\beta.$

###### Proof.

The proof of the theorem is rather standard, by induction on the length $n$ of
the proof of
$\Gamma,\alpha\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\beta$.

$n=1$:

In this case $\beta$ is either an instance of an axiom, or an assumption form
$\Gamma$, or $\alpha=\beta$. In the first two cases, the result follows by the
(w) axiom. The remaining case uses that
${\triangle^{\top}}\alpha\rightarrow\alpha$ is provable.

$n>1$:

We assume that for all shorter proofs the results holds, and let $\gamma_{1}$,
…, $\gamma_{n},\beta$ be a proof of $\beta$ from $\Gamma\cup\\{\alpha\\}$. We
distinguish three cases:

(Conf)

Let $\beta\coloneqq{\sim}\neg\gamma_{n}$ be obtained by the conflation rule.
By the induction hypothesis, ${\triangle^{\top}}\alpha\rightarrow\gamma_{n}$
is provable. By an application of (Conf), (K${\sim}\neg$) and (MP) we obtain
${\sim}\neg{\triangle^{\top}}\alpha\rightarrow{\sim}\neg\gamma_{n}$. By
${\sim}\neg{\triangle^{\top}}\alpha\leftrightarrow{\triangle^{\top}}\alpha$
(see Remark 4.4) it follows that
${\triangle^{\top}}\alpha\rightarrow{\sim}\neg\gamma_{n}$ as desired.

(Nec)

Let $\beta\coloneqq\triangle\gamma_{n}$ be obtained by the necessitation rule.
By the induction hypothesis, ${\triangle^{\top}}\alpha\rightarrow\gamma_{n}$
is provable. By an application of (Nec), using provability of
${\triangle^{\top}}({\triangle^{\top}}\alpha\rightarrow\gamma_{n})\rightarrow({\triangle^{\top}}{\triangle^{\top}}\alpha\rightarrow{\triangle^{\top}}\gamma_{n})$,
and (MP) we obtain
${\triangle^{\top}}{\triangle^{\top}}\alpha\rightarrow{\triangle^{\top}}\gamma_{n}$.
Using provability of
${\triangle^{\top}}{\triangle^{\top}}\alpha\leftrightarrow{\triangle^{\top}}\alpha$
(see Remark 4.4) we conclude
${\triangle^{\top}}\alpha\rightarrow{\triangle^{\top}}\gamma_{n}$ as desired.

(MP)

Let $m<n$ and let $\gamma_{m},\gamma_{n}=\gamma_{m}\rightarrow\beta/\beta$ be
an instance of modus ponens. By the induction hypothesis we have
${\triangle^{\top}}\alpha\rightarrow\gamma_{m}$ and
${\triangle^{\top}}\alpha\rightarrow(\gamma_{m}\rightarrow\beta)$ provable.
From the latter we have also
$\gamma_{m}\rightarrow({\triangle^{\top}}\alpha\rightarrow\beta)$ provable.
Thus, by (suf) and (MP) we obtain
${\triangle^{\top}}\alpha\rightarrow({\triangle^{\top}}\alpha\rightarrow\beta)$.
By the contraction principle of Remark 4.4 we finally obtain
${\triangle^{\top}}\alpha\rightarrow\beta$ as desired.

∎

We proceed to prove finite strong standard completeness (FSSC for short) of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
i.e. strong completeness of the finite consequence of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
w.r.t. the matrix
$([0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},\\{(1,0)\\})$.
We do so by reducing the provability in
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
to that in
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$,
which itself is known to be finite strong standard complete, i.e. finite
strong complete w.r.t. the standard MV algebra
$[0,1]_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
(see e.g. [28, Th. 3.2.14]):

######  Lemma 4.15 (Reducing
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
to
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$).

For any _finite_ set of formulas $\Gamma,\alpha$ in a NNF,

$\Gamma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\alpha\ $ iff |  for some finite $\Sigma:\ \boxdot\Gamma,\Sigma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle}\alpha,$
---|---

where ${\sim}\neg\Gamma\coloneqq\\{{\sim}\neg\gamma\mid\gamma\in\Gamma\\}$ and
$\boxdot\Gamma\coloneqq{\sim}\neg\Gamma\cup\Gamma$, and $\Sigma$ contains
instances of $\neg$-axioms.

###### Proof.

The right-left direction is almost trivial:
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$
is a subsystem of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
and all the axioms in $\Sigma$ are provable in
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
and, thanks to the ${\sim}\neg$-rule,
$\Sigma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\boxdot\gamma$
for each $\gamma\in\Sigma$.

For the other direction, we proceed in a few steps. First, we denote by
$\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2-}}$
provability in
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
_without_ the ${\sim}\neg$-rule. By routine induction on proofs (and using
that ${\sim}\neg$ distributes from/to implications, negations, and
$\triangle$), we can see that

$\Gamma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\alpha\ $ iff |  $\boxdot\Gamma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2-}}\alpha.$
---|---

Then we can list all the instances of $\neg$-axioms in the proof above in
$\Sigma$, and obtain:

$\boxdot\Gamma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2-}}\alpha\ $ iff |  $\boxdot\Gamma,\Sigma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle}\alpha.$
---|---

First, note that we can include in $\Sigma$ all instances of $\neg$-axioms for
all subformulas of $\Gamma,\alpha$ as well and still keep the Lemma valid.
This will come in handy in the following completeness proof. Second, we stress
that in the final proof
$\boxdot\Sigma,\Sigma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle}\alpha$
in
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$,
we still use the language of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
where formulas starting with $\neg$ are seen from the point of view of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$
as atomic. ∎

Lemma 4.15 provides a translation of provability in
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
to provability in
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$,
and allows us in particular to observe that the extension of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$
by $\neg$ is conservative. Now, using finite strong standard completeness of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$,
we can see that
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
is finitely strongly standard complete:

######  Lemma 4.16 (FSSC).

For a  _finite_ set of formulas $\Gamma$,

$\Gamma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\alpha$ iff |  $\Gamma\vDash_{[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha.$
---|---

###### Proof.

The left-right direction expresses soundness and consists of checking that all
the axioms are valid and all the rules sound. We only do some cases:

First the ${\sim}\neg$-rule: assume that $v$ is given and $v(\alpha)=(1,0)$.
Then

$v({\sim}\neg\alpha)={\sim}\neg(1,0)={\sim}(0,1)=(1,0).$

Next, for any $v$,

$\displaystyle v({\sim}\neg(\alpha\rightarrow\beta))$
$\displaystyle={\sim}\neg(v(\alpha)\rightarrow v(\beta))$
$\displaystyle={\sim}\neg(v_{1}(\alpha)\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{1}(\beta),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}(v_{2}(\beta)\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{2}(\alpha)))$
$\displaystyle=((v_{2}(\beta)\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{2}(\alpha)),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}(v_{1}(\alpha)\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{1}(\beta))),$

and

$\displaystyle v({\sim}\neg\alpha\rightarrow{\sim}\neg\beta)$
$\displaystyle={\sim}\neg v(\alpha)\rightarrow{\sim}\neg v(\beta)$
$\displaystyle=({\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\alpha),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{1}(\alpha))\rightarrow({\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\beta),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{1}(\beta))$
$\displaystyle=({\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\alpha)\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\beta),v_{1}(\alpha)\&_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{1}(\beta))$
$\displaystyle=((v_{2}(\beta)\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{2}(\alpha)),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}(v_{1}(\alpha)\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{1}(\beta))).$

Next, for any $v$,

$v(\neg{\sim}\alpha)=\neg{\sim}v(\alpha)=({\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\alpha),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{1}(\alpha))={\sim}\neg
v(\alpha)=v({\sim}\neg\alpha).$

Last, for any $v$,

$\displaystyle v(\neg\triangle\alpha)$
$\displaystyle=\neg(v(\triangle\alpha))=\neg(\triangle_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{1}(\alpha),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\triangle_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\alpha))$
$\displaystyle=({\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\triangle_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\alpha),\triangle_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{1}(\alpha))$
$\displaystyle={\sim}(\triangle_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\alpha),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\triangle_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{1}(\alpha))$
$\displaystyle={\sim}\triangle({\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\alpha),{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{1}(\alpha))$
$\displaystyle={\sim}\triangle{\sim}\neg\alpha.$

We leave the rest of the proof of soundness for the reader.

For the right-left direction, let us assume that
$\Gamma\nvdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\alpha$.
Then for some finite $\Sigma$ containing instances of $\neg$-axioms (in
particular those for subformulas of $\Sigma,\alpha$), we have
$\boxdot\Sigma,\Sigma\nvdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle}\alpha.$
Because
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$
is finitely standard complete, there is an evaluation
$v:\mathrm{At}\to[0,1]_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
sending all formulas in $\boxdot\Sigma,\Sigma$ to $1$, while $v(\alpha)<1$.
Here, $\mathrm{At}$ contains literals from $\Sigma,\alpha$ of the form $p,\neg
p$, and atoms and formulas of the form $\neg\sigma$ from
$\boxdot\Sigma,\Sigma$. We define
$v^{\prime}:\mathtt{Prop}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\to[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
by

$v^{\prime}(p)=(v(p),v(\neg p)).$

Let us denote $\beta^{\neg}$ the NNF of $\neg\beta$ (i.e.
$(\neg\beta)^{\star}$). We can then prove, by routine induction, that for each
formula $\beta$ a subformula of $\Sigma,\alpha$, we have

$v^{\prime}(\beta)=(v(\beta),v(\beta^{\neg})).$

To do so, we use the fact that $v[\Sigma]\subseteq\\{1\\}$, and $\Sigma$
contains all instances of $\neg$-axioms for all subformulas of
$\Sigma,\alpha$, and, subsequently, $\Sigma$ ensures that
$v(\neg\beta)=v(\beta^{\neg})$.

We now immediately see that $v^{\prime}(\alpha)<(1,0)$, because $v(\alpha)<1$.
To prove that indeed $v^{\prime}[\Gamma]\subseteq\\{(1,0)\\}$, we use the fact
that $v[\boxdot\Gamma]\subseteq\\{1\\}$: as for all $\gamma\in\Gamma$,
$v({\sim}\neg\gamma)=1$, $v(\neg\gamma)=v(\gamma^{\neg})=0$. For the latter,
we again need to use the fact that $v[\Sigma]\subseteq\\{1\\}$, and $\Sigma$
contains all instances of $\neg$-axioms for all subformulas of $\Gamma$, as
they prove, by means of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\triangle$,
that $\neg\gamma\leftrightarrow\gamma^{\neg}$, and $v$ has to respect that.
Now we conclude, that for all $\gamma\in\Gamma$,
$v^{\prime}(\gamma)=(v(\gamma),v(\gamma^{\neg}))=(1,0)$. ∎

######  Remark 4.5 (Changing the designated values).

Changing the set of designated values in
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
to the filter $(1,1)^{\uparrow}$ yields the logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}_{(1,1)^{\uparrow}}(\rightarrow)$
of [8], expanded with $\triangle$. It can be axiomatised by removing the
conflation rule (Conf) from the axiomatisation of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
provided in Definition 4.12. Its $(\wedge,\vee,\neg)$ fragment coincides with
$\mathsf{BD}$, while the $(\wedge,\vee,\neg)$ fragment of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
coincides with $\mathsf{ETL}$. We will not use this logic in this paper,
however, it can be proved finitely strongly complete by similar manner as
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$.

######  Example 4.1 (What
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
can express).

Recall first that, semantically, $\neg$ is the symmetry along the horizontal,
$\sim$ is the symmetry along the middle point, and the conflation ${\sim}\neg$
is the symmetry along the vertical line. Let now $v_{1}(p)$ quantify the
evidence for $p$ and $v_{2}(p)$ quantify the evidence against $p$. As
discussed in Section 3.3.1, given any statement $p$, we can determine whether
the evidence we have about it is classical, incomplete, or contradictory:

The formula $\neg p\leftrightarrow{\sim}p$, or equivalently
$p\leftrightarrow{\sim}\neg p$, defines the vertical line: for each valuation
$v$, $v(\neg p\leftrightarrow{\sim}p)=(1,0)$ if and only if
$v_{1}(p)=1-v_{2}(p)$. In a sense, $p\leftrightarrow{\sim}\neg p$ measures how
close our information about $p$ is to the non-controversial classical case.
Moreover, from the semantics of ${\triangle^{\top}}$, it is clear that we can
test whether the information is classical by

$\displaystyle v({\triangle^{\top}}(p\leftrightarrow{\sim}\neg p))$
$\displaystyle=\begin{cases}(1,0)&\text{ if }v_{1}(p)=1-v_{2}(p)\\\
(0,1)&\text{ otherwise}\end{cases}$ (28)

(28) is a useful tool. Assume, we have some finite set of statements
$\\{\alpha_{1},\ldots,\alpha_{n}\\}$. Then, using finite strong completeness
of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
we can check whether those entail classicality of $p$ by establishing the
following inference

$\alpha_{1},\ldots,\alpha_{n}\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}{\triangle^{\top}}(p\leftrightarrow{\sim}\neg
p).$

Unfortunately, $p\rightarrow{\sim}\neg p$ proves ${\sim}\neg p\rightarrow p$,
and thus we cannot really distinguish the left-hand triangle (incompleteness)
from the right-hand triangle (contradictoriness) using these implications.
However, if $p$ is _not_ classical, we can establish whether it is
contradictory or incomplete for example as follows:

$\displaystyle v_{1}(\triangle(p\rightarrow{\sim}\neg p))$
$\displaystyle=\begin{cases}1&\text{ iff }$p$\text{ is incomplete}\\\ 0&\text{
iff }$p$\text{ is contradictory}\end{cases}$ (29)

####  4.2.2 A Nelson-style extension of Łukasiewicz logic

For part of reasoning about belief functions and plausibilities, we will
employ the logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}_{(1,1)^{\uparrow}}(\rightarrowtriangle)$
of [8]. The interpretation of implication in this logic takes a direct
inspiration from Nelson’s paraconsistent logic. We will again skip mentioning
the language in the index throughout this subsection and use simply
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
to refer to the logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}_{(1,1)^{\uparrow}}(\rightarrowtriangle)$.

######  Definition 4.17 (Language and semantics of
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$).

The logic
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
has the following language
$\mathscr{L}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$:

$\alpha\coloneqq\
p\mid\alpha\wedge\beta\mid\alpha\rightarrowtriangle\beta\mid{\sim}\alpha\mid\neg\alpha,$

with
$p\in\mathtt{Prop}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$.
We call the $\rightarrowtriangle$ connective the weak implication. Additional
connectives are definable as follows (where $\Rightarrow,\Leftrightarrow$ are
called strong implication and strong equivalence):

$\displaystyle\alpha\&\beta$
$\displaystyle\coloneqq{\sim}(\alpha\rightarrowtriangle{\sim}\beta)$
$\displaystyle\alpha\Rightarrow\beta$
$\displaystyle\coloneqq(\alpha\rightarrowtriangle\beta)\wedge(\neg\beta\rightarrowtriangle\neg\alpha)$
$\displaystyle\alpha\leftrightarrowtriangle\beta$
$\displaystyle\coloneqq(\alpha\rightarrowtriangle\beta)\wedge(\beta\rightarrowtriangle\alpha)$
$\displaystyle\alpha\Leftrightarrow\beta$
$\displaystyle\coloneqq(\alpha\leftrightarrowtriangle\beta)\wedge(\neg\alpha\leftrightarrowtriangle\neg\beta)$
$\displaystyle\alpha\oplus\beta$
$\displaystyle\coloneqq{\sim}\alpha\rightarrowtriangle\beta$
$\displaystyle\alpha\ominus\beta$
$\displaystyle\coloneqq{\sim}(\alpha\rightarrowtriangle\beta)$
$\displaystyle\alpha\vee\beta$
$\displaystyle\coloneqq\neg(\neg\alpha\wedge\neg\beta)$ $\displaystyle\bot$
$\displaystyle\coloneqq{\sim}(p\rightarrow p)$

To interpret the language, we expand the bilattice $[0,1]^{\Join}$ with the
following operations, derived again from the standard MV algebra (we spell out
the semantics of some of the defined connectives for convenience):

$\displaystyle(a_{1},a_{2})\rightarrowtriangle(b_{1},b_{2})$
$\displaystyle=(a_{1}\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}b_{1},a_{1}\&_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}b_{2})$
$\displaystyle(a_{1},a_{2})\&(b_{1},b_{2})$
$\displaystyle=(a_{1}\&_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}b_{1},a_{1}\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}{\sim}b_{1})$
$\displaystyle{\sim}(a_{1},a_{2})$
$\displaystyle=({\sim}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}a_{1},a_{1})$
$\displaystyle\neg(a_{1},a_{2})$ $\displaystyle=(a_{2},a_{1})$
$\displaystyle(a_{1},a_{2})\oplus(b_{1},b_{2})$
$\displaystyle=(a_{1}\oplus_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}a_{2},{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}a_{1}\&_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}b_{2})$
$\displaystyle(a_{1},a_{2})\ominus(b_{1},b_{2})$
$\displaystyle=(a_{1}\ominus_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}a_{2},a_{1}\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}b_{1})$

$(0,0)$$(1,0)$$(0,1)$$(1,1)$

We put the filter $(1,1)^{\uparrow}\coloneqq\\{(x,y)\mid x=1\\}$ to be the set
of designated values, and denote the resulting matrix
$([0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}},(1,1)^{\uparrow})$.
Observe, that ${\sim}$ now behaves differently than in the logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$:
namely, its value is always on the classical vertical line. The semantical
consequence of
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
is defined as $(1,1)^{\uparrow}$ preservation over all valuation in this
algebra (where $v(\alpha)=(v_{1}(\alpha),v_{2}(\alpha))$):

$\Gamma\vDash_{[0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha\
\ \mbox{ iff }\ \ \forall v(v_{1}[\Gamma]\subseteq\\{1\\}\Rightarrow
v_{1}(\alpha)=1).$

######  Remark 4.6 (Strong and weak implication).

The connective $\rightarrowtriangle$ is called the weak implication. If
$v(\alpha\rightarrowtriangle\beta)$ is designated, then we only know that
$v_{1}(\alpha)\leq v_{1}(\beta)$. The derived weak equivalence
$\alpha\leftrightarrowtriangle\beta\coloneqq(\alpha\rightarrowtriangle\beta)\wedge(\beta\rightarrowtriangle\alpha)$
is not congruential, because its provability does not entail equality of the
semantical values, only of their first coordinates. It is therefore useful to
define the strong counterparts of the two connectives. In particular, the
strong equivalence
$\alpha\Leftrightarrow\beta\coloneqq(\alpha\leftrightarrowtriangle\beta)\wedge(\neg\alpha\leftrightarrowtriangle\neg\beta)$
is congruential.

Observe that, thanks to the peculiar nature of the logic, some of the usual
definitions of Łukasiewicz connectives only work as weak equivalences when
lifted to
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$:
namely,
$\alpha\wedge\beta\leftrightarrowtriangle(\alpha\rightarrowtriangle\beta)\&\alpha$
and
$\alpha\vee\beta\leftrightarrowtriangle((\alpha\rightarrowtriangle\beta)\rightarrowtriangle\beta)$
are valid, but it is no longer the case when both sides of the equivalences
are $\neg$-negated.

######  Definition 4.18.

The logic
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
is axiomatised by the following axioms and rules:

(w) | $\alpha\rightarrowtriangle(\beta\rightarrowtriangle\alpha)$ | ($\vee$) | $((\alpha\rightarrowtriangle\beta)\rightarrowtriangle\beta)\leftrightarrowtriangle\alpha\vee\beta$
---|---|---|---
(sf) | $(\alpha\rightarrowtriangle\beta)\rightarrowtriangle((\beta\rightarrowtriangle\gamma)\rightarrowtriangle(\alpha\rightarrowtriangle\gamma))$ | ($\&$) | $\alpha\&\beta\Leftrightarrow{\sim}(\alpha\rightarrowtriangle{\sim}\beta)$
(waj) | $((\alpha\rightarrowtriangle\beta)\rightarrowtriangle\beta)\rightarrowtriangle((\beta\rightarrowtriangle\alpha)\rightarrowtriangle\alpha)$ | ($\wedge$) | $\alpha\wedge\beta\leftrightarrowtriangle(\alpha\rightarrowtriangle\beta)\&\alpha$
(co) | $({\sim}\beta\rightarrowtriangle{\sim}\alpha)\rightarrowtriangle(\alpha\rightarrowtriangle\beta)$ | ($\neg\wedge$) | $\neg(\alpha\wedge\beta)\Leftrightarrow\neg\alpha\vee\neg\beta$
(dn$\neg$) | $\neg\neg\alpha\Leftrightarrow\alpha$ | ($\neg\vee$) | $\neg(\alpha\vee\beta)\Leftrightarrow\neg\alpha\wedge\neg\beta$
($\neg{\rightarrowtriangle}$) | $\neg(\alpha\rightarrowtriangle\beta)\leftrightarrowtriangle(\alpha\&\neg\beta)$ | ($\neg{\sim}$) | $\neg{\sim}\alpha\leftrightarrowtriangle\alpha$
(MP) | $\alpha,\alpha\rightarrowtriangle\beta\vdash\beta$ |  |

The axioms (w, sf, waj, co, $\vee$, $\wedge$) with the rule (MP) axiomatise
Łukasiewicz logic in terms of weak implication, ($\&$) is the (strong)
definition of the fusion. The remaining are $\neg$-axioms, analogous to those
of the Nelson’s paraconsistent logic $\mathsf{N}4$.

We can, up to weak equivalence, consider formulas in the $\neg$-normal form:

######  Lemma 4.19 (NNF).

For each formula $\alpha$ in
$\mathscr{L}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
there is a formula in $\neg$-negation normal form $\alpha^{\star}$ such that

$\vdash_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha\leftrightarrowtriangle\alpha^{\star}.$

As (MP) is the only rule, the logic possesses a local deduction theorem (LDT)
in terms of the weak implication, as in Ł (cf. [10, Ch.I,Th. 1.2.10]).

We proceed to prove the finite strong standard completeness (FSSC) of the
logic
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$.
We do so by means of a reduction to Łukasiewicz logic, which itself is well-
known to be finite strong standard complete, i.e. finite strong complete
w.r.t. the standard MV algebra
$[0,1]_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
[28, Th. 3.2.14].

######  Lemma 4.20 (Reduction of
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
to Ł).

W.l.o.g. we assume that $\Gamma,\alpha$ consist of formulas in
$\neg$-$\mathsf{NNF}$.

$\Gamma\vdash_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha$
iff
$\Gamma,\Sigma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha$
for $\Sigma$ a finite set consisting of instances of $\neg$-axioms.

###### Proof.

This is almost immediate:
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
is an extension of Ł, so any proof in
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
can be understood as a proof in Ł, with additional assumptions consisting of
all the (finitely many) instances of $\neg$-axioms occurring in the proof.
Observe, that we can equivalently include (finitely many) additional instances
of $\neg$-axioms for subformulas of $\Gamma,\alpha$ in $\Sigma$, and the claim
remains true. ∎

######  Lemma 4.21 (FSSC).

for $\Gamma,\alpha$ a finite set of formulas in
$\mathscr{L}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$,

$\Gamma\vdash_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha\
\ \mbox{iff}\ \
\Gamma\vDash_{[0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha.$

###### Proof.

W.l.o.g. we assume that $\Gamma,\alpha$ consist of formulas in $\neg$-negation
normal form. Assume that
$\Gamma\vdash_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha$.
By the Lemma 4.20, it is the case if and only if
$\Gamma,\Sigma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha$
for $\Sigma$ a finite set consisting of instances of $\neg$-axioms. We will
add the following (finitely many) formulas to $\Sigma$: (i) instances of
$\neg$-axioms for subformulas of $\Gamma,\alpha$, (ii) for each subformula
$\beta$ of $\Gamma,\alpha$ of the form listed on the left, we include an
equivalence listed on the right ($\beta^{\neg}$ denotes the NNF of
$\neg\beta$, i.e. $(\neg\beta)^{\star}$):

$\displaystyle\beta_{1}$ $\displaystyle\wedge\beta_{2}$
$\displaystyle((\beta_{1})^{\neg}\vee(\beta_{2})^{\neg})$
$\displaystyle\leftrightarrowtriangle(\beta_{1}\wedge\beta_{2})^{\neg}$
$\displaystyle\beta_{1}$ $\displaystyle\vee\beta_{2}$
$\displaystyle((\beta_{1})^{\neg}\wedge(\beta_{2})^{\neg})$
$\displaystyle\leftrightarrowtriangle(\beta_{1}\vee\beta_{2})^{\neg}$
$\displaystyle\beta_{1}$ $\displaystyle\rightarrowtriangle\beta_{2}$
$\displaystyle(\beta_{1}\&(\beta_{2})^{\neg})$
$\displaystyle\leftrightarrowtriangle(\beta_{1}\rightarrowtriangle\beta_{2})^{\neg}$
$\displaystyle\beta_{1}$ $\displaystyle\&\beta_{2}$
$\displaystyle(\beta_{1}\rightarrowtriangle{\sim}\beta_{2})$
$\displaystyle\leftrightarrowtriangle(\beta_{1}\&\beta_{2})^{\neg}$
$\displaystyle{\sim}\beta$ $\displaystyle\beta$
$\displaystyle\leftrightarrowtriangle({\sim}\beta)^{\neg}$

We call the resulting finite set $\Sigma^{\prime}$. First we observe that all
the equivalences listed are provable from $\Sigma$ by means of the logic Ł and
$\neg$-axioms instances for subformulas of $\Gamma,\alpha$ (we opt for
enlisting them explicitly for convenience). In particular, we have:

$\Gamma,\Sigma\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha\
\ \mbox{iff}\ \
\Gamma,\Sigma^{\prime}\vdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha.$

Assume now that
$\Gamma,\Sigma^{\prime}\nvdash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\alpha$.
By the FSSC of Ł, we know there is an evaluation $v:\Phi\to[0,1]$, where
$\Phi$ consists of (i) literals from $\Gamma,\Sigma^{\prime},\alpha$, and (ii)
$\neg$-subformulas of $\Sigma^{\prime}$, so that:
$v(\Gamma\cup\Sigma^{\prime})\subseteq\\{1\\}$ while $v(\alpha)<1$. We define
an evaluation
$v^{\prime}:\mathtt{Prop}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\to[0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
by

$v^{\prime}(p)\coloneqq(v(p),v(\neg p)).$

Next, we can easily prove by induction, for each subformula $\beta$ of
$\Gamma,\alpha$, that the extended valuation satisfies

$v^{\prime}(\beta)\coloneqq(v(\beta),v(\beta^{\neg})).$

The proof essentially uses the fact that formulas contained in
$\Sigma^{\prime}$ are $v$-evaluated by $1$.

To conclude, we observe that because $v(\alpha)<1$, by the above we have
$v^{\prime}_{1}(\alpha)<1$. Similarly, because for each $\gamma\in\Gamma$
$v(\gamma)=1$, we have that $v^{\prime}_{1}(\gamma)=1$, making all formulas
from $\Gamma$ designated and $\alpha$ not designated, as desired. ∎

######  Example 4.2 (What we can express in
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$).

Recall first that for each $v$, $v({\sim}p)$ is always on the vertical,
classical line. Observe that, in contrast with
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
we can now directly express incompleteness and contradictoriness: indeed,
$v({\sim}p\rightarrowtriangle\neg p)$ is designated if and only if $v(p)$ lays
within the right triangle, $v(\neg p\rightarrowtriangle{\sim}p)$ is designated
if and only if $v(p)$ lays within the left triangle, and
$v({\sim}p\leftrightarrowtriangle\neg p)$ is designated if and only if $v(p)$
lays on the vertical line. In
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$,
we can thus define ‘$p$ is not incomplete’ as ${\sim}p\rightarrowtriangle\neg
p$, and ‘$p$ is not contradictory’ as $\neg p\rightarrowtriangle{\sim}p$, and
’$p$ is classical’ as ${\sim}p\leftrightarrowtriangle\neg p$.

Moreover, $v((p\rightarrowtriangle q)\wedge(\neg p\rightarrowtriangle\neg q))$
is designated if and only if both $v_{1}(p)\leq v_{1}(q)$ and $v_{2}(p)\leq
v_{2}(q)$, and therefore the formula captures the _information order_ (the
left-right horizontal order) on the $[0,1]^{\Join}$.

###  4.3 Two-layered logic for probabilities

In this subsection, we introduce a two-layered logic
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$
designed to capture reasoning about non-standard probabilities of Subsection
3.1. The _inner layer_ consists of the language, semantics and axiomatisation
of the logic $\mathsf{BD}$ as described in Subsection 2.2. The _outer layer_
consists of the language, semantics and axiomatisation of the logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
as described in Subsection 4.2.1. The two layers are connected with a single
modality $\mathsf{Pr}$ (which can be read as ‘probably’). An application of
the modality to an inner formula yields an atomic modal outer formula, which
is to be interpreted using a probability function over the underlying
probabilistic $\mathsf{BD}$ model, outputting a value in the outer algebra
$[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$.
Other applications of the modality are forbidden in the syntax, in particular,
modalities do not nest.

######  Definition 4.22 (Language and semantics of
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$).

The two-layered language of the logic
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$
is of the form
$(\mathscr{L}_{\mathsf{BD}},\\{\mathsf{Pr}\\},\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}})$,
with $\mathsf{Pr}$ being a unary modality, and it is defined as follows:

inner formulas:

formulas of $\mathscr{L}_{\mathsf{BD}}$

atomic modal formulas:

Let $\phi\in\mathscr{L}_{\mathsf{BD}}$, then $\mathsf{Pr}\phi$ is a modal
atomic formula.

outer formulas:

Let $\mathsf{Pr}\phi$ range over modal atomic formulas, the set of outer
formulas is defined via the following grammar, with the connectives of
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$:

$\alpha\coloneqq\mathsf{Pr}\phi\mid\neg\alpha\mid\alpha\rightarrow\alpha\mid{\sim}\alpha\mid\triangle\alpha.$

Other connectives — $\bot,\wedge,\vee,\&$, $\ominus$ and $\oplus$ — can be
defined as in
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$
of Definition 4.11.

The semantics of
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$
is given over a $\mathsf{BD}$ probabilistic model
$\mathscr{M}=(W,v^{+},v^{-},\mathtt{p})$ (cf. Section 3.1), and the outer
algebra
$[0,1]^{\Join}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$,
as follows:

inner formulas:

for each $\phi\in\mathscr{L}_{\mathsf{BD}}$ the model provides sets
$|\phi|^{+}=\\{w\mid w\vDash^{+}\phi\\}$ and $|\phi|^{-}=\\{w\mid
w\vDash^{-}\phi\\}$, as described in Definition 2.2.

atomic modal formulas:

for each atomic modal formula, $v^{\mathscr{M}}(\mathsf{Pr}\phi)$ in
$[0,1]^{\Join}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
is defined as

$v^{\mathscr{M}}(\mathsf{Pr}\phi)=(v^{\mathscr{M}}_{1}(\mathsf{Pr}\phi),v^{\mathscr{M}}_{2}(\mathsf{Pr}\phi))\coloneqq(\mathtt{p}(|\phi|^{+}),\mathtt{p}(|\phi|^{-}))=\left(\sum\limits_{w\vDash^{+}\phi}\mathtt{m}_{\mathtt{p}}(w),\sum\limits_{w\vDash^{-}\phi}\mathtt{m}_{\mathtt{p}}(w)\right).$

outer formulas:

The map $v^{\mathscr{M}}$ is extended to the outer formulas in an expected
manner, following the Definition 4.11 of the interpretation of
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$
connectives in the algebra
$[0,1]^{\Join}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$.

The outer formula $\alpha$ is said to be valid in $\mathscr{M}$, if
$v^{\mathscr{M}}(\alpha)$ is designated (i.e.
$v^{\mathscr{M}}(\alpha)=(1,0)$). It is said to be valid, if it is valid in
all $\mathsf{BD}$ probabilistic models. The consequence relation for
$\Gamma,\alpha$ a set of outer formulas is defined as

$\Gamma\vDash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha\
\ \mbox{iff}\ \
\forall\mathscr{M}(v^{\mathscr{M}}[\Gamma]\subseteq(1,0)\Rightarrow
v^{\mathscr{M}}(\alpha)=(1,0)).$

######  Definition 4.23 (Axiomatisation of
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$).

The two-layered axiomatisation of logic
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}=(\mathsf{BD},M_{p},{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2})$
consists of the following parts:

inner logic:

the axiomatisation of $\mathsf{BD}$ in the language
$\mathscr{L}_{\mathsf{BD}}$ of Definition 2.1

modal axioms:

$M_{p}$, where $\varphi,\psi\in\mathscr{L}_{\mathsf{BD}}$:

$\displaystyle\\{\mathsf{Pr}\varphi$
$\displaystyle\rightarrow\mathsf{Pr}\psi\mid\varphi\vdash_{\mathsf{BD}}\psi\\}$
$\displaystyle\mathsf{Pr}\neg\varphi$
$\displaystyle\leftrightarrow\neg\mathsf{Pr}\varphi$
$\displaystyle\mathsf{Pr}(\varphi\vee\psi)$
$\displaystyle\leftrightarrow(\mathsf{Pr}\varphi\ominus\mathsf{Pr}(\varphi\wedge\psi))\oplus\mathsf{Pr}\psi$

outer logic:

the axiomatisation of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
of Definition 4.12, instantiated in outer formulas.

A _proof_ of a formula $\alpha$ from a set of assumptions $\Gamma$ in the
logic
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$
(in short
$\Gamma\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$),
where $\Gamma\cup\\{\alpha\\}$ is a finite set of _outer formulas_ , is a
finite tree which can be parsed as follows: the smallest proofs consist of
either (i) a finite tree labelled by $\mathsf{BD}$ formulas, proving
$\varphi\vdash_{\mathsf{BD}}\psi$, followed by the instance
$\mathsf{Pr}\varphi\rightarrow\mathsf{Pr}\psi$ of the first modal axiom, or
(ii) a node labelled by an instance of either of the remaining two modal
axioms or an instance of an axiom of the outer logic in the outer language, or
(iii) an assumption $\beta\in\Gamma$ in the outer language. More complex
proofs are then formed inductively in the standard manner, by means of
syntactically correct applications of the rules of the outer logic to smaller
proofs. The root of the tree is to be labelled by $\alpha$.

######  Theorem 4.24 (FSSC of
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$).

For each $\Gamma,\alpha$ a finite set of outer formulas,

$\Gamma\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha\
\ \mbox{iff}\ \
\Gamma\vDash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha.$

###### Proof.

The soundness and completeness proof essentially relies on the two-layered
nature of the logic. We will use the following facts: (i) the inner logic
$\mathsf{BD}$ is strongly sound and complete w.r.t. its double-valuation
semantics, and it is locally finite, (ii) the outer logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
is finitely strongly sound and complete w.r.t. the outer algebra
$[0,1]^{\Join}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$,
and (iii) the modal axioms are a sound and complete axiomatisation of
probablities over $\mathsf{BD}$ probabilistic models.

Soundness: Given a proof
$\Gamma\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$
and any $\mathsf{BD}$ probabilistic model
$\mathscr{M}=(S,v^{+},v^{-},\mathtt{p})$, we reason inductively: (i) we know
that any proof of $\varphi\vdash_{\mathsf{BD}}\psi$ is sound, therefore it
entails that $|\varphi|^{+}\subseteq|\psi|^{+}$ and
$|\psi|^{-}\subseteq|\varphi|^{-}$ in any $\mathsf{BD}$ model, and thus in
$\mathscr{M}$. This entails that
$\mathtt{p}(|\varphi|^{+})\leq\mathtt{p}(|\psi|^{+})$ and
$\mathtt{p}(|\psi|^{-})\leq\mathtt{p}(|\varphi|^{-})$, and the following
instance $\mathsf{Pr}\varphi\rightarrow\mathsf{Pr}\psi$ of the first modal
axiom is justified, as it results in the value $(1,0)$ in the outer algebra.
The rest of the proof follows from the soundness of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
provided the rest of the modal axioms are sound. Assume an instance
$\mathsf{Pr}\neg\varphi\leftrightarrow\neg\mathsf{Pr}\varphi$ of the second
modal axiom: its left-hand side $\mathsf{Pr}\neg\varphi$ amounts to
$(\mathtt{p}(|\neg\varphi|^{+}),\mathtt{p}(|\neg\varphi|^{-}))=(\mathtt{p}(|\varphi|^{-}),\mathtt{p}(|\varphi|^{+}))$
which is the semantics of $\neg\mathsf{Pr}\varphi$ as desired.

Assume now an instance
$\mathsf{Pr}(\varphi\vee\psi)\leftrightarrow(\mathsf{Pr}\varphi\ominus\mathsf{Pr}(\varphi\wedge\psi))\oplus\mathsf{Pr}\psi$
of the third modal axiom: Its left-hand side $\mathsf{Pr}(\varphi\vee\psi)$
amounts to

$(\mathtt{p}(|\varphi|^{+}\cup|\psi|^{+}),\mathtt{p}(|\varphi|^{-}\cap|\psi|^{-})).$

The first coordinate we know to satisfy

$\mathtt{p}(|\varphi|^{+}\cup|\psi|^{+})=\mathtt{p}(|\varphi|^{+})+\mathtt{p}(|\psi|^{+})-\mathtt{p}(|\varphi|^{+}\cap|\psi|^{+})$

directly by the axiom (iii) of Definition 3.2, while the second coordinate
satisfies

$\mathtt{p}(|\varphi|^{-}\cap|\psi|^{-})=\mathtt{p}(|\varphi|^{-})+\mathtt{p}(|\psi|^{-})-\mathtt{p}(|\varphi|^{-}\cup|\psi|^{-}).$

The first coordinate immediately matches

$v_{1}((\mathsf{Pr}\varphi\ominus\mathsf{Pr}(\varphi\wedge\psi))\oplus\mathsf{Pr}\psi)=(v_{1}(\mathsf{Pr}\varphi)-v_{1}(\mathsf{Pr}(\varphi\wedge\psi)))+v_{1}(\mathsf{Pr}\psi),$

because $(|\varphi|^{+}\cap|\psi|^{+})\leq\mathtt{p}(|\varphi|^{+})$ by
monotonicity and therefore the truncated
$\ominus_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
semantics outputs
$v_{1}(\mathsf{Pr}\varphi)-v_{1}(\mathsf{Pr}(\varphi\wedge\psi))$ and does not
trivialise to $0$. The second coordinate

$v_{2}((\mathsf{Pr}\varphi\ominus\mathsf{Pr}(\varphi\wedge\psi))\oplus\mathsf{Pr}\psi)=(v_{2}(\mathsf{Pr}(\varphi\wedge\psi))\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{2}(\mathsf{Pr}\varphi))\&_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{2}(\mathsf{Pr}\psi)$

and because now by monotonicity
$\mathtt{p}(|\varphi\wedge\psi|^{-})=\mathtt{p}(|\varphi|^{-}\cup|\psi|^{-})\geq\mathtt{p}(|\varphi|^{-})$,
the implication does not trivialise to $1$ and this computes exactly as
required.

Completeness: Assume that
$\Gamma\nvdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$.
We will show that there is $\mathsf{BD}$ probabilistic model validating
$\Gamma$ while refuting $\alpha$. We will use the canonical model
$\mathscr{M}_{c}=(\mathcal{P}(\mathsf{Lit}),v_{c}^{+},v_{c}^{-})$ of
Definition 3.5 to do so. Consider the finite set of $\mathsf{BD}$ subformulas
of modal atoms of $\Gamma,\Phi$ to be given by

$\mathtt{Sf}_{\Gamma,\alpha}\coloneqq\\{\varphi\mid\exists\varphi^{\prime}:\mathsf{Pr}\varphi^{\prime}\mbox{
a modal atom of }\Gamma\cup\\{\alpha\\}\mbox{ and }\varphi\mbox{ a subformula
of }\varphi^{\prime}\\}.$

Because $\mathsf{BD}$ is locally finite, also the set

$\Phi_{\Gamma,\alpha}\coloneqq\\{\psi\mid\exists\varphi\in\mathtt{Sf}_{\Gamma,\alpha}\
\mbox{ and }\ \varphi\dashv\vdash_{\mathsf{BD}}\psi\\}$

is finite. Now define the finite set $\Sigma$ of outer formulas to contain all
instances of the modal axioms for formulas from $\Phi_{\Gamma,\alpha}$.

Given that
$\Gamma\nvdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$,
it is obviously also the case that
$\Gamma,\Sigma\nvdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$.
Then we know, by FSSC of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
that there is a refuting valuation

$v:\\{\mathsf{Pr}\varphi\mid\varphi\in\Phi_{\Gamma,\alpha}\\}\to[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},$

i.e. $v[\Gamma\cup\Sigma]\subseteq\\{(1,0)\\}$ while $v(\alpha)<(1,0)$.
Because $v[\Sigma]\subseteq\\{(1,0)\\}$, and $\Sigma$ in fact fully describes
behaviour of a probability on the $\mathsf{BD}$ formula algebra generated by
propositional atoms from the set $\Phi_{\Gamma,\alpha}$, we define the
probability of a $\mathsf{BD}$ formula $\phi\in\Phi_{\Gamma,\alpha}$ to be

$(\mathtt{p}^{+}(\varphi),\mathtt{p}^{-}(\varphi))=v(\mathsf{Pr}\varphi).$

It is then a routine to check that this assignment indeed is a probability on
the respective formula algebra. Therefore, by Theorem 3.4, we know that this
map can be extended to act as a probability on the powerset of the canonical
$\mathsf{BD}$ model
$(\mathcal{P}(\mathsf{Lit}),v^{+},v^{-},\mathtt{p}^{\prime})$ with
$\mathsf{Lit}$ being the finite set of literals from the set
$\Phi_{\Gamma,\alpha}$, i.e.
$\mathtt{p}^{+}(\varphi)=\mathtt{p}^{\prime}(|\varphi|^{+})$ and
$\mathtt{p}^{-}(\varphi)=\mathtt{p}^{\prime}(|\varphi|^{-})$ for each formula
from the set $\Phi_{\Gamma,\alpha}$. This concludes the proof. ∎

######  Example 4.3.

Assume for example that ${\sim}\mathsf{Pr}(\varphi\wedge\neg\varphi)$, i.e.
that the positive probability of the contradiction is $0$. Observe that then
positive probability of $(\varphi\vee\neg\varphi)$ is $1$:

${\sim}\mathsf{Pr}(\varphi\wedge\neg\varphi)\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}{\sim}\neg{\sim}\mathsf{Pr}(\varphi\wedge\neg\varphi)\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}{\sim}{\sim}\neg\mathsf{Pr}(\varphi\wedge\neg\varphi)\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\neg\mathsf{Pr}(\varphi\wedge\neg\varphi)\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\mathsf{Pr}(\varphi\vee\neg\varphi).$

From the third axiom we then obtain

$\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}(\mathsf{Pr}\varphi\ominus\mathsf{Pr}(\varphi\wedge\neg\varphi))\oplus\mathsf{Pr}\neg\varphi$

which is equivalent (and therefore provably so) to

$\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}(\mathsf{Pr}\varphi\rightarrow\mathsf{Pr}(\varphi\wedge\neg\varphi))\rightarrow\mathsf{Pr}\neg\varphi.$

It is easy to prove that
${\sim}\mathsf{Pr}(\varphi\wedge\neg\varphi)\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}(\mathsf{Pr}\varphi\rightarrow\mathsf{Pr}(\varphi\wedge\neg\varphi))\leftrightarrow{\sim}\mathsf{Pr}\varphi$,
and from that we obtain

${\sim}\mathsf{Pr}(\varphi\wedge\neg\varphi)\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}{\sim}\mathsf{Pr}\varphi\rightarrow\neg\mathsf{Pr}\varphi\vdash_{\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}{\sim}{\neg}\mathsf{Pr}\varphi\rightarrow\mathsf{Pr}\varphi.$

As ${\sim}{\neg}\mathsf{Pr}\varphi\rightarrow\mathsf{Pr}\varphi$ and
$\mathsf{Pr}\varphi\rightarrow{\sim}{\neg}\mathsf{Pr}\varphi$ are provable
from each other (cf. Example 4.1), we can see that assuming that
${\sim}\mathsf{Pr}(\varphi\wedge\neg\varphi)$ entails that
$\mathsf{Pr}\varphi$ is classical. On the other hand, assuming
$\mathsf{Pr}\varphi$ is classical, we can prove that
${\sim}\mathsf{Pr}(\varphi\wedge\neg\varphi)\leftrightarrow\mathsf{Pr}(\varphi\vee\neg\varphi)$.

###  4.4 Two-layered logics for belief and plausibility functions

In this subsection, we introduce two logics formalising two different two-
dimensional interpretations of belief and plausibility. The first option is to
treat the belief modality $\mathsf{B}$ as a ‘Belnapian belief’ described in
Section 3.3.1. This way, _the negative support_ of $\mathsf{B}\phi$ is equal
to $\mathtt{bel}(|\phi|^{-})$ (i.e., the belief in $\phi$’s negative
extension). The _plausibility of $\phi$_ can be defined in terms of its belief
(cf. Remark 4.7 for the details).

The second option is to interpret belief and plausibility as two independent
measures. In this approach, $\mathsf{B}\phi$’s negative support to be equal to
the _plausibility of $\neg\phi$_ as presented in Section 3.3.2. Dually, the
negative support of $\mathsf{Pl}\phi$ _is the belief in $\neg\phi$_.

These two approaches require two different logics.
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
is more suitable to formalise the Belnapian belief since the validity takes
into account both positive and negative supports and since the belief modality
should act in a symmetric manner. On the other hand,
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
is better suited to formalise the reasoning with independent $\mathtt{bel}$
and $\mathtt{pl}$ since it can separate positive and negative supports of a
given statement (recall Example 4.2).

####  4.4.1 Two-layered logic for belief functions

######  Definition 4.25 (Language and semantics of
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$).

The two-layered language of the logic
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$
is of the form
$(\mathscr{L}_{\mathsf{BD}},\\{\mathsf{B}\\},\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}})$,
with a unary modality $\mathsf{B}$, and is defined as follows:

inner formulas:

formulas of $\mathscr{L}_{\mathsf{BD}}$

atomic modal formulas:

Let $\phi\in\mathscr{L}_{\mathsf{BD}}$, then $\mathsf{B}\phi$ is a modal
atomic formula.

outer formulas:

Let $\mathsf{B}\phi$ range over modal atomic formulas, the set of outer
formulas is defined via the following grammar, with the connectives of
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$:

$\alpha\coloneqq\mathsf{B}\phi\mid\neg\alpha\mid\alpha\rightarrow\alpha\mid{\sim}\alpha\mid\triangle\alpha.$

Other connectives: $\bot$, $\wedge$, $\vee$, $\&$, $\ominus$, and $\oplus$,
can be defined as in
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$
of Definition 4.11.

The semantics of the two-layered language is given over a $\mathsf{DS}$ model
$\mathscr{M}=(W,v^{+},v^{-},\mathtt{bel})$, and the outer algebra
$[0,1]^{\Join}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$,
as follows:

inner formulas:

for each $\phi\in\mathscr{L}_{\mathsf{BD}}$ the model provides sets
$|\phi|^{+}=\\{w\mid w\vDash^{+}\phi\\}$ and $|\phi|^{-}=\\{w\mid
w\vDash^{-}\phi\\}$, as described in Definition 2.2.

atomic modal formulas:

for each atomic modal formula $\mathsf{B}\phi$,
$v^{\mathscr{M}}(\mathsf{B}\phi)$ in
$[0,1]^{\Join}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
is defined as

$v^{\mathscr{M}}(\mathsf{B}\phi)=(v^{\mathscr{M}}_{1}(\mathsf{B}\phi),v^{\mathscr{M}}_{2}(\mathsf{B}\phi))\coloneqq(\mathtt{bel}(|\phi|^{+}),\mathtt{bel}(|\phi|^{-}))=\left(\sum\limits_{X\subseteq|\phi|^{+}}\\!\\!\\!\\!\\!\mathtt{m}_{\mathtt{bel}}(X),\sum\limits_{X\subseteq|\phi|^{-}}\\!\\!\\!\\!\\!\mathtt{m}_{\mathtt{bel}}(X)\right).$

outer formulas:

The map $v^{\mathscr{M}}$ is extended to the outer formulas in an expected
manner, following the Definition 4.11 of the interpretation of
$\mathscr{L}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}$
connectives in the algebra
$[0,1]^{\Join}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$.

The outer formula $\alpha$ is said to be valid in $\mathscr{M}$, if
$v^{\mathscr{M}}(\alpha)$ is designated (i.e.
$v^{\mathscr{M}}(\alpha)=(1,0)$). It is said to be valid if it is valid in all
$\mathsf{DS}$ models. The consequence relation for $\Gamma,\alpha$ a set of
outer formulas is defined as

$\Gamma\vDash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha\
\ \mbox{iff}\ \
\forall\mathscr{M}(v^{\mathscr{M}}[\Gamma]\subseteq(1,0)\Rightarrow
v^{\mathscr{M}}(\alpha)=(1,0)).$

######  Remark 4.7.

Note that we can also introduce a definable modality $\mathsf{Pl}$ into
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$.
Indeed, since we can interpret $1-\mathtt{bel}(|\neg\phi|^{+})$ as the value
of the _plausibility_ of $\phi$ (recall Lemma 2.11), we have that the
following equivalence is valid:

$\mathsf{Pl}\phi\leftrightarrow{\sim}\mathsf{B}\neg\phi$

######  Definition 4.26 (Belief function axioms).

We define a sequence of outer formulas $\gamma_{n}$ in propositional letters
of the inner language $p_{1},\ldots,p_{n}$ inductively as follows:

$\displaystyle\gamma_{1}$ $\displaystyle\coloneqq\mathsf{B}p_{1}$
$\displaystyle\gamma_{n+1}$
$\displaystyle\coloneqq\gamma_{n}\oplus(\mathsf{B}p_{n+1}\ominus\gamma_{n}[\mathsf{B}\psi:\mathsf{B}(\psi\wedge
p_{n+1})\mid\mathsf{B}\psi\mbox{ atoms of }\gamma_{n}])$

where $\gamma_{n}[\mathsf{B}\psi:\mathsf{B}(\psi\wedge
p_{n+1})\mid\mathsf{B}\psi\mbox{ modal atoms of }\gamma_{n}])$ is the result
of replacing each modal atom $\mathsf{B}\psi$ in $\gamma_{n}$ with the modal
atom $\mathsf{B}(\psi\wedge p_{n+1})$ (semantically, it is a relativisation of
the corresponding belief function to the sets $|p_{n+1}|^{+-}$).

The $n$-th belief function axiom (i.e. the $n$-monotonicity) is expressed by
substitution instances (substituting inner formulas for the atomic letters
$p_{1},\ldots,p_{n}$) of

$\alpha_{n}\coloneqq\gamma_{n}\rightarrow\mathsf{B}\left(\bigvee_{i=1}^{n}p_{n}\right).$

######  Lemma 4.27 (Soundness of the axioms).

The modal axioms $\alpha_{n}$ are sound w.r.t. $\mathsf{DS}$ models.

###### Proof.

We need to prove that the axioms introduced in Definition 4.26 are sound, i.e.
that the formulas $\gamma_{n}$ indeed express semantically the appropriate
sums from Definition 2.6. Because of the two-dimensional nature of the
semantics of the modality

$v^{\mathscr{M}}(\mathsf{B}\phi)=(v^{\mathscr{M}}_{1}(\mathsf{B}\phi),v^{\mathscr{M}}_{2}(\mathsf{B}\phi))\coloneqq(\mathtt{bel}(|\phi|^{+}),\mathtt{bel}(|\phi|^{-})),$

we need to consider both $\mathtt{bel}^{+}$ as a general belief function on
the Lindenbaum algebra $\mathscr{L}_{\mathsf{BD}}$, and $\mathtt{bel}^{-}$ as
a general belief function on its dual $\mathscr{L}_{\mathsf{BD}}^{op}$.

Recall that $\mathtt{bel}^{+}$ on $\mathscr{L}_{\mathsf{BD}}$ is _$n$
-monotone_ if, for every $a_{1},\ldots,a_{n}$, it holds that

$\mathtt{bel}^{+}\left(\bigvee\limits^{n}_{i=1}a_{i}\right)\geq\sum\limits_{\scriptsize{\begin{matrix}J\subseteq\\{1,\ldots,n\\}\\\
J\neq\varnothing\end{matrix}}}(-1)^{|J|+1}\cdot\mathtt{bel}^{+}\left(\bigwedge\limits_{j\in
J}a_{j}\right).$

What the sum expresses is that we always add ($+$) beliefs of conjunctions of
an odd size, while we subtract ($-$) beliefs of conjunctions of an even size.
To write down exactly the same sum as a
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
formula is however more problematic than in the probability case because the
sums and subtractions of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
are truncated to stay within the margins of $[0,1]$ and we have to be careful
to reflect this in the way we arrange the elements of the sum so that we never
lose information. We first need to see that the axioms can indeed be re-
defined recursively as follows ($\mathtt{t}_{n}$ now denote terms in the
language of linear inequalities):

$\displaystyle\mathtt{t}_{1}$ $\displaystyle\coloneqq\mathtt{bel}^{+}(a_{1})$
$\displaystyle\mathtt{t}_{n+1}$
$\displaystyle\coloneqq\mathtt{t}_{n}+(\mathtt{bel}^{+}(a_{n+1})-\mathtt{t}_{n}[\mathtt{bel}^{+}(\psi):\mathtt{bel}^{+}(\psi\wedge
a_{n+1})\mid\mathtt{bel}^{+}(\psi)\ \mbox{atoms of}\ \mathtt{t}_{n}])$

The $n$-th axiom is now written as (the trivial case of $n=1$ is included for
convenience):

$\mathtt{t}_{n}\leq\mathtt{bel}^{+}\left(\bigvee_{i=1}^{n}a_{n}\right).$

The intuition behind this definition comes from the powerset algebras and it
is geometrical. In each inductive step, we look at what happens if we add one
more set (element $a_{n+1}$) to the union: we keep the sum we had so far
($\mathtt{t}_{n}$), add $\mathtt{bel}(a_{n+1})$, and subtract the sum we had
_relativised_ to $\mathtt{bel}(a_{n+1})$ (replacing beliefs of the sets in the
original sum by beliefs of their intersection with the new set $a_{n+1}$).
That the two definitions are equivalent can be proven by a routine (but
tedious) induction. The whole point of this definition is that in the above,

$\mathtt{bel}^{+}(a_{n+1})\geq\mathtt{t}_{n}[\mathtt{bel}^{+}(\psi):\mathtt{bel}^{+}(\psi\wedge
a_{n+1})\mid\mathtt{bel}^{+}(\psi)\ \mbox{atoms of}\ \mathtt{t}_{n}],$

and therefore

$0\leq\mathtt{bel}^{+}(a_{n+1})-\mathtt{t}_{n}[\mathtt{bel}^{+}(\psi):\mathtt{bel}^{+}(\psi\wedge
a_{n+1})\mid\mathtt{bel}^{+}(\psi)\ \mbox{atoms of}\ \mathtt{t}_{n}]\leq 1.$

Dually, recall that as $\mathtt{bel}^{-}$ is a general belief function on
$\mathscr{L}_{\mathsf{BD}}^{op}$, then for every $a_{1},\ldots,a_{n}$ it holds
that

$\mathtt{bel}^{-}\left(\bigwedge\limits^{n}_{i=1}a_{i}\right)\leq\sum\limits_{\scriptsize{\begin{matrix}J\subseteq\\{1,\ldots,n\\}\\\
J\neq\varnothing\end{matrix}}}(-1)^{|J|+1}\cdot\mathtt{bel}^{-}\left(\bigvee\limits_{j\in
J}a_{j}\right).$

These axioms can be re-defined recursively as follows (this is tailored to be
expressed in the Łukasiewicz language):

$\displaystyle\mathtt{s}_{1}$ $\displaystyle\coloneqq\mathtt{bel}^{-}(a_{1})$
$\displaystyle\mathtt{s}_{n+1}$
$\displaystyle\coloneqq(\mathtt{s}_{n}+1-\mathtt{s}_{n}[\mathtt{bel}^{-}(\psi):\mathtt{bel}^{-}(\psi\vee
a_{n+1})\mid\mathtt{bel}^{-}(\psi)\ \mbox{atoms of}\
\mathtt{s}_{n}])-(1-\mathtt{bel}^{-}(a_{n+1})).$

The $n$-th axiom is now written as:

$\mathtt{s}_{n}\geq\mathtt{bel}^{-}\left(\bigwedge_{i=1}^{n}a_{n}\right).$

The main reason we did it this particular way is that now the following sum
stays within margins of $[0,1]$ (and therefore directly corresponds to a Ł
formula):

$0\leq\mathtt{s}_{n}+1-\mathtt{s}_{n}[\mathtt{bel}^{-}(\psi):\mathtt{bel}^{-}(\psi\vee
a_{n+1})\mid\mathtt{bel}^{-}(\psi)\ \mbox{atoms of}\ \mathtt{s}_{n}]\leq 1.$

It remains to show that for each $n$ and each $\mathsf{DS}$ model
$(S,v^{+},v^{-},\mathtt{bel})$ we will have

$v_{1}(\gamma_{n})\leq\mathtt{bel}\left|\bigvee_{i=1}^{n}p_{n}\right|^{+}\mbox{
and}\quad
v_{2}(\gamma_{n})\geq\mathtt{bel}\left|\bigvee_{i=1}^{n}p_{n}\right|^{-}.$

The case $n=1$ is trivial, we, therefore, go directly for the recursion step.
For the first coordinate,

$\displaystyle v_{1}(\gamma_{n+1})$
$\displaystyle=v_{1}(\gamma_{n})\oplus_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}(\mathtt{bel}(|p_{n+1}|^{+})\ominus_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}v_{1}(\gamma_{n}[\mathsf{B}\psi:\mathsf{B}(\psi\wedge
p_{n+1})]))$
$\displaystyle=\mathtt{t}_{n}(|p_{1}|^{+},\ldots,|p_{n}|^{+})+(\mathtt{bel}(|p_{n+1}|^{+})-\mathtt{t}_{n}[\mathtt{bel}(|\psi|^{+}):\mathtt{bel}(|\psi\wedge
p_{n+1}|^{+})])$
$\displaystyle=\mathtt{t}_{n}+(\mathtt{bel}(|p_{n+1}|^{+})-\mathtt{t}_{n}[\mathtt{bel}(|\psi|^{+}):\mathtt{bel}(|\psi|^{+}\cap|p_{n+1}|^{+})])$
$\displaystyle\leq\mathtt{bel}\bigcup_{i=1}^{n}|p_{n}|^{+}=\mathtt{bel}\left|\bigvee_{i=1}^{n}p_{n}\right|^{+}.$

For the second coordinate,

$\displaystyle v_{2}(\gamma_{n+1})$
$\displaystyle=v_{2}(\gamma_{n})~{}\&_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}~{}(v_{2}(\gamma_{n}[\mathsf{B}\psi:\mathsf{B}(\psi\wedge
p_{n+1})])\rightarrow_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}\mathtt{bel}(|p_{n+1}|^{-}))$
$\displaystyle=(v_{2}(\gamma_{n})\oplus_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}v_{2}(\gamma_{n}[\mathsf{B}\psi:\mathsf{B}(\psi\wedge
p_{n+1})]))\ominus_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}{\sim_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\mathtt{bel}(|p_{n+1}|^{-})$
$\displaystyle=(\mathtt{s}_{n}(|p_{1}|^{-},\ldots,|p_{n}|^{-})+1-\mathtt{s}_{n}[\mathtt{bel}(|\psi|^{-}):\mathtt{bel}(|\psi\vee
p_{n+1}|^{-})])-(1-\mathtt{bel}(|p_{n+1}|^{-}))$
$\displaystyle=(\mathtt{s}_{n}+1-\mathtt{s}_{n}[\mathtt{bel}(|\psi|^{-}):\mathtt{bel}(|\psi|^{-}\cap|p_{n+1}|^{-})])-(1-\mathtt{bel}(|p_{n+1}|^{-}))$
$\displaystyle\geq\mathtt{bel}\bigcap_{i=1}^{n}\left|p_{n}\right|^{-}=\mathtt{bel}\left|\bigvee_{i=1}^{n}p_{n}\right|^{-}$

∎

######  Definition 4.28 (Axiomatisation of
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$).

The two-layered axiomatisation of logic
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}=(\mathsf{BD},M_{b},{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2})$
consists of

inner logic:

the axiomatisation of $\mathsf{BD}$ of Definition 2.1

modal axioms:

$M_{b}$:

$\displaystyle\\{\mathsf{B}\varphi$
$\displaystyle\rightarrow\mathsf{B}\psi\mid\varphi\vdash_{\mathsf{BD}}\psi\\}$
$\displaystyle\mathsf{B}\neg\varphi$
$\displaystyle\leftrightarrow\neg\mathsf{B}\varphi$
$\displaystyle\\{\alpha_{n}\ $ $\displaystyle|\ n\in\mathbb{N}\\}\mbox{
(substitution instances of)}$

outer logic:

the axiomatisation of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
of Definition 4.12

A proof of a formula $\alpha$ from a set of assumptions $\Gamma$ in the logic
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$
(in short
$\Gamma\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$),
where $\Gamma,\alpha$ is a finite set of outer formulas, is a finite tree
which can be parsed as follows: the smallest proofs consist of either (i) a
finite tree labeled by $\mathsf{BD}$ formulas, proving
$\varphi\vdash_{\mathsf{BD}}\psi$, followed by the instance
$\mathsf{B}\varphi\rightarrow\mathsf{B}\psi$ of the first modal axiom, or (ii)
a node labelled by an instance of the remaining two modal axioms or an
instance of an axiom of the outer logic in the outer language, or (iii) an
assumption $\beta\in\Gamma$ in the outer language. More complex proofs are
then formed inductively in the standard manner, by means of syntactically
correct applications of the rules of the outer logic to smaller proofs. The
root of the tree is to be labelled by $\alpha$.

######  Theorem 4.29 (FSSC of
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$).

For each $\Gamma,\alpha$ a finite set of outer formulas,

$\Gamma\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha\
\ \mbox{iff}\ \
\Gamma\vDash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha.$

###### Proof.

The soundness and completeness proof essentially relies on the two-layered
nature of the logic. We will use the following facts: (i) the inner logic
$\mathsf{BD}$ is strongly sound and complete w.r.t. its double-valuation
semantics, and it is locally finite, (ii) the outer logic
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
is finitely strongly sound and complete w.r.t. the outer algebra
$[0,1]^{\Join}_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$,
and (iii) the modal axioms are a sound and complete axiomatisation of belief
functions over $\mathsf{DS}$ models.

Soundness: Given a proof
$\Gamma\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$
and any $\mathsf{DS}$ model $\mathscr{M}=(S,v^{+},v^{-},\mathtt{bel})$, we
reason inductively: (i) we know that any proof of
$\varphi\vdash_{\mathsf{BD}}\psi$ is sound, therefore it entails that
$|\varphi|^{+}\subseteq|\psi|^{+}$ and $|\psi|^{-}\subseteq|\varphi|^{-}$ in
any $\mathsf{BD}$ model, and thus in $\mathscr{M}$. This entails that
$\mathtt{bel}^{+}\varphi\leq\mathtt{bel}^{+}\psi$ and
$\mathtt{bel}^{-}\psi\leq\mathtt{bel}^{-}\varphi$, and the following instance
$\mathsf{B}\varphi\rightarrow\mathsf{B}\psi$ of the first modal axiom is
justified, as it results in the value $(1,0)$ in the outer algebra. The rest
of the proof follows from the soundness of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
providing the rest of the modal axioms are sound. Assume an instance
$\mathsf{B}\neg\varphi\leftrightarrow\neg\mathsf{B}\varphi$ of the second
modal axiom: Its left-hand side $\mathsf{B}\neg\varphi$ amounts to
$(\mathtt{bel}|\neg\varphi|^{+},\mathtt{bel}|\neg\varphi|^{-})=(\mathtt{bel}|\varphi|^{-},\mathtt{bel}|\varphi|^{+})$
which is the semantics of $\neg\mathsf{B}\varphi$ as desired. The soundness of
the axioms $\alpha_{n}$ has been demonstrated in Lemma 4.27.

Completeness: Assume that
$\Gamma\nvdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$.
We will show that there is $\mathsf{DS}$ model validating $\Gamma$ while
refuting $\alpha$. We will again use the canonical model
$\mathscr{M}_{c}=(\mathcal{P}(\mathsf{Lit}),v_{c}^{+},v_{c}^{-})$ of
Definition 3.5 to do so. Consider the finite set of $\mathsf{BD}$ subformulas
of modal atoms of $\Gamma,\Phi$ to be given by

$\mathtt{Sf}_{\Gamma,\alpha}\coloneqq\\{\varphi\mid\exists\varphi^{\prime}\
\mathsf{B}\varphi^{\prime}\mbox{ a modal atom of }\Gamma\cup\\{\alpha\\}\mbox{
and }\varphi\mbox{ a subformula of }\varphi^{\prime}\\}.$

Because $\mathsf{BD}$ is locally finite, also the set

$\Phi_{\Gamma,\alpha}\coloneqq\\{\psi\mid\exists\varphi\in\mathtt{Sf}_{\Gamma,\alpha}\
\mbox{ and }\ \varphi\dashv\vdash_{\mathsf{BD}}\psi\\}$

is finite. Now define the finite set $\Sigma$ of outer formulas to contain all
instances of the modal axioms for formulas from $\Phi_{\Gamma,\alpha}$.

Given that
$\Gamma\nvdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$,
it is obviously also the case that
$\Gamma,\Sigma\nvdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\alpha$.
Then we know, by FSSC of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$,
that there is a refuting valuation

$v:\\{\mathsf{B}\varphi\mid\varphi\in\Phi_{\Gamma,\alpha}\\}\to[0,1]^{\Join}_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}},$

i.e. $v[\Gamma\cup\Sigma]\subseteq\\{(1,0)\\}$ while $v(\alpha)<(1,0)$.
Because $v[\Sigma]\subseteq\\{(1,0)\\}$, and $\Sigma$ in fact fully describes
behaviour of a belief function on the $\mathsf{BD}$ formula algebra generated
by propositional atoms from the set $\Phi_{\Gamma,\alpha}$, we define the
belief function of a $\mathsf{BD}$ formula $\phi\in\Phi_{\Gamma,\alpha}$ to be

$(\mathtt{bel}^{+}(\varphi),\mathtt{bel}^{-}(\varphi))=v(\mathsf{B}\varphi).$

It is then a routine to check that this assignment indeed is a belief function
on the respective formula algebra (or its dual). Therefore, by Theorem 3.12,
we know that this map can be extended to a belief function
$\mathtt{bel}^{\prime}$ on the powerset of the canonical $\mathsf{BD}$ model
$(\mathcal{P}(\mathsf{Lit}),v^{+},v^{-},\mathtt{bel}^{\prime})$ with
$\mathsf{Lit}$ being the finite set of literals from the set
$\Phi_{\Gamma,\alpha}$, i.e.
$\mathtt{bel}^{+}(\varphi)=\mathtt{bel}^{\prime}(|\varphi|^{+})$ and
$\mathtt{bel}^{-}(\varphi)=\mathtt{bel}^{\prime}(|\varphi|^{-})$ for each
formula from the set $\Phi_{\Gamma,\alpha}$. This concludes the proof. ∎

######  Example 4.4.

Assume that $\mathsf{B}\varphi$ is classical, i.e. that
$\mathsf{B}\varphi\leftrightarrow{\sim}\neg\mathsf{B}\varphi$. Then, starting
from the $\alpha_{2}$ axiom, and
$\mathsf{B}(\varphi\vee\neg\varphi)\leftrightarrow\neg\mathsf{B}(\varphi\wedge\neg\varphi)$,
we obtain, consequently using the conflation rule and distribution, the
classicality, contraposition, $\vee$-definition, and finally
$\mathsf{B}(\varphi\vee\neg\varphi)\vee\mathsf{B}\neg\varphi\leftrightarrow\mathsf{B}(\varphi\vee\neg\varphi)$:

$\displaystyle\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}((\mathsf{B}\varphi\rightarrow\mathsf{B}(\varphi\wedge\neg\varphi))\rightarrow\mathsf{B}\neg\varphi)\rightarrow\neg\mathsf{B}(\varphi\wedge\neg\varphi)$
$\displaystyle\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}{\sim}\neg((\mathsf{B}\varphi\rightarrow\mathsf{B}(\varphi\wedge\neg\varphi))\rightarrow\mathsf{B}\neg\varphi)\rightarrow\neg\mathsf{B}(\varphi\wedge\neg\varphi)$
$\displaystyle\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}((\mathsf{B}\varphi\rightarrow{\sim}\neg\mathsf{B}(\varphi\wedge\neg\varphi))\rightarrow{\sim}\mathsf{B}\varphi)\rightarrow{\sim}\mathsf{B}(\varphi\wedge\neg\varphi)$
$\displaystyle\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}((\neg\mathsf{B}(\varphi\wedge\neg\varphi)\rightarrow{\sim}\mathsf{B}\varphi)\rightarrow{\sim}\mathsf{B}\varphi)\rightarrow{\sim}\mathsf{B}(\varphi\wedge\neg\varphi)$
$\displaystyle\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}(\neg\mathsf{B}(\varphi\wedge\neg\varphi)\vee{\sim}\mathsf{B}\varphi)\rightarrow{\sim}\mathsf{B}(\varphi\wedge\neg\varphi)$
$\displaystyle\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}(\mathsf{B}(\varphi\vee\neg\varphi)\vee\neg\mathsf{B}\varphi)\rightarrow{\sim}\mathsf{B}(\varphi\wedge\neg\varphi)$
$\displaystyle\vdash_{\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}}\mathsf{B}(\varphi\vee\neg\varphi)\rightarrow{\sim}\mathsf{B}(\varphi\wedge\neg\varphi)$

The converse implication is provable as well. (Also note that the same proof
with $\mathsf{B}$ replaced by $\mathsf{Pr}$ would work for probabilities, thus
extending the Example 4.3).

####  4.4.2 Two-layered logic for belief and plausibility functions

######  Definition 4.30 (Language and semantics of
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$).

The two-layered language of the logic
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
is of the form
$(\mathscr{L}_{\mathsf{BD}},\\{\mathsf{B},\mathsf{Pl}\\},\mathscr{L}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}})$,
with unary modalities $\mathsf{B}$ and $\mathsf{Pl}$, and it is defined as
follows:

inner formulas:

formulas of $\mathscr{L}_{\mathsf{BD}}$

atomic modal formulas:

Let $\phi\in\mathscr{L}_{\mathsf{BD}}$, then $\mathsf{B}\phi$ and
$\mathsf{Pl}\phi$ are modal atomic formulas.

outer formulas:

Let $\mathsf{B}\phi$ and $\mathsf{Pl}\phi$ range over modal atomic formulas,
the set of outer formulas is defined via the following grammar, with the
connectives of
$\mathscr{L}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$:

$\alpha\coloneqq\mathsf{B}\phi\mid\mathsf{Pl}\phi\mid\neg\alpha\mid\alpha\wedge\alpha\mid\alpha\rightarrowtriangle\alpha\mid{\sim}\alpha.$

Other connectives: $\bot$, $\vee$, $\&$, $\ominus$ and $\oplus$, can be
defined as in
$\mathscr{L}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
of Definition 4.17.

The semantics of the two-layered language is given over a
$\mathsf{DS}_{\mathtt{pl}}$ model
$\mathscr{M}=(W,v^{+},v^{-},\mathtt{bel},\mathtt{pl})$, and the outer algebra
$[0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$,
as follows:

inner formulas:

for each $\phi\in\mathscr{L}_{\mathsf{BD}}$ the model provides sets
$|\phi|^{+}=\\{w\mid w\vDash^{+}\phi\\}$ and $|\phi|^{-}=\\{w\mid
w\vDash^{-}\phi\\}$, as described in Definition 2.2.

atomic modal formulas:

for atomic modal formulas $\mathsf{B}\phi$ and $\mathsf{Pl}\phi$,
$v^{\mathscr{M}}(\mathsf{B}\phi)$ and $v^{\mathscr{M}}(\mathsf{Pl}\phi)$ in
$[0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
are defined as follows:

$v^{\mathscr{M}}(\mathsf{B}\phi)=(v^{\mathscr{M}}_{1}(\mathsf{B}\phi),v^{\mathscr{M}}_{2}(\mathsf{B}\phi))\coloneqq(\mathtt{bel}(|\phi|^{+}),\mathtt{pl}(|\phi|^{-}));$
$v^{\mathscr{M}}(\mathsf{Pl}\phi)=(v^{\mathscr{M}}_{1}(\mathsf{Pl}\phi),v^{\mathscr{M}}_{2}(\mathsf{Pl}\phi))\coloneqq(\mathtt{pl}(|\phi|^{+}),\mathtt{bel}(|\phi|^{-})).$

outer formulas:

The map $v^{\mathscr{M}}$ is extended to the outer formulas in an expected
manner, following the Definition 4.11 of the interpretation of
$\mathscr{L}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
connectives in the algebra
$[0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$.

The outer formula $\alpha$ is said to be valid in $\mathscr{M}$, if
$v^{\mathscr{M}}(\alpha)$ is designated (i.e.
$v_{1}^{\mathscr{M}}(\alpha)=1$). It is said to be valid if it is valid in all
$\mathsf{DS}_{\mathtt{pl}}$ models. The consequence relation for
$\Gamma,\alpha$ a set of outer formulas is defined as

$\Gamma\vDash_{\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha\
\ \mbox{iff}\ \
\forall\mathscr{M}(v_{1}^{\mathscr{M}}[\Gamma]\subseteq\\{1\\}\Rightarrow
v_{1}^{\mathscr{M}}(\alpha)=1).$

######  Definition 4.31 (Belief and plausibility functions axioms).

We define sequences of outer formulas $\gamma_{n}$, and $\sigma_{n}$ in
propositional letters of the inner language $p_{1},\ldots,p_{n}$ inductively
as follows:

$\displaystyle\gamma_{1}$ $\displaystyle\coloneqq\mathsf{B}p_{1}$
$\displaystyle\gamma_{n+1}$
$\displaystyle\coloneqq\gamma_{n}\oplus(\mathsf{B}p_{n+1}\ominus\gamma_{n}[\mathsf{B}\psi:\mathsf{B}(\psi\wedge
p_{n+1})\mid\mathsf{B}\psi\mbox{ atoms of }\gamma_{n}])$
$\displaystyle\sigma_{1}$ $\displaystyle\coloneqq\mathsf{Pl}p_{1}$
$\displaystyle\sigma_{n+1}$
$\displaystyle\coloneqq(\sigma_{n}\oplus{\sim}\sigma_{n}[\mathsf{Pl}\psi:\mathsf{Pl}(\psi\vee
p_{n+1})\mid\mathsf{Pl}\psi\mbox{ atoms of
}\sigma_{n}])\ominus{\sim}\mathsf{Pl}p_{n+1}$

where $\gamma_{n}[\mathsf{B}\psi:\mathsf{B}(\psi\wedge
p_{n+1})\mid\mathsf{B}\psi\mbox{ atoms of }\gamma_{n}])$ is the result of
replacing each atom $\mathsf{B}\psi$ in $\gamma_{n}$ with the atom
$\mathsf{B}(\psi\wedge p_{n+1})$, and
$\sigma_{n}[\mathsf{Pl}\psi:\mathsf{Pl}(\psi\vee
p_{n+1})\mid\mathsf{Pl}\psi\mbox{ atoms of }\sigma_{n}]$ is the result of
replacing each atom $\mathsf{Pl}\psi$ in $\sigma_{n}$ with the atom
$\mathsf{Pl}(\psi\vee p_{n+1})$.

The $n$-th belief function axiom (i.e. the $n$-monotonicity) is expressed by
substitution instances (substituting inner formulas for the atomic letters
$p_{1},\ldots,p_{n}$) of

$\alpha_{n}\coloneqq\gamma_{n}\rightarrowtriangle\mathsf{B}\left(\bigvee_{i=1}^{n}p_{n}\right).$

The $n$-th plausibility function axiom is expressed by substitution instances
(substituting inner formulas for the atomic letters $p_{1},\ldots,p_{n}$) of

$\beta_{n}\coloneqq\mathsf{Pl}\left(\bigwedge_{i=1}^{n}p_{n}\right)\rightarrowtriangle\sigma_{n}.$

######  Lemma 4.32 (Soundness of the axioms).

The axioms $\alpha_{n}$ and $\beta_{n}$ are sound w.r.t.
$\mathsf{DS}_{\mathtt{pl}}$ models.

###### Proof.

We need to prove that the axioms introduced in Definition 4.31 are sound, i.e.
that the formulas $\gamma_{n},\sigma_{n}$ indeed express semantically the
appropriate sums from Definition 2.6 and Definition 2.7. First note that the
validity of the axioms $\alpha_{n},\beta_{n}$ means that, for each
$\mathsf{DS}_{\mathtt{pl}}$ model $\mathscr{M}$,
$v^{\mathscr{M}}_{1}(\alpha_{n})=1$ and $v^{\mathscr{M}}_{1}(\beta_{n})=1$.
Thus we only care about the first coordinates. Because the weak implication
still expresses the order of the first coordinates
($(a_{1},a_{2})\rightarrowtriangle(b_{1},b_{2})$ is designated if and only if
$a_{1}\leq b_{1}$), we only need to check that the first coordinates of
formulas $\gamma_{n},\sigma_{n}$ express semantically the appropriate sums
from Definition 2.6 and Definition 2.7. But this can be done exactly as in
proof of Lemma 4.27, using the terms $\mathtt{t}_{n}$ for $\gamma_{n}$, and
straightforward analogues of terms $\mathtt{s}_{n}$ for $\sigma_{n}$. This
follows from the fact, that the $n$-th axiom of the general belief function
$\mathtt{bel}^{-}$ on $\mathscr{L}_{\mathsf{BD}}^{op}$ and the $n$-th axiom of
the general plausibility function $\mathtt{pl}^{+}$ on
$\mathscr{L}_{\mathsf{BD}}$ are of the same shape (not to confuse the two
notions however, notice that while $\mathtt{bel}^{-}$ is antitone on
$\mathscr{L}_{\mathsf{BD}}$, $\mathtt{pl}^{+}$ is monotone on
$\mathscr{L}_{\mathsf{BD}}$). ∎

######  Definition 4.33 (Axiomatisation of
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$).

The two-layered axiomatisation of logic
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}=(\mathsf{BD},M^{\mathbb{N}}_{b},{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}_{(1,1)^{\uparrow}}(\rightarrowtriangle))$

inner logic:

the axiomatisation of $\mathsf{BD}$ of Definition 2.1

modal axioms:

$M_{b}^{\mathbb{N}}$:

$\displaystyle\\{\mathsf{B}\varphi$
$\displaystyle\Rightarrow\mathsf{B}\psi,\mathsf{Pl}\varphi\Rightarrow\mathsf{Pl}\psi\mid\varphi\vdash_{\mathsf{BD}}\psi\\}$
$\displaystyle\mathsf{B}\neg\varphi$
$\displaystyle\Leftrightarrow\neg\mathsf{Pl}\varphi$
$\displaystyle\\{\alpha_{n},\beta_{n}$ $\displaystyle\mid
n\in\mathbb{N}\\}\mbox{ (substitution instances of)}$

outer logic:

the axiomatisation of
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
of Definition 4.18

A proof of a formula $\alpha$ from a set of assumptions $\Gamma$ in the logic
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
(in short
$\Gamma\vdash_{\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha$),
where $\Gamma,\alpha$ is a finite set of outer formulas, is a finite tree
which can be parsed as follows: the smallest proofs consist of either (i) a
finite tree labeled by $\mathsf{BD}$ formulas, proving
$\varphi\vdash_{\mathsf{BD}}\psi$, followed by the instance
$\mathsf{B}\varphi\Rightarrow\mathsf{B}\psi$ or by the instance
$\mathsf{Pl}\varphi\Rightarrow\mathsf{Pl}\psi$ of the first modal axiom, or
(ii) a node labelled by an instance of the remaining two modal axioms or an
instance of an axiom of the outer logic in the outer language, or (iii) an
assumption $\beta\in\Gamma$ in the outer language. More complex proofs are
then formed inductively in the standard manner, by means of syntactically
correct applications of the rules of the outer logic to smaller proofs. The
root of the tree is to be labelled by $\alpha$.

######  Theorem 4.34 (FSSC of
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$).

For each $\Gamma,\alpha$ a finite set of outer formulas,

$\Gamma\vdash_{\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha\
\ \mbox{iff}\ \
\Gamma\vDash_{\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha.$

###### Proof.

The soundness and completeness proof is almost the same as before. We will now
use the following facts: (i) the inner logic $\mathsf{BD}$ is strongly sound
and complete w.r.t. its double-valuation semantics, and it is locally finite,
(ii) the outer logic
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$
is finitely strongly sound and complete w.r.t. the outer algebra
$[0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$,
and (iii) the modal axioms are a sound and complete axiomatisation of belief
and plausibility functions over $\mathsf{DS}_{\mathtt{pl}}$ models.

Soundness: Given a proof
$\Gamma\vdash_{\mathtt{Bel}^{N{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha$
and any $\mathsf{DS}_{\mathtt{pl}}$ model
$\mathscr{M}=(S,v^{+},v^{-},\mathtt{bel},\mathtt{pl})$, we reason inductively:
(i) we know that any proof of $\varphi\vdash_{\mathsf{BD}}\psi$ is sound,
therefore it entails that $|\varphi|^{+}\subseteq|\psi|^{+}$ and
$|\psi|^{-}\subseteq|\varphi|^{-}$ in any $\mathsf{BD}$ model, and thus in
$\mathscr{M}$. This entails that
$\mathtt{bel}(|\varphi|^{+})\leq\mathtt{bel}(|\psi|^{+})$ and
$\mathtt{bel}(|\psi|^{+})\leq\mathtt{bel}(|\varphi|^{+})$, and
$\mathtt{pl}(|\varphi|^{+})\leq\mathtt{pl}(|\psi|^{+})$ and
$\mathtt{pl}(|\psi|^{-})\leq\mathtt{pl}(|\varphi|^{-})$, and either of the
following instances $\mathsf{B}\varphi\Rightarrow\mathsf{B}\psi$ and
$\mathsf{Pl}\varphi\Rightarrow\mathsf{Pl}\psi$ of the first modal axiom is
justified, as it results in a value $(1,x)$ in the outer algebra. The rest of
the proof follows from the soundness of
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$,
providing the rest of the modal axioms are sound. Assume an instance
$\mathsf{B}\neg\varphi\Leftrightarrow\neg\mathsf{Pl}\varphi$ of the second
modal axiom: its left-hand side $\mathsf{B}\neg\varphi$ amounts to
$(\mathtt{bel}(|\neg\varphi|^{+}),\mathtt{pl}(|\neg\varphi|^{-}))=(\mathtt{bel}(|\varphi|^{-}),\mathtt{pl}(|\varphi|^{+}))$
which matches exactly the semantics of $\neg\mathsf{Pl}\varphi$ as desired.
The soundness of the axioms $\alpha_{n}$, and $\beta_{n}$ has been
demonstrated in Lemma 4.32.

Completeness: Assume that
$\Gamma\nvdash_{\mathtt{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha$.
We will show that there is $\mathsf{DS}_{\mathtt{pl}}$ model validating
$\Gamma$ while refuting $\alpha$. We will again use the canonical model
$\mathscr{M}_{c}=(\mathcal{P}(\mathsf{Lit}),v_{c}^{+},v_{c}^{-})$ of
Definition 3.5 to do so. Consider the finite set of $\mathsf{BD}$ subformulas
of modal atoms of $\Gamma,\Phi$ to be given by

$\mathtt{Sf}_{\Gamma,\alpha}\coloneqq\\{\varphi\mid\exists\mathsf{M}\\!\in\\!\\{\mathsf{B},\mathsf{Pl}\\}~{}\exists\varphi^{\prime}:\mathsf{M}\varphi^{\prime}\mbox{
a modal atom of }\Gamma\cup\\{\alpha\\}\mbox{ and }\varphi\mbox{ a subformula
of }\varphi^{\prime}\\}.$

Because $\mathsf{BD}$ is locally finite, also the set

$\Phi_{\Gamma,\alpha}\coloneqq\\{\psi\mid\exists\varphi\in\mathtt{Sf}_{\Gamma,\alpha}\
\mbox{ and }\ \varphi\dashv\vdash_{\mathsf{BD}}\psi)\\}$

is finite. Now define the finite set $\Sigma$ of outer formulas to contain all
instances of the modal axioms for formulas from $\Phi_{\Gamma,\alpha}$.

Given that
$\Gamma\nvdash_{\mathtt{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha$,
it is obviously also the case that
$\Gamma,\Sigma\nvdash_{\mathtt{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}}\alpha$.
Then we know, by FSSC of
$\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}$,
that there is a refuting valuation

$v:\\{\mathsf{B}\varphi\mid\varphi\in\Phi_{\Gamma,\alpha}\\}\to[0,1]^{\Join}_{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}},$

i.e. $v_{1}[\Gamma\cup\Sigma]\subseteq\\{1\\}$ while $v_{1}(\alpha)<1$.
Because $v_{1}[\Sigma]\subseteq\\{1\\}$, and $\Sigma$ in fact fully describes
behaviour of a belief or plausibility function on the $\mathsf{BD}$ formula
algebra generated by propositional atoms from the set $\Phi_{\Gamma,\alpha}$,
we can define the belief functions $\mathtt{bel}^{+},\mathtt{bel}^{-}$ and the
plausibility functions $\mathtt{pl}^{+},\mathtt{pl}^{-}$ of a $\mathsf{BD}$
formula $\varphi\in\Phi_{\Gamma,\alpha}$ to be

$\displaystyle\mathtt{bel}^{+}(\varphi)=v_{1}(\mathsf{B}\varphi)$
$\displaystyle\mathtt{bel}^{-}(\varphi)=v_{2}(\mathsf{Pl}\varphi)$
$\displaystyle\mathtt{pl}^{+}(\varphi)=v_{1}(\mathsf{Pl}\varphi)$
$\displaystyle\mathtt{pl}^{-}(\varphi)=v_{2}(\mathsf{B}\varphi).$

It is then a routine to check that this assignment indeed results in belief
and plausibility functions on the respective formula algebra (or its dual).

Therefore, by Theorem 3.12 and Theorem 3.13, we know that $\mathtt{bel}$ can
be extended to a belief function $\mathtt{bel}^{\prime}$, and $\mathtt{pl}$ to
$\mathtt{pl}^{\prime}$, on the powerset of the canonical $\mathsf{BD}$ model
$(\mathcal{P}(\mathsf{Lit}),v^{+},v^{-},\mathtt{bel}^{\prime},\mathtt{pl}^{\prime})$
with $\mathsf{Lit}$ being the finite set of literals from the set
$\Phi_{\Gamma,\alpha}$, i.e.
$\mathtt{bel}^{+}(\varphi)=\mathtt{bel}^{\prime}(|\varphi|^{+})$,
$\mathtt{bel}^{-}(\varphi)=\mathtt{bel}^{\prime}(|\varphi|^{-})$,
$\mathtt{pl}^{+}(\varphi)=\mathtt{pl}^{\prime}(|\varphi|^{+})$ and
$\mathtt{pl}^{-}(\varphi)=\mathtt{pl}^{\prime}(|\varphi|^{-})$ for each
formula from the set $\Phi_{\Gamma,\alpha}$. This concludes the proof. ∎

######  Remark 4.8 (Belief below plausibility).

When dealing with $\mathsf{DS}_{\mathtt{pl}}$ models in the context of
Subsection 3.3.3 where $\mathtt{bel}(X)\leq\mathtt{pl}(X)$ for any
$X\subseteq\mathcal{P}(S)$, we simply extend the logic
$\mathsf{Bel}^{\mathsf{N}{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}}$
with additional axioms

$\mathsf{B}\varphi\rightarrowtriangle\mathsf{Pl}\varphi.$

Note that $\mathsf{B}\varphi\rightarrowtriangle\mathsf{Pl}\varphi$ proves
$\neg\mathsf{Pl}\varphi\rightarrowtriangle\neg\mathsf{B}\varphi$ because of
the $\mathsf{B}\neg$-axiom. The additional axioms are sound, whenever we
ensure that $\mathtt{bel}(|\varphi|^{+})\leq\mathtt{pl}(|\varphi|^{+})$ in the
underlying $\mathsf{DS}_{\mathtt{pl}}$ models.

We conclude this whole subsection with some general remarks concerning the
two-layered Łukasiewicz-based logics presented above.

######  Remark 4.9 (Adding $\bot$ and $\top$ to the inner logic).

Adding the constants $\bot$ and $\top$ to $\mathsf{BD}$ results in the logic
$\mathsf{BD}^{*}$ (see Subsection 2.2 for its axiomatisation). Using
$\mathsf{BD}^{*}$ as the inner logic, however, affects how the modal part of
the logic is to be completely axiomatised because we now have formulas whose
measure is always $0$ (or $1$ respectively). This is simply achieved by
extending the modal part with the modal axiom $\mathsf{Pr}\top$ (respectively,
$\mathsf{B}\top$ $\mathsf{Pl}\top$). One can think of it as a way to avoid a
necessitation modal rule, which would only make sense to add if we allowed
inner formulas as assumptions in the consequence relation of the two-layered
logics (see Remark 4.11).

######  Remark 4.10.

As one can see from Remark 4.9, $\mathsf{Pr}$, $\mathsf{B}$, and $\mathsf{Pl}$
are not _normal_ modalities (unless the inner logic includes constants) in the
sense that no formula of the form $\mathsf{M}\phi$ with
$\phi\in\mathscr{L}_{\mathsf{BD}}$ and
$\mathsf{M}\in\\{\mathsf{Pr},\mathsf{B},\mathsf{Pl}\\}$ is valid. Note,
however, that all three modalities are _regular_ : if $\phi\vdash\chi$ is
$\mathsf{BD}$\- or $\mathsf{BD}^{*}$-valid, then
$\mathsf{M}\phi\rightsquigarrow\mathsf{M}\chi$ is valid as well for
$\rightsquigarrow\in\\{\rightarrow,\rightarrowtriangle,\Rightarrow\\}$.

######  Remark 4.11 (Allowing inner assumptions).

If we wish to allow inner formulas as assumptions in the consequence relation
of the two-layered logics (in line with the abstract approach of [12, 3]), we
would consider a mixed-consequence relation of the form

$\Phi,\Gamma\vdash\alpha,$

where $\Phi$ is a finite set of inner formulas, and $\Gamma,\alpha$ is a
finite set of outer formulas. The semantics is now given as follows: for each
model $\mathscr{M}=(S,v^{+},v^{-},f)$ validating $\Phi$ (in the sense of
$\mathsf{BD}$ semantics), if the $f$-derived valuation $v^{\mathscr{M}}$
validates $\Gamma$ in the outer algebra, it also validates $\alpha$. For the
axiomatisation, we need to update it with the following (obviously sound)
_modal rules_ , i.e. rules whose assumptions are inner formulas and whose
conclusion is an outer formula (replacing now redundant monotonicity modal
axioms):

$\displaystyle\varphi$ $\displaystyle\lhd\mathsf{B}\varphi$
$\displaystyle\\{\Phi$
$\displaystyle\lhd\mathsf{B}\varphi\rightarrow\mathsf{B}\psi\mid\Phi,\varphi\vdash_{\mathsf{BD}}\psi\\}$

and similarly for the other modalities. The notion of a two-layered proof
needs to be adapted as well in an expected manner: upper parts of a proof tree
may consist of a $\mathsf{BD}$ proof followed by an application of a modal
rule. The completeness proof becomes more subtle now as well: basically, to
refute $\Phi,\Gamma\vdash\alpha$, we need to construct an appropriate measure
on the canonical $\mathsf{BD}$ model for the finite set $\mathsf{Lit}$ of
literals from $\Phi,\Gamma\vdash\alpha$, relativized to $\Phi$ (i.e.,
$(\mathcal{P}(\mathsf{Lit}),v^{+}_{c},v^{-}_{c})$, relativized to the set
$|\bigwedge\Phi|^{+}$). This takes into account that we need to measure
$\mathsf{BD}$ formulas up to equi-provability from $\Phi$131313It is worth
mentioning that the relation $\varphi\equiv_{\Phi}\psi$ given as
$\Phi,\varphi\vdash_{\mathsf{BD}}\psi$ and
$\Phi,\psi\vdash_{\mathsf{BD}}\varphi$ is in general not a congruence w.r.t.
$\neg$. The logic $\mathsf{BD}$ is only weakly Fregean..

###  4.5 Translations

Here, we follow [3] and provide a translation of the two-layered logics with
inequalities given in section 4.1 into
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$
and
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$
and back. In fact, the original translations work just fine.

####  4.5.1 Translations to
$\mathsf{Pr}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$

######  Definition 4.35 (Functional counterparts).

Let $l_{1}$, …, $l_{n}$ be literals, and $\alpha(l_{1},\ldots,l_{n})$ be an
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}_{\triangle^{\top}}$
formula in NNF. A  _functional counterpart_ of $\alpha$ (denoted $f_{\alpha}$)
is a function $f_{\alpha}:\mathbb{R}^{n}\rightarrow\mathbb{R}$ s.t. for any
$v$,

$\displaystyle v_{1}(\alpha)$
$\displaystyle=f_{\alpha}(v_{1}(l_{1}),\ldots,v_{1}(l_{n}))$ $\displaystyle
v_{2}(\alpha)$ $\displaystyle=f_{\alpha}(v_{2}(l_{1}),\ldots,v_{2}(l_{n}))$

######  Definition 4.36 (From weight formulas to Łukasiewicz two-layer
formulas).

Let

$\underbrace{\sum\limits_{i=1}^{n}a_{i}\cdot\mathtt{w}^{+}(\phi_{i})}_{t}\geqslant
c$

be a PWF that does not contain $\mathtt{w}^{-}$. Let, further, for any
$f:\mathbb{R}^{n}\rightarrow\mathbb{R}$, $f^{\sharp}=\min(1,\max(f,0))$.

Now, for

$f(x_{1},\ldots,x_{n})=\sum\limits_{i=1}^{n}a_{i}\cdot\mathtt{w}^{\pm}(\phi_{i})-c+1$

let $\beta(p_{1},\ldots,p_{n})$ be an Ł-formula s.t. $f_{\beta}=f^{\sharp}$.
Thus, we can define the ∙-translation as follows141414Recall that we
manipulate with weight formulas classically..

$\displaystyle(t\geqslant c)^{\bullet}$
$\displaystyle={\triangle^{\top}}\beta(\mathsf{Pr}\phi_{1},\ldots,\mathsf{Pr}\phi_{n})$
$\displaystyle\bot^{\bullet}$ $\displaystyle=\bot$
$\displaystyle\alpha\supset\alpha^{\prime}$
$\displaystyle=\alpha^{\bullet}\rightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\alpha^{\prime\bullet}$

######  Remark 4.12.

Observe that we can actually avoid using $\neg$ if we use $\sim$ or $\bot$ as
a primitive
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$-connective.
This will give us an embedding into $\mathsf{Pr_{lin}}$ from [3]. Note,
furthermore, that because of ${\triangle^{\top}}$, all translated formulas
have either value $(1,0)$, or $(0,1)$. Again, we do not actually use two-
dimensionality. Furthermore, it is evident that all
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}_{(x,y)}$
entailments are the same and that $\neg$ and $\sim$ are identical if all
atomic propositions are prenexed by ${\triangle^{\top}}$.

######  Proposition 4.37.

Let $\Xi\cup\\{\alpha\\}$ be a set of weight formulas. Then,
$\Xi\vDash_{\mathtt{m}\mathsf{BD}}\alpha$ iff
$\Xi^{\bullet}\vDash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\alpha^{\bullet}$.

We define our translation on NNFs of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
formulas. Note also that
$\neg{\triangle^{\top}}\phi\leftrightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}{\sim}{\triangle^{\top}}\phi$.
Thus, we can ignore the Belnap–Dunn negation.

######  Definition 4.38 (From Łukasiewicz two-layer formulas to weight
formulas).

Let $\alpha$ be an NNF of an
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
probabilistic formula and let $\alpha^{-}$ be the result of replacing each
$\mathsf{Pr}\phi_{i}$ with a $p_{i}$. Since $f_{\alpha^{-}}=\max\limits_{k\in
K}\min\limits_{j\in J_{k}}t_{k,j}$ for some $K$ and $J$ where for every $k\in
K$ and $j_{k}\in J$ there is a linear function $f_{k,j}$ with integer
coefficients and

$t_{k,j}=f^{\sharp}_{k,j}\text{ or
}t_{k,j}=1-{\triangle^{\top}}(1-f^{\sharp}_{f,j})$

it is possible to define the ∘-translation of $\alpha$ as follows.

$\alpha^{\circ}=\bigvee\limits_{k\in K}\bigwedge\limits_{j\in
J_{k}}\alpha_{k,j}$

Here for $f_{k,j}=\sum\limits_{i=1}^{n}a_{i}\cdot x_{i}+c$, we have

$\displaystyle\alpha_{k,j}$
$\displaystyle=\begin{cases}\sum\limits_{i=1}^{n}a_{i}\cdot\mathtt{w}^{+}(\phi_{i})\geqslant
1-c&\text{ if }t_{k,j}=f^{\sharp}_{k,j}\\\
\sum\limits_{i=1}^{n}a_{i}\cdot\mathtt{w}^{+}(\phi_{i})<-c&\text{
otherwise}\end{cases}$

######  Proposition 4.39.

Let $\Xi\cup\\{\alpha\\}$ be a set of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
two-layer formulas. Then,
$\Xi\\!\vDash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\\!\alpha$
iff $\Xi^{\circ}\\!\vDash_{\mathtt{m}\mathsf{BD}}\\!\alpha^{\circ}$.

####  4.5.2 Translations to
$\mathsf{Bel}^{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}_{\triangle}$

######  Definition 4.40 (Language and semantics of
$\langle\mathsf{BD},B,{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}_{(1,0)}(\rightarrow,\triangle)\rangle$
for beliefs).

The language is as follows. Let $\phi\in\mathscr{L}_{\mathsf{BD}}$. The set of
(upper-layer) formulas is defined via the following grammar.

$\alpha\coloneqq\mathtt{Bel}\phi\mid\neg\alpha\mid\alpha\rightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\alpha\mid{\triangle^{\top}}\alpha$

$\bot$ is defined as
$\neg(\beta\rightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\beta)$.
All other connectives — $\sim$, $\wedge$, $\vee$, $\odot$, and $\oplus$ — can
be defined as usual.

The semantics is given over De Morgan algebras with belief functions:
$v_{1}(\mathtt{Bel}\phi)=\mathtt{bel}(v(\phi))$;
$v_{2}(\mathtt{Bel}\phi)=\mathtt{bel}(v(\neg\phi))$. The connectives are
defined in the expected fashion.

######  Definition 4.41 (From belief formulas to Łukasiewicz modal formulas).

Let

$\underbrace{\sum\limits_{i=1}^{n}a_{i}\cdot\mathtt{b}^{+}(\phi_{i})}_{t}\geqslant
c$

be a PBF that does not contain $\mathtt{b}^{-}$. Let, further, for any
$f:\mathbb{R}^{n}\rightarrow\mathbb{R}$, $f^{\sharp}=\min(1,\max(f,0))$.

Now, for

$f(x_{1},\ldots,x_{n})=\sum\limits_{i=1}^{n}a_{i}\cdot\mathtt{w}^{\pm}(\phi_{i})-c+1$

let $\beta(p_{1},\ldots,p_{n})$ be an Ł-formula s.t. $f_{\beta}=f^{\sharp}$
(recall definition 4.35). Thus, we can define the ∙-translation as
follows151515Recall that we manipulate with weight formulas classically..

$\displaystyle(t\geqslant c)^{\bullet}$
$\displaystyle={\triangle^{\top}}\beta(\mathsf{B}\phi_{1},\ldots,\mathsf{B}\phi_{n})$
$\displaystyle\bot^{\bullet}$ $\displaystyle=\bot$
$\displaystyle\alpha\supset\alpha^{\prime}$
$\displaystyle=\alpha^{\bullet}\rightarrow_{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}\alpha^{\prime\bullet}$

######  Proposition 4.42.

Let $\Xi\cup\\{\alpha\\}$ be a set of belief formulas. Then,
$\Xi\vDash_{\mathtt{b}\mathsf{BD}}\alpha$ iff
$\Xi^{\bullet}\vDash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\alpha^{\bullet}$.

######  Definition 4.43 (From Łukasiewicz two-layer formulas to belief
formulas).

Let $\alpha$ be an NNF of an
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
two-layer formula and let $\alpha^{-}$ be the result of replacing each
$\mathtt{Bel}\phi_{i}$ with a $p_{i}$. Since $f_{\alpha^{-}}=\max\limits_{k\in
K}\min\limits_{j\in J_{k}}t_{k,j}$ for some $K$ and $J$ where for every $k\in
K$ and $j_{k}\in J$ there is a linear function $f_{k,j}$ with integer
coefficients and

$t_{k,j}=f^{\sharp}_{k,j}\text{ or
}t_{k,j}=1-{\triangle^{\top}}(1-f^{\sharp}_{f,j})$

it is possible to define the ∘-translation of $\alpha$ as follows

$\alpha^{\circ}=\bigvee\limits_{k\in K}\bigwedge\limits_{j\in
J_{k}}\alpha_{k,j}$

Here for $f_{k,j}=\sum\limits_{i=1}^{n}a_{i}\cdot x_{i}+c$, we have

$\displaystyle\alpha_{k,j}$
$\displaystyle=\begin{cases}\sum\limits_{i=1}^{n}a_{i}\cdot\mathtt{b}^{+}(\phi_{i})\geqslant
1-c&\text{ if }t_{k,j}=f^{\sharp}_{k,j}\\\
\sum\limits_{i=1}^{n}a_{i}\cdot\mathtt{b}^{+}(\phi_{i})<-c&\text{
otherwise}\end{cases}$

######  Proposition 4.44.

Let $\Xi\cup\\{\alpha\\}$ be a set of
${\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}$
two-layer formulas. Then,
$\Xi\\!\vDash_{{\mathchoice{\mbox{\rm\L}}{\mbox{\rm\L}}{\mbox{\rm\scriptsize\L}}{\mbox{\rm\tiny\L}}}^{2}}\\!\alpha$
iff $\Xi^{\circ}\\!\vDash_{\mathtt{b}\mathsf{BD}}\\!\alpha^{\circ}$.

##  5 Conclusion

Let us recapitulate the main results of our paper. We developed the axiomatics
of non-standard belief and plausibility functions (Section 3) and proved their
completeness (Theorems 3.12 and 3.13). We then proposed two different kinds of
formalising reasoning with non-standard probabilities and belief functions
(Section 4). In both cases, we show how to reason with inconsistent and
incomplete information in a non-trivial manner. We established completeness of
these logics: Theorems 4.24 and 4.29 give completeness of two-layered logics
while Theorems 4.3 and 4.8 provide completeness of calculi of inequalities _à
la_ Fagin, Halpern, and Megiddo [23]. Finally, we defined faithful
translations in the manner of [3] between these two frameworks in Propositions
4.37, 4.39, 4.42, and 4.44.

Still, several important questions remain unanswered. First, in the case of
classical probability theory, belief and plausibility functions are not the
only uncertainty measures more general than probabilities proper. In
particular, probabilities can be generalised by lower and upper probabilities
(cf., e.g. [32, §2.3] for more details). It would be instructive to define
their $\mathsf{BD}$ counterparts and investigate their properties. Second,
Bayes’ and Jeffrey’s conditionings of non-standard probabilities are given in
[33]. It is reasonable to construct conditioning of non-standard belief and
plausibility functions. Furthermore, to the best of our knowledge, there is no
work done on the conditioning of non-standard probabilities on arbitrary
lattices.

On the logic side, we plan to investigate the proof theory of our two-layered
logics. We are particularly interested in providing structural proof theory in
the form of display or sequent calculi and in expanding on the tableaux
framework presented in [8]. The tableaux will also allow us to establish the
decidability and complexity bounds of our two-layered logics.

## References

  * [1] A.R. Anderson and N.D. Belnap.  Tautological entailments.  Philosophical Studies, 13(1):9–24, Jan 1962.
  * [2] A.R. Anderson, N.D. Belnap, and J.M. Dunn.  A useful four-valued logic: How a computer should think.  In Entailment II, The Logic of Relevance and Necessity, pages 506–541. Princeton Legacy Library, 1992.
  * [3] P. Baldi, P. Cintula, and C. Noguera.  Classical and fuzzy two-layered modal logics for uncertainty: Translations and proof-theory.  International Journal of Computational Intelligence Systems, 13(1):988–1001, 2020.
  * [4] J.-P. Barthélemy.  Monotone functions on finite lattices: An ordinal approach to capacities, belief and necessity functions.  In Preferences and Decisions under Incomplete Knowledge, Studies in fuzziness and soft computing, pages 195–208. Physica-Verlag HD, Heidelberg, 2000.
  * [5] N.D. Belnap.  How a computer should think.  In H. Omori and H. Wansing, editors, New Essays on Belnap-Dunn Logic, volume 418 of Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science). Springer, Cham, 2019.
  * [6] P. Besnard and J. Lang.  Possibility and necessity functions over non-classical logics.  In Uncertainty Proceedings 1994, pages 69–76. Elsevier, 1994.
  * [7] M. Bílková, S. Frittella, O. Majer, and S. Nazari.  Belief based on inconsistent information.  In International Workshop on Dynamic Logic, pages 68–86. Springer, 2020.
  * [8] Marta Bílková, Sabine Frittella, and Daniil Kozhemiachenko.  Constraint tableaux for two-dimensional fuzzy logics.  In Lecture Notes in Computer Science, Lecture notes in computer science, pages 20–37. Springer International Publishing, Cham, 2021.
  * [9] J. Bueno-Soler and W. Carnielli.  Paraconsistent probabilities: Consistency, contradictions and Bayes’ theorem.  Entropy (Basel), 18(9):325, September 2016.
  * [10] L. Běhounek, P. Cintula, and P. Hájek.  Introduction to Mathematical Fuzzy Logic.  In P. Cintula, P. Hájek, and C. Noguera, editors, Handbook of Mathematical Fuzzy Logic, volume 37 of Studies in logic, pages 1–102. College Publications, 2011.
  * [11] P. Cintula, P. Hájek, and C. Noguera.  Handbook of Mathematical Fuzzy Logic 1.  Studies in Logic 37. College Publications, 2011.
  * [12] P. Cintula and C. Noguera.  Modal Logics of Uncertainty with Two-Layer Syntax: A General Completeness Theorem.  In Proceedings of WoLLIC 2014, pages 124–136, 2014.
  * [13] N.C.A. da Costa.  On the theory of inconsistent formal systems.  Notre Dame Journal of Formal Logic, 15(4):497–510, 1974.
  * [14] Š. Dautović, D. Doder, and Z. Ognjanović.  An epistemic probabilistic logic with conditional probabilities.  In Logics in Artificial Intelligence. JELIA 2021, volume 12678 of Lecture notes in computer science, pages 279–293. Springer International Publishing, Cham, 2021.
  * [15] A.P. Dempster.  Upper and lower probabilities induced by a multivalued mapping.  The Annals of Mathematical Statistics, 38(2):325–339, April 1967\.
  * [16] A.P. Dempster.  A generalization of bayesian inference.  Journal of the Royal Statistical Society: Series B (Methodological), 30(2):205–232, 1968.
  * [17] D. Dubois.  On ignorance and contradiction considered as truth-values.  Logic Journal of the IGPL, 16(2):195–216, 2008.
  * [18] D. Dubois, J. Lang, and H. Prade.  Possibilistic logic.  In Nonmonotonic reasoning and uncertain reasoning, volume 3 of Handbook of logic in artificial intelligence and logic programming, pages 279–293. Oxford University Press, 1994.
  * [19] D. Dubois and H. Prade.  Combination and Propagation of Uncertainty with Belief Functions – A Reexamination.  In A.K. Joshi, editor, Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, CA, USA, August 1985, pages 111–113. Morgan Kaufmann, 1985.
  * [20] D. Dubois and H. Prade.  Representation and combination of uncertainty with belief functions and possibility measures.  Computational Intelligence, 4(3):244–264, September 1988.
  * [21] J.M. Dunn.  Intuitive semantics for first-degree entailments and ‘coupled trees’.  Philosophical Studies, 29(3):149–168, 1976.
  * [22] J.M. Dunn.  Contradictory information: Too much of a good thing.  Journal of Philosophical Logic, 39:425––452, 2010.
  * [23] R. Fagin, J. Y. Halpern, and N. Megiddo.  A logic for reasoning about probabilities.  Information and Computation, 87:78–128, 1990.
  * [24] M. Fitting.  Kleene’s three-valued logics and their children.  Fundamenta informaticae, 20(1, 2, 3):113–131, 1994.
  * [25] J.M. Font.  Belnap’s Four-Valued Logic and De Morgan Lattices.  Logic Journal of the IGPL, 5(3):1–29, 1997.
  * [26] S. Frittella, K. Manoorkar, A. Palmigiano, A. Tzimoulis, and N. Wijnberg.  Toward a Dempster-Shafer theory of concepts.  International Journal of Approximate Reasoning, 125:14–25, 2020\.
  * [27] M. Grabisch.  Belief functions on lattices.  International Journal of Intelligent Systems, 24(1):76–95, January 2009.
  * [28] P. Hájek.  Metamathematics of Fuzzy Logic, volume 4 of Trends in Logic.  Kluwer, 1998.
  * [29] P. Hájek, L. Godo, and F. Esteva.  Fuzzy logic and probability.  In P. Besnard and S. Hanks, editors, IJAI’95: Proceedings of the Eleventh Annual Conference on Uncertainty in Artificial Intelligence, Montreal, Quebec, Canada, August 18–20, 1995, pages 237–244. Morgan Kaufmann, 1995.
  * [30] P. Hájek and S. Tulipani.  Complexity of fuzzy probability logics.  Fundamenta Informaticae, 45(3):207–213, 2001.
  * [31] P. Halmos.  Measure Theory.  Van Nostrand Reinhold Co., New York, NY., 1950.
  * [32] J.Y. Halpern.  Reasoning about uncertainty.  The MIT Press, 2nd edition, 2017.
  * [33] D. Klein, O. Majer, and S. Rafiee Rad.  Probabilities with gaps and gluts.  Journal of Philosophical Logic, 50(5):1107–1141, October 2021.
  * [34] E.D. Mares.  Paraconsistent probability theory and paraconsistent bayesianism.  Logique et analyse, pages 375–384, 1997.
  * [35] D. Nelson.  Constructible falsity.  The Journal of Symbolic Logic, 14(1):16–26, 1949.
  * [36] S.P. Odintsov.  Constructive negations and paraconsistency, volume 26 of Trends in logic.  Springer, 2008.
  * [37] H. Omori and K. Sano.  Generalizing Functional Completeness in Belnap-Dunn Logic.  Studia Logica, 103(5):883–917, Oct 2015.
  * [38] H. Omori and H. Wansing.  40 years of FDE: An introductory overview.  Studia Logica, 105(6):1021–1049, 2017.
  * [39] A. Pietz and U. Rivieccio.  Nothing but the truth.  Journal of Philosophical Logic, 42(1):125–135, 2013.
  * [40] A. Přenosil.  Reasoning with Inconsistent Information.  PhD thesis, Charles University, Prague, 2018.
  * [41] G. Shafer.  A mathematical theory of evidence.  Princeton university press, 1976.
  * [42] P. Smets.  Belief functions.  In P. Smets, Mamdani A., D. Dubois, and H. Prade, editors, Non-Standard Logics for Automated Reasoning, pages 253–286. Academic Press, 1988\.
  * [43] P. Smets.  The nature of the unnormalized beliefs encountered in the transferable belief model.  In D. Dubois and M.P. Wellman, editors, UAI ’92: Proceedings of the Eighth Annual Conference on Uncertainty in Artificial Intelligence, Stanford University, Stanford, CA, USA, July 17-19, 1992, pages 292–297. Morgan Kaufmann, 1992.
  * [44] R.P. Stanley.  Enumerative Combinatorics, volume 1 of Cambridge Studies in Advanced Mathematics.  Cambridge University Press, 2 edition, 2011.
  * [45] D. Vakarelov.  Notes on N-lattices and constructive logic with strong negation.  Studia Logica, 36(1–2):109–125, 1977.
  * [46] H. Wansing.  Constructive negation, implication, and co-implication.  Journal of Applied Non-Classical Logics, 18(2–3):341–364, 2008\.
  * [47] R.R. Yager.  On the Dempster-Shafer framework and new combination rules.  Information sciences, 41(2):93–137, 1987.
  * [48] L.A. Zadeh.  Fuzzy sets as a basis for a theory of possibility.  Fuzzy Sets And Systems, 1(1):3–28, January 1978.
  * [49] C. Zhou.  Belief functions on distributive lattices.  Artificial Intelligence, 201:1–31, 2013.

##  Appendix A Proofs of Section 2.3

The following Lemma is used to prove Theorem 2.9

######  Lemma A.1.

_[49, Lemma 2.6]_ Let $\mu:{\mathcal{P}}(X)\to\mathbb{R}$ be a function such
that: $\mu(\varnothing)=0$ and $\mu(A\cup B)=\mu(A)+\mu(B)-\mu(A\cap B)$ for
every $A,B\in\mathcal{P}(X)$. Then, we have:

$\mu\left(\bigcup\limits_{i=1}^{n}R_{i}\right)=\sum\limits_{J\subseteq\\{1,\ldots,n\\},J\neq\varnothing}(-1)^{|J|+1}\mu\left(\bigcap\limits_{j\in
J}R_{i}\right).$ (30)

##### Theorem 2.9

Let $\mathcal{L}$ be a finite lattice and
$\mathtt{bel}:{\cal{L}}\rightarrow[0,1]$ be a monotone function. Let further,
$\mathtt{m}_{\mathtt{bel}}:{\cal{L}}\rightarrow[0,1]$ be the Möbius transform
of $\mathtt{bel}$. Then, $\mathtt{bel}$ is a general belief function iff
$\mathtt{m}_{\mathtt{bel}}$ is a general mass function.