Mathematical fuzzy logic; Logics of uncertainty; Łukasiewicz logic; Probability logics; Two-layered modal logics; Hypersequent calculi
Abstract
This paper is a contribution to the study of two distinct kinds of logics for modelling uncertainty. Both approaches use logics with a two-layered modal syntax, but while one employs classical logic on both levels and infinitely-many multimodal operators, the other involves a suitable system of fuzzy logic in the upper layer and only one monadic modality. We take two prominent examples of the former approach, the probability logics Prlin and Prpol (whose modal operators correspond to all possible linear/polynomial inequalities with integer coefficients), and three logics of the latter approach: PrŁ, PrŁ△ and PrPŁ△ (given by the Łukasiewicz logic and its expansions by the Baaz–Monteiro projection connective △ and also by the product conjunction). We describe the relation between the two approaches by giving faithful translations of Prlin and Prpol into, respectively, PrŁ△ and PrPŁ△, and vice versa. We also contribute to the proof theory of two-layered modal logics of uncertainty by introducing a hypersequent calculus HPrŁ for the logic PrŁ. Using this formalism, we obtain a translation of Prlin into the logic PrŁ, seen as a logic on hypersequents of relations, and give an alternative proof of the axiomatization of Prlin.
Numerous logical systems have been proposed, and intensively studied in recent years, to cope with reasoning about uncertain events. Among them, two of the most prominent examples are the systems introduced by Fagin, Halpern, and Megiddo [2] (see also Halpern's monograph [3]), which we denote here as Prlin and Prpol. These systems employ a rather sophisticated two-layered modal syntax: They start, in a first layer, by expressing classical events (i.e., propositions that can only be true or false) by means of the syntax of propositional classical logic; then, they define the atomic statements of the second syntactical layer as linear inequalities (in the case of Prlin), or polynomial inequalities (in the case of Prpol), of probabilities of these classical events. Each of these inequalities can be seen as the application of a multimodal operator on classical formulas. Finally, such atomic statements may be combined using classical connectives again.
The consequence relation of both logics Prlin and Prpol is then introduced semantically by means of Kripke frames enriched by a probability measure, which allows for expressing the validity of statements of these logics: in the atomic case, as the truth of inequalities involving the probability of events, i.e., of sets of worlds described by classical formulas, and, in the case of complex formulas, by using the usual semantics of classical logic.
Despite dealing with the intrinsically graded notion of probability, the semantics of these logics remains essentially bivalent. An alternative approach to reasoning about uncertain events uses the framework of mathematical fuzzy logic and takes sentences like “φ is probable” at face value, i.e., identifying its truth degree with the probability of φ. Then, one combines such formulas using connectives of a suitable fuzzy logic. Hence, this approach also uses a two-layered modal syntax which is, however, radically simplified. Indeed, it employs only one monadic modality (for “is probable”), instead of infinitely-many polyadic modalities, as it shifts the syntactical complexity of the atomic statements to the many-valued semantics of the fuzzy logic in question.
The original rendering of this approach [4,5] used Łukasiewicz logic Ł to govern modal formulas. The resulting logic, which we denote here as PrŁ, was given by using Kripke frames enriched by a probability measures, analogously to Prlin and Prpol. Later, several authors studied numerous similar logical systems by altering not only the upper logic but also the lower one (to speak about probability of fuzzy events) and even their interlinking modalities (to speak about other measures of uncertainty such as necessity, possibility, or belief functions).1
In this paper we will focus only on the logic PrŁ and two of its expansions, PrŁ△ and PrPŁ△, which use stronger fuzzy logics to govern the behavior of modal formulas in the upper syntactical layer, namely the logic Ł△ expanding Ł with the Baaz–Monteiro projection operator △, and its further expansion PŁ△ with the product conjunction.2
A natural question presents itself: what is the relation between the two approaches? More precisely: can Prlin and Prpol be translated into two-layered modal fuzzy logics and, hence, be casted into a syntactically simpler framework without losing expressivity? This paper intends to give a positive answer to this question while providing inverse translations as well, thus showing that both approaches are indeed much more closely related than it might have seemed at first sight.
The answer is, nonetheless, not as straightforward as one could expect: We present translations of Prlin and Prpol into, respectively the logics PrŁ△ and PrPŁ△, and vice versa. The need for the product conjunction of PrPŁ△ in the second case is hardly a surprise, since we need to take care of products in the polynomial inequalities of Prpol. However, the presence of the projection connective △ in both cases may appear as an unexpected nuisance.
The effort toward amending this eyesore led to the second main contribution of the paper: We show that the logic PrŁ can be axiomatized using a particular Gentzen-style calculus, denoted as HPrŁ, which is an extension of a known calculus for Łukasiewicz logic. Unlike classical Gentzen calculi, which work with sequents, in our case we have to consider more complex syntactical structures, known as hypersequents of relations. Interestingly enough, these structures yield a rich framework that allows us to circumvent the use of the projection connective △ and present the desired translation of Prlin into the logic PrŁ, seen as a logic on hypersequents of relations. Although the calculus HPrŁ is not analytic, its existence enhances the applicability of the logic PrŁ and deepens our theoretic understanding of this logic; e.g., we can use it to obtain an alternative proof of the axiomatization of Prlin, which is arguably simpler that the one known from the literature [6]. Therefore, the results of this paper strengthen the overall prominence of PrŁ among logics of uncertainty.
The paper is organized as follows: First, in Section 2, we introduce the syntax, the semantics, and axiomatizations for the logics under investigation, in a reasonably self-contained yet streamlined manner. Then, in Section 3, we present the mentioned translations of Prlin and Prpol into, respectively the logics PrŁ△ and PrPŁ△, and vice versa. In Section 4 we introduce a hypersequent calculus HPrŁ and prove that it axiomatizes the logic PrŁ. In Section 5 we provide a faithful translation of the logic Prlin into PrŁ (seen as a logic of hypersequents of relations) and give an alternative proof of the axiomatization of Prlin. Finally, in Section 6 we add some concluding remarks and hints at future research directions.
2. CLASSICAL AND FUZZY LOGICS OF UNCERTAINTY
2.1. Propositional Core
In this paper, we need the following four propositional logics: (1) classical logic CL cast in the language with the truth-constant ⊥ and implication →, (2) Łukasiewicz logic Ł in the same language, (3) Ł△, the expansion of Ł in the language with the additional unary connective △ known as Baaz–Monteiro projection, and, finally, (4) PŁ△, the expansion of Ł△ with the additional binary connective ⊙ (called product conjunction). Next, we review some of the properties of these logics needed for the paper; we refer the reader to the corresponding chapters of the Handbook of Mathematical Fuzzy Logic [9] for more details and references.
We expect the reader to be familiar with the notion of formula (over an arbitrary propositional language) and the notion of evaluation in classical logic. In the case of Ł, Ł△, and PŁ△, (standard) evaluations are functions from the corresponding set of formulas into the real unit interval [0, 1], such that e(⊥)=0 and
Let L be any of these four logics and Ψ∪{φ} a set of formulas in the language of L. We say that φ is a semantical consequence of Ψ in L, in symbols Ψ⊨Lφ, if for each evaluation e such that e(ψ)=1 for all ψ∈Ψ, we have e(φ)=1.
We also expect the reader to be familiar with the notion of derivability relation ⊢AX in a (finitary) Hilbert-style axiomatic system AX; we say that AX is an axiomatization of a logic L if for each finite set Ψ∪{φ} of formulas, we have Ψ⊨Lφ iff Ψ⊢AXφ. It is well known that there are numerous axiomatizations of classical logic (where the equivalence holds even for infinite sets of premises) and the three fuzzy logics considered here. We write ⊢L when an axiomatization of a logic L is fixed or known from the context.
Let us conclude this subsection by recalling additional definable connectives of Łukasiewicz logic together with their standard semantics:
Whenever necessary to avoid confusions, we add “Ł” as a subscript to the connectives in order to distinguish them from the classical ones.
2.2. Five Two-Layered Modal Languages
We start by recalling the language ℒlin of the logic Prlin. It is a two-layered modal language: first, in a lower layer, we have the nonmodal formulas which are simply those of classical propositional logic. Then, we have basic inequality formulas of the form
∑i=1naiP(φi)⩾c,
where φis are nonmodal formulas and c and ai are constants for integers (in other works in the literature real numbers [3] or also rationals [10] are used). In the extreme case in which n=0 or all ai's are 0, we have the basic inequality formula 0⩾c. The linear combination on the left-hand side of the inequality is called a basic inequality term. The formulas of the upper layer of ℒlin, called modal formulas, are then obtained from basic inequality formulas via the usual connectives of classical logic. Obvious abbreviations apply; in particular, we use the following:
The language ℒpol is obtained by using again the language of classical logic for the lower layer, and allowing any polynomial basic inequality terms in the upper layer, i.e., the basic inequality formulas of ℒlin have the general form
∑i=1naiP(φi,1)⋯P(φi,mi)⩾c.
Complex formulas of the upper layer are built as in ℒlin, combining basic inequality formulas by means of connectives of classical logic. Note that in ℒpol one can express fundamental probabilistic notions, e.g., independence of events using formulas of the kind
P(φ∧ψ)=P(φ)⋅P(ψ).
Let us now turn our attention to the fuzzy approach toward logics of probability. We introduce three languages, ℒPŁ, ℒPŁ△, and ℒPPŁ△, where, as before, the lower-layer formulas are those of classical logic, but instead of basic inequality formulas combined by connectives of classical logic, the modal formulas are built from simple atomic modal formulas of the form P(φ) (where φ is a classical formula) using the connectives of the logic Ł, Ł△, or PŁ△, respectively. For example, P(p→p) and P(⊥) are atomic modal formulas in any of these two-layered modal languages, P(⊥)→ŁP(p→p) is a nonatomic modal formula in any of them, △P(⊥) is a nonatomic modal formula in ℒPŁ△ and ℒPPŁ△, and △P(⊥)⊙P(p→p) is a nonatomic modal formula in ℒPPŁ△. Observe that the two-layered syntax does not admit iterative applications of the modal operator (e.g., P(P(p)→P(q)) is a not a well-formed formula) nor combinations of atomic modal formulas with nonmodal formulas in the upper level (e.g., p⊙P(q) is not a well-formed formula either).
Remark 1.
Note that a basic inequality formula ∑i=1naiP(φi)⩾c of ℒlin can be seen as an atomic modal formula obtained by applying an n-ary modality □a1,…,an,c, on n classical formulas φ1,…,φn. In this way, one can see ℒlin as an instance of an abstract two-layered modal language [7]. The same is true for ℒpol, but here the set of used modalities is even more complex. Thus, the five languages can be summarized in the following table:
Language
Lower l.
Modalities
Upper l.
ℒlin
CL
{ t⩾c:t lin}
CL
ℒpol
CL
{ t⩾c:t poly}
CL
ℒPŁ
CL
{P}
Ł
ℒPŁ△
CL
{P}
Ł△
ℒPPŁ△
CL
{P}
PŁ△
Convention 1.
Henceforth, we will adopt the following notational convention for distinguishing modal and nonmodal formulas in each of the logics we consider.
Nonmodal
Modal
Formulas
φ,ψ,…
γ,δ,…
(Multi)sets of formulas
Φ,Ψ,…
Γ,Δ,…
Note that we will use the same symbols for sets and multisets of formulas, relying on the context for resolving ambiguities.
2.3. One Semantics and Five Logics
The semantical picture for all five languages is based on Kripke models enriched by (finitely additive) probability measures. A (probabilistic) Kripke model is a triple M=〈W,〈ew〉w∈W,μ〉, where
W is a nonempty set of worlds
ews are classical propositional evaluations
μ is a finitely additive measure over a Boolean subalgebra of the powerset algebra of W such that
φM={w:ew(φ)=1}
is a measurable set for any classical formula φ
Clearly, M allows us to define the truth values of nonmodal formulas in each of its worlds. The assignment of truth values of modal formulas depends on the language in question, but in all cases we evaluate modal formulas only at the level of the whole model.
For basic inequality formulas of ℒlin we define
||∑i=1naiP(φi)⩾c||M=1iff∑i=1naiμ(φiM)⩾c.
The truth values of basic inequality formulas of ℒpol are defined analogously, and truth values of complex modal formulas in both languages are then defined using the truth-functions of classical connectives.
Recall that ℒPŁ, ℒPŁ△, and ℒPPŁ△ share the same atomic modal formulas; we define their truth values simply as
||P(φ)||M=μ(φM).
Then, clearly, we always have ||P(φ)||M∈[0,1], and so we can compute the truth values of more complex modal formulas using truth functions for connectives of the corresponding logic. For example ||P(p→p)||M=1, because p→p is a tautology of classical logic, and ||P(⊥)||M=0 because ⊥ is a contradiction. As for nonatomic examples, one can easily compute ||P(⊥)→ŁP(p→p)||M=1, ||△P(⊥)||M=||△P(⊥)⊙P(p→p)||M=0.
For each of the five languages we have introduced, we can define the corresponding logic as the consequence relation on the set of modal formulas given as preservation of the truth value 1 over all Kripke models; for instance, we define Prlin as the following consequence relation between sets of modal ℒlin-formulas and modal ℒlin-formulas as
Γ⊨Prlinδiff||δ||M=1 for each Kripke model Mwhere ||γ||M=1 for each γ∈Γ.
Analogously, we define the logics Prpol, PrŁ, PrŁ△, and PrPŁ△.
2.4. Axiomatizations
An axiomatization for Prlin proposed in the literature [2], which we will denote here as AXPrlin, consists of: (1) any axiomatization of classical logic for both modal and nonmodal formulas, (2) the following three axioms and one rule,
and (3) the axioms to manipulate linear inequalities, meant to be instantiated with any basic inequality formula ∑i=1kaiP(φi)⩾c, integers c′ and d′<c and d>0, and permutation σ:
The proof that AXPrlin is indeed an axiomatization of Prlin relies essentially on linear programming methods. The original paper [2] also shows that the satisfiability problem for Prlin is NP-complete. On the other hand, the same paper proves that the satisfiability problem for Prpol is in PSPACE, and provides an axiomatization for this logic, but only via a reduction to real closed field theory. Another axiomatization of Prpol, in the language ℒpol was found only later [11] and it includes an infinitary rule.
In contrast, the axiomatizations of PrŁ, PrŁ△, and PrPŁ△ are much simpler: [6–8] they use any axiomatization of classical logic for nonmodal formulas, any axiomatization of Ł (or Ł△ or PŁ△, respectively) for modal formulas and just three additional axioms and one rule:
As in Prlin and Prpol, the satisfiability problems for PrŁ and PrPŁ△ are also known to be NP-complete and in PSPACE, respectively [12].
3. TRANSLATING Prlin INTO PrŁ△ AND Prpol INTO PrPŁ△
In this section, we show that the classical probability logic Prlin can be faithfully translated into the two-layered modal fuzzy logic PrŁ△ and vice versa, and then we extend this result to obtain translations between the logics Prpol and PrPŁ△. Let us start by preparing two useful notational conventions.
First, for any formula φ of Ł, Ł△, or PŁ△ with (at most) n propositional variables p1,…,pn we denote by fφ the function from [0,1]n to [0,1] such that, for each evaluation e, we have
e(φ)=fφ(e(p1),…,e(pn)).
Second, for each function f:Rn→R, we define the function f#:[0,1]n→[0,1] as
f#=min{1,max{f,0}}.
Let us start by translating Prlin into PrŁ△. Let t⩾c be a basic inequality formula in ℒlin, where t stands for ∑i=1naiP(φi), and consider the linear polynomial with integer coefficients
f(x1,…,xn)=∑i=1naixi−c+1.
By the well-known McNaughton Theorem (see, e.g., its formulation in Lemma 2.1.21 of chapter IX in the Handbook of Mathematical Fuzzy Logic [13]) one can algorithmically build a formula ψ of Ł over variables p1,…,pn, such that
fψ=f#.
Let us denote by ψ(P(φ1),…,P(φn)) the formula resulting from ψ by replacing each variable pi in ψ by P(φi) and let us define
(t⩾c)∙=△ψ(P(φ1),…,P(φn)).
Clearly, (t⩾c)∙ is a formula of ℒPŁ△. We can easily extend it to a translation of all modal formulas from ℒlin by setting ⊥∙=⊥Ł and (γ→δ)∙=γ∙→Łδ∙. Let us denote as Γ∙ the set resulting from applying the translation to each formula in Γ.
Theorem 1.
LetΓ∪{δ}be a set of modal formulas ofℒlin. Then, Γ⊨PrlinδiffΓ∙⊨PrŁ△δ∙.
Proof.
It is easy to see that all we need to prove is that, for each Kripke model M and each modal formula γ of ℒlin, we have ||γ||M=1 iff ||γ∙||M=1.
We prove the claim by induction over the complexity of γ. Assume that γ is a basic inequality formula ∑i=1naiP(φi)⩾c. Then, we can write the following sequence of equivalences: ||γ||M=1 iff ∑i=1naiμ(φiM)⩾c iff ∑i=1nai||P(φi)||M⩾c iff max{0,min{1,∑i=1nai||P(φi)||M−c+1}}=1 iff f#(P(φ1),…,P(φn))=1 iff fψ(P(φ1),…,P(φn))=1 iff ||γ∙||M=1.
To prove the induction step, we only need to note that (1) for a basic inequality formula γ we have that (thanks to the semantics of △) ||γ∙||M<1 implies ||γ∙||M=0 and (2) the Łukasiewicz implication behaves on values 0 and 1 as the classical one.
Now we will show a translation in the converse direction, from PrŁ into Prlin. Consider any modal formula γ of PrŁ△ and the formula γ^ in the language of Ł△ resulting from γ by replacing each atomic modal formula P(φi) by a propositional variable pi. It is well known [13] that
fγ̂=maxk∈Kminj∈Jktk,j
where for each k∈K and j∈Jk, there is a linear function fk,j with integer coefficients and
As in the previous translation, for any set of modal formulas Γ of PrŁ△, we also let Γ∘={γ∘|γ∈Γ}.
Theorem 2.
LetΓ∪{δ}be a set of modal formulas ofℒPŁ△. Then, Γ⊨PrŁ△δiffΓ∘⊨Prlinδ∘.
Proof.
First note that, for each linear function f=∑i=1naixi+c with integer coefficients and each Kripke model M, we have
M satisfies ∑i=1naiP(φi)⩾1−c iff
f#(||P(φ1)||M,…||P(φn)||M)=1.
M satisfies ∑i=1naiP(φi)<−c iff
1−△(1−f#(||P(φ1)||M,…||P(φn)||M))=1.
Therefore, for each Kripke Model M and each formula γ of PrŁ, we have the following chain of equivalent statements which is clearly all we need to prove the theorem:
||γ||M=1
fγ̂(||P(φ1)||M,…||P(φn)||M)=1
There is k∈K such that, for each j∈Jk, we have tk,j(||P(φ1)||M,…,||P(φn)||M)=1
There is k∈K such that, for each j∈Jk, we have that γk,j is satisfied in M
The formula γ∘ is satisfied in M
Now we extend the translation to Prpol and PrPŁ△ and show that the classical probability logic Prpol can be faithfully translated into the two-layered modal fuzzy logic PrPŁ△ and so, thanks to the known simple and finitary axiomatization of PrPŁ△, this translation provides us with an alternative indirect but simple and finitary axiomatization of Prpol.
Let t⩾c be a basic inequality formula in ℒpol of the form
∑i=1naiP(φi,1)⋯P(φi,mi)⩾c
As before, we consider the linear polynomial
f(x1,…,xn)=∑i=1naixi−c+1,
and the corresponding formula ψf of Ł over propositional variables p1,…,pn, such that
e(ψf)=max{0,min{1,f(e(p1),…,e(pn))}}.
Let us denote as (t⩾c)∙ the formula resulting from △ψf by replacing each propositional variable pi in ψf by P(φi,1)⊙P(φi,2)⊙⋯⊙P(φi,mi). Clearly, (t⩾c)∙ is a formula of ℒPrPŁ△. We can easily extend it to a translation of all modal formulas from ℒpol by setting ⊥∙=⊥Ł and (γ→δ)∙=γ∙→Łδ∙. Let us denote as Γ∙ the set resulting from applying the translation to each formula in Γ.
Theorem 3.
LetΓ∪{δ}be a set of formulas ofℒpol. Then, Γ⊨PrpolδiffΓ∙⊨PrPŁ△δ∙.
Proof.
Again, it is enough to show that, for each Kripke model M and each modal formula γ of ℒpol, we have ||γ||M=1 iff ||γ∙||M=1, which is proved in the same way as in Theorem 1.
To provide the inverse translation from PrPŁ△ into Prpol, we proceed analogously to the case of PrŁ△ into Prlin: we know [13] that for formulas γ^ of PŁ△ we have an analogous description of fγ̂: the only difference is that the functions fk,j can now be polynomial with integer coefficients. Thus we have to change the definition of γk,j accordingly; in particular for fk,j=∑i=1naixi,1…xi,mi+c, we set γk,j=
Having these new definitions, we can observe that the proof of Theorem 2 also gives the fatihfulness of the final translation of this section:
Theorem 4.
LetΓ∪{δ}be a set of modal formulas ofℒPPŁ△. Then, Γ⊨PrŁ△δiffΓ∘⊨Prpolδ∘.
4. PROOF THEORY FOR PrŁ
This section is devoted to the proof theory of the two-layered modal fuzzy logic PrŁ, seen as a logic on hypersequents instead of simple formulas. In the first subsection, we will extend the known [14,15] hypersequent calculus of relations HŁ for Łukasiewicz logic to a system HŁres and show that it axiomatizes Łukasiewicz logic in a stronger sense. In the second subsection, we will introduce another hypersequent calculus of relations, HPrŁ, and (using a translation into the calculus HŁres) show that it is an axiomatization of PrŁ.
Before delving into the details of the calculi, let us recall a few basic notions concerning multisets, that will repeatedly occur in the treatment of sequents and hypersequents.
By a multiset over a set A we mean a function Γ from A to the set ℕ of natural numbers. By ℘M(A) we denote the set of all multisets over A. The root set of a multiset Γ is the set
|Γ|={a∈A|Γ(a)>0}.
If a∈|Γ|, we say that a is an element of Γ of multiplicityΓ(a). A multiset Γ is finite if |Γ| is finite. The empty multiset, i.e., the constant function 0, will be denoted by the same symbol ∅ used for the empty set—the context will always be sufficient to resolve ambiguities. Given two multisets Γ and Δ, we define their multiset union Γ⊎Δ as
(Γ⊎Δ)(a)=Γ(a)+Δ(a),for each a∈A.
As it is customary, we use square brackets for multiset abstraction; so, e.g., [a,a,b,c] will denote the multiset Γ such that Γ(a)=2, Γ(b)=Γ(c)=1, and Γ(d)=0, for any d∉{a,b,c}. We will denote as [a]n the multiset composed of n occurrences of a, and identify [a]0 with ∅.
4.1. A Strongly Complete Hypersequent Calculus of Relations for Łukasiewicz Logic
Let us start by recalling a proof-theoretic system for Łukasiewicz logic introduced by Ciabattoni, Fermüller, and Metcalfe [15], which we denote here as HŁ (see also the monograph by Gabbay, Metcalfe, and Olivetti [14]).
The basic building blocks of such calculi are sequents of relations, i.e., syntactic objects of the kind Γ◃Δ where Γ and Δ are multisets of formulas, and ◃ stands for either the symbol ⪯ or ≺.
A hypersequent of relationsG is a finite multiset of sequents of relations, denoted as
Γ1◃1Δ1|…|Γn◃nΔn
where each sequent Γi◃iΔi belonging to |G| is called a component of the hypersequent. In the following we omit the “of relations” suffix; as we do not work here with any other (hyper)sequents, there is no risk of confusion.
We also adopt the following simplifying conventions: we identify a sequent S with a hypersequent singleton [S] and, if on either side of a sequent we have a multiset union of multisets of formulas, we write simply a comma instead of ⊎ (let us stress that we do not use this convention in other contexts, e.g., in the consequence relation defined below, where we work with a set of hypersequents).
Let us define the semantics of hypersequents and the corresponding consequence relation. We extend any evaluation e of formulas of Łukasiewicz logic to multisets of formulas by setting e(∅)=0 and
e([φ1,…,φn])=∑i⩽n(e(φi)−1).
Then, we say that e satisfies a hypersquent G if there is a component Γ⪯Δ (or Γ≺Δ) of G such that e(Γ)⩽e(Δ) (resp. e(Γ)<e(Δ)). Given hypersequents G,G1,…,Gn, we denote as G1,…,Gn⊨ŁG the fact that any evaluation e which satisfies G1,…,Gn, satisfies G as well.
Note that an evaluation e satisfies a formula φ iff it satisfies the hypersequent ∅⪯φ; indeed we have 0=e(∅)⩽e([φ])=e(φ)−1 iff 1=e(φ). Therefore, the consequence relation just defined on multisets actually contains the usual consequence relation on formulas; indeed, for any set of formulas Ψ∪{φ} we have
Ψ⊨Łφiff{∅⪯ψ|ψ∈Ψ}⊨Ł∅⪯φ.
Hypersequent calculi will be used to axiomatize the consequence relation on hypersequents. Given a calculus HAX, a derivation of a hypersequent G from hypersequents G1,…,Gn in HAX is just a labeled tree, where the root is G, each node is labeled by a rule of HAX, and the leaves are either axioms or one of G1,…,Gn. As before, by G1,…,Gn⊢HAXG we mean that there exists such a derivation.
It is known [14] that the hypersequent calculus HŁ displayed in Table 4.13 axiomatizes the tautologies of Łukasiewicz logic, i.e., for any hypersequent G, we have
⊨HŁGiff⊢HŁG.
Let us now consider the extension of HŁ with the rule
G|Γ⪯ΔG|Δ≺ΓG(res)
and denote the resulting calculus as HŁres. The rule (res) clearly makes HŁres not analytic,4 but it is needed for obtaining a calculus which, as proved in the next theorem, captures as well the consequence relation (with finite sets of premises) of the Łukasiewicz logic on formulas.
Theorem 5.
For each hypersequentGand sequentsS1,…,Sn, we have:
S1,…,Sn⊢HŁresGiffS1,…,Sn⊨HŁG.
Proof.
The left-to-right direction holds in view of the soundness of HŁ and of the soundness of the rule (res), which is easily provable. For the converse direction, let us first introduce the following notation: for any multisets Γ and Δ of formulas, we let
(Γ≺Δ)¬=Δ⪯Γ(Γ⪯Δ)¬=Δ≺Γ
From S1,…,Sn⊨HŁG, we obtain
⊨HŁG|S1¬|…|Sn¬.
Indeed, if this were not the case, we would be able to find an evaluation which would satisfy neither G nor any of the Si¬. On the other hand, any evaluation which does not satisfy Si¬, will satisfy Si. Hence, we would obtain a counterexample to S1,…,Sn⊨HŁG.
Now, by the (weak) completeness of HŁ, we obtain that ⊢HŁG|S1¬|…|Sn¬. By repeated applications of the rule (res) to the latter hypersequent and the sequents S1,…,Sn, we get the desired proof of G from S1,…,Sn in the calculus HŁres.
4.2. A Hypersequent Calculus for PrŁ
In this subsection, we will introduce our hypersequent calculus HPrŁ for the logic PrŁ, seen as a consequence relation on hypersequents built over modal formulas of ℒPŁ. For ease of reference, we say that a sequent Γ◃Δ is (modal) PrŁ-sequent, classical sequent, or Ł-sequent whenever Γ and Δ are multisets of (modal) formulas of ℒPŁ, formulas of classical logic, or formulas Łukasiewicz logic, respectively. Furthermore, we say that a sequent Γ◃Δ is an atomic (modal) PrŁ-sequent, classical sequent, or Ł-sequent whenever Γ and Δ are multisets of atomic (modal) formulas of ℒPŁ, formulas of classical logic, or formulas of Łukasiewicz logic, respectively. We extend these conventions to hypersequents in the obvious way.
The semantics of modal PrŁ-hypersequents is defined in the expected way: Given a (probabilistic) Kripke model M and a multiset of modal formulas [γ1,⋯γn] of PrŁ, we let
||[γ1,⋯γn]||M=∑i⩽n(||γi||M−1)
and say that M satisfies a modal PrŁ-hypersequent G if ||Γ||M⩽||Δ||M (resp. ||Γ||M<||Δ||M) for some component Γ⪯Δ (resp. Γ≺Δ) of G; the consequence relation G1,…,Gn⊨PrŁG is then defined as expected. As in the case of Łukasiewicz logic, for every set Γ∪{δ} of modal ℒPŁ-formulas, we have
Γ⊨PrŁδiff{∅⪯γ|γ∈Γ}⊨PrŁ∅⪯δ.
To prove that HPrŁ axiomatizes PrŁ, we will make an essential use of the analogous result that HŁres axiomatizes Ł and thus our axiomatization results will share the restriction to premises being sequents (which again suffices to capture PrŁ seen as a consequence relation on formulas). The proof is based on a hypersequent variant of the translation of PrŁ into Ł, which is at the core of various proofs of completeness of PrŁ (the original idea is due to Hájek, Godo, and Esteva [4] and was further developed in subsequent works) [6–8]. In particular, we reduce the validity of modal PrŁ-hypersequents to the validity of certain consequences over Ł-hypersequents and thus (due to our axiomatization result) also to the derivability in HŁres. Then, we complete the proof by translating Ł-hypersequents back into modal PrŁ-hypersequents and showing that certain extra premises, corresponding to the axioms of probability, are derivable in HPrŁ.
Note that the translation does not depend on the proposed calculus HPrŁ, so let us deal with it first. We start by defining for each classical formula φ its equivalence set
φ¯={ψ|⊢CLψ↔φ}.
Now, for any atomic modal formula P(φ), we let P(φ)∗=pφ¯, where pφ¯ is a fresh propositional variable in the language of Ł, and for complex modal formulas, we let (γ1→Łγ2)∗=γ1∗→Łγ2∗ and ⊥Ł∗=⊥Ł. We also extend the translation to multisets of formulas in the expected way, i.e., [γ1,…,γn]∗=[γ1∗,…,γn∗]. Then, given a hypersequent G=Γ1◃1Δ1|…|Γn◃nΔn, we define G∗=Γ1∗◃1Δ1∗|…|Γn∗◃nΔn∗.
Finally, we include a translation of the axioms of probability into Ł-sequents. In order to keep the translation finite, we need to make it relative to a given finite set V of propositional variables. Let us define the set AXV∗ as the union of the following sets of Ł-sequents (by Vφ we denote the set of variables occurring in φ):
TAUTV={∅⪯pφ¯|Vφ⊆V and ⊢CLφ}CONTRV={pφ¯⪯⊥|Vφ⊆V and φ⊢CL⊥}ADDV={pφ∨ψ¯,pφ∧ψ¯⪯pφ¯,pψ¯|Vφ,Vψ⊆V}∪{pφ¯,pψ¯⪯pφ∨ψ¯,pφ∧ψ¯|Vφ,Vψ⊆V}
By AXV we denote the corresponding set of PrŁ-sequents, obtained by replacing each propositional variable pφ¯ by the atomic modal formula P(φ).
Lemma 6.
LetVbe a set of propositional variables. Then, for any modalPrŁ-hypersequentGcontaining only variables fromV, we have
⊨PrŁGiffAXV∗⊨ŁG∗.
Proof.
We prove the right-to-left direction counterpositively. Assume that ⊭PrŁG, i.e., there is a Kripke model M such that, for each component Γ⪯Δ (resp. Γ≺Δ) of G, we have ||Γ||M>||Δ||M (resp. ||Γ||M⩾||Δ||M). Now, let e^ be an evaluation of Łukasiewicz logic such that ê(pφ¯)=||P(φ)||M for each φ. This evaluation is well defined, since pφ¯=pψ¯ means that ⊢CLφ↔ψ, hence ||P(φ)||M=||P(ψ)||M. It is straightforward to check that ê satisfies all of the sequents in AXV∗, and none of the components of G∗, i.e., it provides a counterexample to AXV∗⊨ŁG∗.
For the left-to-right direction, let ê be an evaluation satisfying the Ł-sequents from AXV∗ that does not satisfy G∗.
From the former assumption we know that, for each φ,ψ with Vφ,Vψ⊆V, we have
e^(p⊤¯)=1
e^(p⊥¯)=0
e^(pφ∨ψ¯)+ê(pφ∧ψ¯)=ê(pφ¯)+ê(pψ¯).
Let W be the set of classical evaluations and consider the subset of the powerset of W defined as
BV={{w|w(φ)=1}|φ a formula and Vφ⊆V}.
Clearly, BV is the domain of a Boolean subalgebra BV of the powerset algebra of W. Then, we define a function μ′:BV→[0,1] as
μ′({w|w(φ)=1})=ê(pφ¯).
Due to the properties of ê listed above, we know that μ′ is a finitely additive probability measure on BV and so, by the Horn–Tarski theorem [16,17], we know that there is a finitely additive probability measure μ on the powerset algebra of W such that μ(X)=μ′(X) for each X∈BV.
Then, M=〈W,〈w〉w∈W,μ〉 is a Kripke model (the measurability condition is trivial as all subsets of W are μ-measurable) and we only need to check that G is not satisfied in M. This is a routine check, since ||P(φ)||M=ê(pφ¯) and so ||Γ||M=ê(Γ∗) for each multiset Γ of modal formulas occurring in G.
The calculus HPrŁ that we propose as axiomatization of the logic PrŁ is composed of all the rules in Table 1, which are applicable to classical hypersequents, and all the rules in Table 2, which consist of
variants of all of the rules in Table 1, plus the rule (res) applicable to modal PrŁ-hypersequents,
the axiom
⪯p|p⪯⊥(cl)
where the propositional variable p belongs to the language of classical logic CL, i.e., to the nonmodal formulas of PrŁ,
Additional rules for the hypersequent calculus HPrŁ for PrŁ.
A few additional words are needed on the rule (gen). First, note that the multiset [⊥]l can also be empty (the multiplicity l is allowed to be 0), i.e., the presence of ⊥ is not required for the application of the rule. Second, it can only be applied to classical sequents (i.e., hypersequents with only one component) and produces a modal PrŁ-sequent.
To establish the announced axiomatizability result, we only need to prepare one crucial yet easy-to-prove lemma.
Lemma 7.
LetGbe a modalPrŁ-hypersequent such that⊨PrŁG. Then, AXV⊢HPrŁGand there is a derivation ofGfromAXVwhich does not use the rule(gen).
Proof.
By Lemma 6 and Theorem 5 we know that AXV∗⊢HŁresG∗. Replacing each translated atom pφ¯ in the latter proof by an atomic modal formula P(φ), and replacing each rule used in HŁ by its modal counterpart in HPrŁ, we obtain a proof of G from AXV in HPrŁ which does not make use of the rule (gen).
Theorem 8.
For each modalPrŁ-hypersequentGand modalPrŁ-sequentsS1,…,Snwe have
S1,…,Sn⊢HPrŁGiffS1,…,Sn⊨PrŁG.
Proof.
We prove the claim without premises; the extension to the full claim is then done using the rule (res) as in the proof of Theorem 5.
The soundness is easy. For the completeness direction, assume ⊨PrŁG. Then, by the previous lemma, AXV⊢HPrŁG and thus it suffices to show that, for each S∈AXV, we have ⊢HPrŁS.
This can be obtained by suitable applications of the rule (gen). First, observe that, for Vφ,Vψ⊆V, the following sequents
φ∨ψ,φ∧ψ⪯φ,ψ and φ,ψ⪯φ∨ψ,φ∧ψ
are derivable in HŁ, hence also in HPrŁ. Adding to their derivations an application of the rule of (gen) results in a derivation of the corresponding sequent from AXV in HPrŁ.
Next, let us now show that the sequent ∅⪯P(φ) is derivable in HPrŁ, for any classical tautology φ. First, note that if φ is a classical tautology, letting p1,…,pn be the variables occurring in φ, we have that p1∨¬p1,…pn∨¬pn⊨[0,1]Łφ; hence, in particular,
∅⪯p1∨¬p1,…,∅⪯pn∨¬pn⊨Ł∅⪯φ
and, by the finite strong completeness of HŁ(res), there is a derivation d of ∅⪯φ from the premises ∅⪯p1∨¬p1,…,∅⪯pn∨¬pn in the calculus HŁ(res). Recall that all the rules of this calculus belong to HPrŁ as well, and hence we obtain our desired derivation of ∅⪯P(φ) in HPrŁ by appending, after the conclusion ∅⪯φ of d, an application of the rule (gen), and before each premise ∅⪯pi∨¬pi the following:
Finally, let us consider the sequents in CONTRV. Applying an argument similar to the one for TAUTV, we have that, for any nonmodal formula φ such that φ⊢CL⊥, the sequent
φ⪯⊥
is derivable in HPrŁ. A derivation of P(φ)⪯⊥Ł is then obtained by adding an application of (gen) to the derivation φ⪯⊥.
5. ALTERNATIVE PROOF OF COMPLETENESS OF Prlin AND TRANSLATION INTO PrŁ
In this section, we will show that the logic Prlin can be semantically translated into the logic PrŁ (seen as consequence relation of hypersequents) and obtain an alternative translation into PrŁ△ (seen as consequence on formulas). We will also use a converse of this translation and the fact that HPrŁ axiomatizes PrŁ to obtain an alternative proof of the fact that the axiomatic system AXPrlin introduced in Subsection 2.4 is indeed an axiomatization of Prlin, i.e., we show that
Γ⊢AXPrlinδiffΓ⊨Prlinδ.
Recall that modal formulas of Prlin are combinations of basic inequality formulas using connectives of classical logic. Following the usual classical terminology, let us call the basic inequality formulas and their negation literals and their disjunctions clauses. Then, we know that each modal formula of Prlin is equivalent to a conjunction of certain clauses.
Let us start our work in this section by showing that the clauses of Prlin can be faithfully translated into atomic modal PrŁ-hypersequents. First, consider a basic inequality formula γ of the form
∑i=1naiP(φi)⩾c
and note that γ can be equivalently replaced (modulo a suitable permutations) by another inequality
Given a basic inequality formula γ and given γH=Γ⪯Δ, we define (¬γ)H as Δ≺Γ. Finally, given any clause δ=γ1∨⋯∨γn, we define δH as the hypersequent γ1H|…|γnH.
Lemma 9.
LetMbe a Kripke model andδa clause inℒlin. Then, Msatisfiesδiff it satisfiesδH.
Proof.
Let us first assume that δ is a basic inequality formula of the form
∑i=1maiP(φi)⩽∑i=m+1naiP(φi)−c
where all ais are nonnegative. We know that M satisfies δ iff the corresponding inequality holds with P(φi) replaced by xi=μ(φiM). Recall that, using the definition of s(γ), we can write that equivalently as
∑i=1maixi−∑i=1mai⩽∑i=m+1naixi−∑i=m+1nai−s(δ)
Note that for each nonnegative integer k we have ||[⊥]k||M=−k and we also have
Thus, indeed, δ is satisfied in M iff δH is (we only have to distinguish if s(δ) is negative or not and move it to the appropriate side of the inequality, which clearly coincides with definition of δH).
The case of δ being a negated literal or a clause then easily follows using the related definitions of satisfiability of formulas of ℒlin and PrŁ-hypersequents.
Theorem 10.
LetΓ∪{δ}be a finite set of formulas ofℒlinandδ1∧⋯∧δma conjunctive normal form of(∧γ∈Γγ)→δ. Then
Γ⊨Prlinδiff⊨PrŁδiH for each i=1,…,m.
Proof.
First note that, due to a classical reasoning, we have Γ⊨Prlinδ iff for each i we have ⊨Prlinδi and so the proof follows from Lemma 9.
We can use this result to provide an alternative translation from Prlin into PrŁ△. It is well known [14] that any Ł-hypersequent G can be interpreted (using again essentially McNaughton theorem) as a formula I(G) of Ł△ (the operation △ is essential to capture the sequents of the form Γ≺Δ) such that ⊨ŁG if and only if ⊨Ł△I(G). Recalling that the atomic modal formulas of PrŁ and PrŁ△ are the same, we can replace the propositional atoms by such formulas and extend the previous result to probability logics: ⊨PrŁG if and only if ⊨PrŁ△I(G). Therefore, we easily obtain:
Corollary 11.
LetΓ∪{δ}be a finite set of formulas ofℒlinandδ1∧⋯∧δma conjunctive normal form of(∧γ∈Γγ)→δ. Then,
Γ⊨Prlinδiff⊨PrŁ△I(δ1H)∧⋯∧I(δmH).
We will now provide a converse translation, from atomic modal PrŁ-hypersequents to formulas of Prlin. This time we will proceed syntactically: we will show that, if an atomic modal hypersequent is provable in HPrŁ, its translation is derivable in AXPrlin. This, together with the previous semantical translation, will provide us with an alternative completeness proof for Prlin.
Consider a multiset Γ of atomic PrŁ-formulas (i.e., formulas of the form P(φ) or ⊥Ł), and recall that we denote by Γ(α) the number of occurrences of the formula α in Γ. We define a linear term tΓ:
tΓ=∑α∈|Γ|,α≠⊥ŁΓ(α)α
Let Γ,Δ be two multisets of atomic PrŁ-formulas; we define the translation of atomic sequents Γ⪯Δ and Γ≺Δ as follows:
and, for any atomic modal PrŁ-hypersequent H=Γ1◃1Δ1|…|Γn◃nΔn, we define
H♯=(Γ1◃1Γ1)♯∨⋯∨(Γn◃nΓn)♯.
Let us now show that the translation (⋅)♯ is actually an inverse of the translation (⋅)H, i.e., for any clause δ of ℒlin, we have (δH)♯=δ. We show the claim for δ being a basic inequality formula, the generalization to clauses being easy. Let us assume, without loss of generality, that δ is of the form
∑i=1maiP(φi)⩽∑i=m+1naiP(φi)−c
with ai>0 for i=1,…,n. We only handle the case when
s(δ)=∑i=1mai−∑i=m+1nai+c⩾0,
since the case where s(δ)<0 is similar. Therefore, by the definition of the translation (⋅)H,
LetH0be an atomic modalPrŁ-hypersequent. If⊨PrŁH0, then⊢AXPrlinH0♯.
Proof.
Due to Lemma 7, we know that there is a derivation d of H0 from the set of sequents AXV in the calculus HPrŁ such that d does not use the rule (gen). Note that, except for (res) all the rules of the calculus are analytic, hence they cannot have premises using nonatomic modal hypersequents, if the conclusions are atomic. On the other hand, inspecting the proof of the mentioned Lemma 7, we also know that the rule (res) needs to be applied in d only to premises containing atomic modal formulas. Therefore, all PrŁ-hypersequents occurring in d have to be atomic and modal. The proof is done by showing that for each such hypersequent G0 (i.e., in particular, for the final hypersequent H0), we have ⊢AXPrlinG0♯.
We proceed by induction on the length of d. Let us first consider the case that G0 is one of the axioms of HPrŁ, i.e., we need to find proofs of the following formulas:
P(φ)⩽P(φ) (if G0 is an instance of an axiom (id)): this is just axiom (LQ1).
0⩽P(φ) (if G0 is an instance of an axiom (⊥)): this is just axiom (QU1).
0⩽0 (if G0 is an instance of axiom (emp)): this is just axiom (LQ1).
¬(0⩽−1) (if G0 is an instance of axiom (⊥≺)): it follows using axioms (LQ1) and (LQ7).
Next we deal with the case G0∈AXV, i.e., we need to find proofs of the following formulas:
1⩽P(φ) whenever ⊢CLφ: Clearly, in this case ⊢Prlinφ↔⊤ and so, by the axiom (QU2) and the rule (QUGEN), we obtain ⊢Prlin1⩽P(φ).
P(φ)⩽0 whenever φ⊢CL⊥. Using (QU3) we have that P(⊤∧φ)+P(⊤∧¬φ)=P(⊤). By (QU1) and (QUGEN), we get P(φ)+P(¬φ)=1. On the other hand, since ¬φ is a tautology, by the previous point we have P(¬φ)=1, hence we finally obtain a derivation of P(φ)=0.
P(φ∨ψ)+P(φ∧ψ)⩽P(φ)+P(ψ) and P(φ)+P(ψ)⩽P(φ∨ψ)+P(φ∧ψ): We prove both inequalities at once using two instances of axiom (QU3):
P(φ)=P(φ∧ψ)+P(φ∧¬ψ)P(φ∨ψ)=P((φ∨ψ)∧ψ)+P((φ∨ψ)∧¬ψ)
As the first one is equivalent (using the rule (QUGEN), properties of classical logic, and rules for manipulation of equalities in Prlin) to
P(φ∨ψ)=P(ψ)+P(φ∧¬ψ),
the claim easily follows by simple manipulation of equalities in the logic Prlin.
Now assume that G0 is a consequence of some of the rules of HPrŁ. Note that, as d is a derivation of the atomic modal hypersequent H0, we do not need to check the case of logical rules and have to deal with the structural ones only. The case of rules (ew) and (ec) is simple. Indeed, whenever G0=G|H, then G0♯=G♯∨H♯ and so easily get ⊢AXPrlinG0♯ from either of the two possible induction assumptions: ⊢AXPrlinG♯ or ⊢AXPrlinG♯∨H♯∨H♯.
Let us now consider an instance of the rule (split⪯) (the case of (splitŁ) is handled analogously), i.e., the case where G0=G|Γ1⪯Δ1|Γ2⪯Δ2 and the premise is G|Γ1,Γ2⪯Δ1,Δ2. By induction hypothesis, we have ⊢AXPrlinG♯∨ϵ, where ϵ=(Γ1,Γ2⪯Δ1,Δ2)♯. Without loss of generality, let ϵ1=(Γ1⪯Δ1)♯=t1⩽c1 and ϵ2=(Γ2⪯Δ2)♯=t2⩽c2. We have then
ϵ=t1+t2⩽c1+c2
We want to prove that
⊢AXPrlinG♯∨(t1⩽c1)∨(t2⩽c2).
First, recalling that ϵ is the same as the formula −t1−t2⩾−c1−c2, and t2⩽c2 is the same as −t2⩾−c2, we have that
(ϵ∧t1⩾c1)→t2⩽c2
is an instance of axiom (LQ4). On the other hand, we have that t1⩽c1∨t1⩾c1 is an instance of axiom (LQ6). By classical reasoning, we obtain thus a derivation in AXPrlin of
ε→t1⩽c1∨t2⩽c2
hence, a derivation in AXPrlin of G0♯∨ε1∨ε2 from G0♯∨ϵ.
For the rule (mix), we have G0=G|Γ1,Γ2⪯Δ1,Δ2 and, by the induction hypothesis, we have ⊢AXPrlinG♯∨(Γ1⪯Δ1)♯ and ⊢AXPrlinG♯∨(Γ2⪯Δ2)♯. Note that, from axiom (LQ4), we know that (Γ1⪯Δ1)♯∧(Γ2⪯Δ2)♯→(Γ1,Γ2⪯Δ1,Δ2)♯ and so the claim follows using a simple classical reasoning.
For the rules (wl), we have either G0=G|Γ,γ⪯Δ or G0=G|Γ,γ≺Δ and, by the induction hypothesis, we have either ⊢AXPrlinG♯∨(Γ⪯Δ)♯ or ⊢PrlinG♯∨(Γ≺Δ)♯. We deal with the first case with the additional assumption that γ=P(φ); the second case and the case γ=⊥Ł are analogous. Assume that (Γ⪯Δ)♯=t⩽c and note that (Γ,γ⪯Δ)♯=t+P(φ)⩽c+1. So, the following instance of (LQ4):
(−P(φ)⩾−1)∧(−t⩾−c)→−t−P(φ)⩾−c−1
together with the known fact that ⊢AXPrlinP(φ)⩽1, completes the proof, using a simple classical reasoning.
For the rule (w⊥), we have G0=(G|Γ,⊥Ł≺Δ) and, by the induction hypothesis, we know that ⊢AXPrlinG♯∨(Γ⪯Δ)♯. Let us compute that
(Γ,⊥≺Δ)♯=¬(tΔ⩽tΓ−c(Γ⪯Δ)−1)=(tΔ−tΓ>−c(Γ⪯Δ)−1)
and note that this formula follows from (Γ⪯Δ)♯=tΔ−tΓ⩾−c(Γ⪯Δ) using axiom (LQ7). Thus, again, a classical reasoning completes the proof.
Finally, we deal with the rule (res), i.e., when G0=G and the premises are G|Γ⪯Δ and G|Δ≺Γ. Thus, by the induction hypothesis, we have ⊢PrlinG♯∨(Γ⩽Δ)♯ and ⊢PrlinG♯∨(Δ≺Γ)♯. Note that the latter is equivalent to ⊢PrlinG♯∨¬((Γ⩽Δ)♯ which due to classical reasoning entails ⊢PrlinG♯.
Using this lemma, together with Theorems 10 and 8, we obtain the promised alternative proof of axiomatization of Prlin.
Theorem 13.
LetΓ∪{δ}be a finite set of formulas ofℒlin. Then,
Γ⊢AXPrlinδiffΓ⊨Prlinδ.
Proof.
The left-to-right direction is easy to check. For the right-to-left direction, by Theorem 10, we obtain that ⊨PrŁδiHfor each i=1,…,m, where δ1∧⋯∧δm is a conjunctive normal form of (∧γ∈Γγ)→δ. Then, by Lemma 12, since (δiH)♯=δi, we get that ⊢AXPrlinδi for each i=1,…,m. As axioms and rules of AXPrlin for modal formulas are those of classical logic, we first obtain ⊢AXPrlin(∧γ∈Γγ)→δ and, thus, also Γ⊢AXPrlinδ.
6. CONCLUSION
In this paper we have given a precise answer to the question about the relationship between the logics of uncertainty introduced and studied by Fagin, Halpern, Meggido, and others, and those developed in the area of mathematical fuzzy logic by Hájek, Godo, Esteva, and others. Indeed, we have shown that Prlin and Prpol can be faithfully translated, respectively, into the two-layered modal fuzzy logics PrŁ△ and PrPŁ△, and vice versa. Moreover, we have contributed to the proof theory of these logics by offering a hypersequent calculus of relations HPrŁ for the logic PrŁ (which could be easily extended to a calculus for PrŁ△). Interestingly enough, we have obtained two benefits from the formalism of hypersequents of relations for the study of Prlin: it allowed us to provide another translation into a fuzzy logic without using the △ connective, and it gave us a new proof of the axiomatization of Prlin. Therefore, this paper has provided some further evidence that the mathematical fuzzy logic approach to reasoning about uncertain events is a fruitful one that, in a sense, can encompass other popular approaches.
Let us mention several possible future lines of research. First, regarding proof theory, a crucially important open question is whether the calculus HPrŁ can be reformulated as an analytic one, i.e., without the rule (res) or any variant thereof. Note that, however, in light of our completeness theorem, any valid PrŁ-hypersequent G has a proof in HPrŁ with a well-structured form: a part of the proof using only the modal rules, a part using only the nonmodal rules and the rule (gen), and finally a series of applications of the nonanalytic rule (res), in order to obtain a derivation of G. This consideration might be instrumental in using the calculus for establishing interesting computational complexity bounds and/or finding conditions under which the rule (res) can be eliminated.
Regarding the proof theory of other two-layered modal fuzzy logics, we believe that the crucial trick used for proving completeness of the calculus, i.e., the translation of modal hypersequents into propositional ones, could be put to use to obtain complete hypersequent calculi in a much more general framework [6,7]. On the other hand, this method can be exploited in its full power only when we already possess a hypersequent calculus for the logic handling the modal formulas. Since, to the best of our knowledge, such a calculus is lacking for the logic PŁ, we do not see an easy way to extend our approach for obtaining analogous results for the logics PrPŁ△ and Prpol.
Moreover, we plan to continue the investigation of translations between logics of uncertainty: in particular we believe that also other classical logics dealing with measures of uncertainty different from probability, such as, e.g., plausibilities or belief functions [3,6], are amenable to similar translations into suitable two-layered modal fuzzy logics.
Finally, we plan to develop the existing abstract two-layered formalism [7] in two directions: (1) to provide, in the style of abstract algebraic logic, general completeness theorems of two-layered modal logics obtained by combination of arbitrary members of a fairly wide family of nonclassical logics and (2) show that such general results subsume most (if not all) completeness theorems provided so far in the literature for particular systems.
CONFLICT OF INTEREST
The authors declare that they have no conflict of interests.
AUTHORS' CONTRIBUTIONS
That they have equally contributed to the paper.
ACKNOWLEDGMENTS
The authors were supported by the grant GA17-04630S of the Czech Science Foundation. Cintula also acknowledges support by RVO 67985807. Baldi also acknowledges support by the Department of “Philosophy Piero Martinetti” of the University of Milan under the Project “Departments of Excellence 2018-2022” awarded by the Ministry of Education, University and Research (MIUR).
Footnotes
This paper is an extended and revised version of the conference communication [1] Besides improving the notation and streamlining the presentation of our original results, in this paper: (1) we provide inverse translations from fuzzy to classical probability logics (Theorems 2 and 4), (2) we give a hypersequent calculus of relations that axiomatizes Łukasiewicz logic in a strong sense (Theorem 5), (3) we axiomatize the probability logic based on Łukasiewicz logic with a hypersequent calculus of relations (Theorem 8), (4) using this result, we obtain simpler proofs of additional translations between fuzzy and classical probability logics (Theorem 10 and Corollary 11) and, finally, (5) we give an alternative proof of axiomatization of one of the prominent classical probability logics (Theorem 13).
The logics of uncertainty introduced above are usually denoted using different symbols in the literature. In particular, the classical ones (or more precisely their axiomatic systems) Prlin and Prpol are denoted by AXprob and AXprob,× in Halpern's book [3] and, following the notational conventions introduced in Hájek's book [8], the fuzzy ones PrŁ, PrŁ△, and PrPŁ△ are traditionally denoted as FP(Ł), FP(Ł△), FP(PŁ), respectively. We have opted here for a uniform but neutral terminology, for ease of reference through the paper.
Note that we also include the rules for the connectives ∨, ∧, and ¬, although they are in principle derivable from those for → and ⊥ (recall that the former connectives are definable via the latter ones in Łukasiewicz logic). Also, note that when the symbol ◃ occurs in a rule of the calculus, it has to be read as two rules, one for each uniform instantiation of ◃.
Let us recall that a calculus is said to be analytic when, for all of its rules, all the formulas occurring in the premises already occur in the conclusion. The prototypical example of rule that breaks the analyticity of a proof-system is the (cut) rule; a variant thereof can actually be shown to be derivable in our calculus HŁres.
6.T. Flaminio, L. Godo, and E. Marchioni, Reasoning about uncertainty of fuzzy events: an overview, P. Cintula, C. Fermüller, and L. Godo (editors), Understanding Vagueness: Logical, Philosophical, and Linguistic Perspectives, College Publications, London, England, Vol. 36, 2011, pp. 367-400.
12.P. Hájek and S. Tulipani, Complexity of fuzzy probability logics, Fundam. Inform., Vol. 45, 2001, pp. 207-213.
13.S. Aguzzoli, S. Bova, and B. Gerla, Free algebras and functional representation for fuzzy logics, P. Cintula, P. Hájek, and C. Noguera (editors), Handbook of Mathematical Fuzzy Logic, College Publications, London, England, Vol. 37, 2011, pp. 713-791. Chapter IX in: 38
TY - JOUR
AU - Paolo Baldi
AU - Petr Cintula
AU - Carles Noguera
PY - 2020
DA - 2020/07/17
TI - Classical and Fuzzy Two-Layered Modal Logics for Uncertainty: Translations and Proof-Theory
JO - International Journal of Computational Intelligence Systems
SP - 988
EP - 1001
VL - 13
IS - 1
SN - 1875-6883
UR - https://doi.org/10.2991/ijcis.d.200703.001
DO - 10.2991/ijcis.d.200703.001
ID - Baldi2020
ER -
, Petr Cintula2, 