Multi-agent Logics for Reasoning About Higher-Order Upper and Lower Probabilities

Abstract

We present a propositional and a first-order logic for reasoning about higher-order upper and lower probabilities. We provide sound and complete axiomatizations for the logics and we prove decidability in the propositional case. Furthermore, we show that the introduced logics generalize some existing probability logics.

1 Introduction

In the last few decades, uncertain reasoning has become an active topic of investigation for researchers in the fields of computer science, artificial intelligence and cognitive science. The frameworks designed for modeling uncertainty often use probability-based interpretation of knowledge or belief. One particular line of research concerns the formalization of reasoning about probability in terms of logic with a well-defined syntax and semantics (Fagin et al. 1990; Fagin and Halpern 1994; Fattorosi-Barnaba and Amati 1989; Frish and Haddawy 1994; Halpern 1990; Heifetz and Mongin 2001; Meier 2012; Ognjanović and Rašković 1999, 2000; Ognjanović et al. 2016; Rašković et al. 2008).

In order to model some situations of interest, where sharp numerical probabilities appear too simple for modeling uncertainty, various imprecise probability models are developed (de Cooman and Hermans 2008; Dubois and Prade 1988; Levi 1980; Miranda 2008; Shafer 1976; Walley 1991, 2000; Zadeh 1978). Some of those approaches use sets of probability measures instead of one fixed measure, and the uncertainty is represented by two boundaries, called lower probability and upper probability (Huber 1981; Kyburg 1961). Given an arbitrary set P of probability measures, the former one assigns to an event X the infimum of the probabilities assigned to X by the measures in P, while the later one returns their supremum.

Those two probability notions were previously formalized in the logic developed in Halpern and Pucella (2002), where lower and upper probability operators are applied to propositional formulas, and in Savić et al. (2017a), where a first-order logic is also considered.

In this paper, we use the papers (Halpern and Pucella 2002; Savić et al. 2017a) as a starting point and generalize them in a way that we reason not only about lower and upper probabilities an agent assigns to a certain event, but also about her uncertain belief about other agent’s imprecise probabilities. Thus, we introduce separate lower and upper probability operators for different agents, and we allow nesting of the operators, similarly as it has been done in Fagin and Halpern (1994) in the case of simple probabilities. We first present a propositional variant of this logic, which we denote by ${\mathsf {ILUPP}}$,¹ and then we extend it to a first-order logic. We prove that ${\mathsf {ILUPP}}$ is decidable and we propose sound and strongly complete axiomatizations for both logics.

Our language contains the upper and lower probability operators $U^a_{\ge r}$ and $L^a_{\ge r}$, for every agent a and every rational number r from the unit interval (we also introduce the operators with other types of inequalities, like $U^a_{=r}$). Consider the following example: Suppose that an agentais planning to visit a city based on the weather reports from several sources, and she decides to take an action if the probability of rain is at most$\frac{1}{10}$, according to all reports she considers. Since she wishes to go together withb, she should be sure with probability at least$\frac{9}{10}$thatb(who might consult different weather reports) has the same conclusion about the possibility of rain. In our language, this situation can be formalized as

$$\begin{aligned} U_{\le \frac{1}{10}}^a Rain \wedge L_{\ge \frac{9}{10}}^a\left( U_{\le \frac{1}{10}}^b Rain\right) . \end{aligned}$$

We also introduce the notions of lower and upper probability of a (possibly infinite) set of agents by introducing the operators $L_{\ge s}^G$ and $U_{\ge s}^G$. In our approach we assume that the agents can share their sets of probabilities in order to obtain a larger set that is available to all the members of the group.

It is worth clarifying the additional expressive power of our first-order logic, which we denote by ${\mathsf {ILUPFO}}$, and it’s comparison with (Savić et al. 2017a). The paper (Savić et al. 2017a) introduces a logic whose syntax allows only Boolean combinations of formulas in which lower and upper probability operators are applied to first order sentences. On the other hand, here we use the most general approach, allowing arbitrary combination of probability operators, so we can express the statement like “according to the agent a, the lower probability of rain in all cities is at least$\frac{1}{3}$” ($L_{\ge \frac{1}{3}}^a \forall x Rain(x))$, but also “There exists a city in which it will surely not rain:”

$$\begin{aligned} (\exists x)U_{= 0}^a Rain(x). \end{aligned}$$

The appropriate modal semantics for our logics consists of a specific class of Kripke models, in which every world is equipped with sets of probability measures (one set for each agent).

We propose sound and strongly complete axiomatizations of the logics. Interestingly, we use the same axiomatizations that we used in Savić et al. (2017a), and we show that they are also complete for the richer logics presented here. Of course, the instances of the axiom schemata are different, because the sets of formulas of ${\mathsf {ILUPP}}$ and ${\mathsf {ILUPFO}}$ are larger, due to nesting of lower and upper probability operators, and due to the presence of more agents. Also, the definition of the syntactical consequence (proof) $\vdash$ is different, due to the different interpretation of classical formulas. Since the sets of formulas and the classes of models are different, the proof techniques are modified. In order to achieve completeness, we use a Henkin-like construction, following some of our earlier developed methods (Doder et al. 2010; Ognjanović and Rašković 1999; Rašković et al. 2008; Savić et al. 2017a; Tomović et al. 2015).

In addition, we show how to extend the proposed axiomatizations in order to properly capture the notions of lower and upper probability of an infinite set of agents.

The interesting situation that one axiomatic system is sound and complete for more than one class of models is not an exception. For example, modal system K is also sound and complete with respect to the class of all irreflexive models (Hughes and Cresswell 1984).

We also prove that the satisfiability problem for ${\mathsf {ILUPP}}$ logic is decidable. We combine the method of filtration (Hughes and Cresswell 1984) and a reduction to linear programming. In the first part of the proof, we show that a formula $\alpha$ is satisfiable in a world w of an ${\mathsf {ILUPP}}$ model if and only if it is satisfiable in a finite model, i.e., a model with a finite number of worlds, bounded by a number which is a function of the length of $\alpha$, and such that the sets of probability measures are finite in every world of the model. Note that, while in a standard modal framework this is enough to prove decidability, since for every natural number k there are only finitely many modal models with k worlds, this is not the case for our logic. Indeed, since our models involve sets of probability measures, for every finite set of k worlds, there are uncountably many probability measures defined on them, and uncountably many models with k worlds. However, in the second part of the proof we use a reduction to linear programming to solve the probabilistic satisfiability in a finite number of steps.

Finally, we show that the logics proposed in this paper generalize the logics for reasoning about sharp probabilities from Ognjanović and Rašković (2000), Ognjanović et al. (2016). Indeed, we use an additional axiom scheme to restrict the class of our models to the models isomorphic to those from Ognjanović and Rašković (2000), Ognjanović et al. (2016). We also formally infer all the axioms from Ognjanović and Rašković (2000), Ognjanović et al. (2016) using our extended axiomatization.

The paper is organized as follows: in Sect. 2 we introduce the set of formulas of the logic ${\mathsf {ILUPP}}$ and we define the corresponding semantics. Then, in Sect. 3 we prove that the satisfiability problem for the logic ${\mathsf {ILUPP}}$ is decidable. In Sect. 4 we provide an axiomatic system ${\mathsf {ILUPP}}$, and we prove that the axiomatization is strongly complete. The first-order logic ${\mathsf {ILUPFO}}$ is presented in Sect. 5. In Sect. 6, we show how to extend the presented axiomatic systems in case of infinite number of agents and we discuss decidability issues. We show that the proposed logics generalize the probability logics from Ognjanović and Rašković (2000), Ognjanović et al. (2016) in Sect. 7. Finally, Sect. 8 contains some concluding remarks.

2 The Logic ${\mathsf {ILUPP}}$

In this section we introduce the syntax and the semantics of the logic ${\mathsf {ILUPP}}$.

Let $\varSigma =\{a,b,\ldots \}$ be a finite, non-empty set of agents. Let $S=\mathbb {Q}\cap [0,1]$ and let $\mathcal L=\{p,q,r,\ldots \}$ be a denumerable set of propositional letters. The language of the logic ${\mathsf {ILUPP}}$ consists of the elements of set $\mathcal L$, propositional connectives $\lnot$ and $\wedge$, and

• the list of upper probability operators $U_{\ge s}^a$, for every $a\in \varSigma$ and $s\in S$,

• the list of lower probability operators $L_{\ge s}^a$, for every $a\in \varSigma$ and $s\in S$.

Definition 1

(Formula) The set $For_{{\mathsf {ILUPP}}}$ of formulas is the smallest set containing all elements of $\mathcal L$ and that is closed under following formation rules: if $\alpha ,\beta$ are formulas, then $L^a_{\ge s}\alpha$, $U^a_{\ge s}\alpha$, $\lnot \alpha$ and $\alpha \wedge \beta$ are formulas as well. The formulas from $For_{{\mathsf {ILUPP}}}$ will be denoted by $\alpha ,\beta ,\ldots$

Intuitively, $U^a_{\ge s}\alpha$ means that according to an agent a, upper probability that a formula $\alpha$ is true is greater or equal to s and analoguosly $L^a_{\ge s}\alpha$ means that according to an agent a lower probability that a formula $\alpha$ is true is greater or equal to s.

Note that we use conjunction and negation as primitive connectives, while $\vee$, $\rightarrow$ and $\leftrightarrow$ are introduced in the usual way. We also use abbreviations to introduce other types of inequalities:

• $U_{< s}^a\alpha$ is $\lnot U_{\ge s}^a\alpha$, $U_{\le s}^a\alpha$ is $L_{\ge 1-s}^a\lnot \alpha$, $U_{=s}^a\alpha$ is $U_{\le s}^a\alpha \wedge U_{\ge s}^a\alpha$, $U_{> s}^a\alpha$ is $\lnot U_{\le s}^a\alpha$,

• $L_{< s}^a\alpha$ is $\lnot L_{\ge s}^a\alpha$, $L_{\le s}^a\alpha$ is $U_{\ge 1-s}^a\lnot \alpha$, $L_{=s}^a\alpha$ is $L_{\le s}^a\alpha \wedge L_{\ge s}^a\alpha$, $L_{> s}^a\alpha$ is $\lnot L_{\le s}^a\alpha$.

For example, the expression

$$\begin{aligned} p\wedge U_{=0.9}^a L_{=0.3}^b(p\vee q) \end{aligned}$$

is a formula of our language.

Furthermore, we introduce the additional operators $L_{\ge s}^G$ and $U_{\ge s}^G$ that can speak about upper/lower probability of a group of agentsG. We assume that the agents can share their sets of probabilities in order to obtain a larger set that is available to all the members of the group. Naturally, upper probability of an event w.r.t. that set will be at least upper probability of an individual agent; similarly, its lower probability is at most lower probability of a member of the group. Following that intuition, we introduce the abbreviations:

• $L_{\ge s}^G\alpha$ is the formula $\bigwedge _{a \in G}L_{\ge s}^a\alpha$,

• $U_{\ge s}^G\alpha$ is the formula $\bigvee _{a \in G}U_{\ge s}^a\alpha$.

We also introduce the corresponding operators with other types of inequalities, in the same way as we have done it for individual agents.

This formalization is in tune with the intuition behind the example given in the introduction, where the agent ais reasoning in a skeptical way: she will visit a city as the probability of rain is at most$\frac{1}{10}$, according toallweather reports she considers. Then, if the agentbshares a new, more negative report coming from a different source (e.g. probability of rain is$\frac{1}{5}$), acan revise her decision based on the updated upper probability.

At first glance, the asymmetry between $L_{\ge s}^G$ and $U_{\ge s}^G$ (conjunction vs disjunction) might look counter-intuitive. On the contrary, we believe that using the same type of connective (e.g. conjunction, which would be in the spirit of the epistemic operator $E_G$ “everyone in the group G knows”) would not fit the general intuition behind upper and lower probabilities: if increasing (resp. decreasing) upper probability comes from enlarging (narrowing) the set of probabilities, then lower probability should decrease (increase).² Moreover, we will see that our definition of $L_{\ge s}^G$ and $U_{\ge s}^G$ implies that the groups semantically behave like individual agents.

In the last section, we discuss the alternative possibility for defining lower and upper probability of a group.

The semantics of the logic ${\mathsf {ILUPP}}$ is based on the possible-world approach. Every world is equipped with an evaluation function on propositional letters, and one generalized probability space for each agent.

Definition 2

(${\mathsf {ILUPP}}$-structure) An ${\mathsf {ILUPP}}$-structure is a tuple $\langle W,LUP,\upsilon \rangle$, where:

• W is a nonempty set of worlds,

• LUP assigns, to every $w\in W$ and every $a\in \varSigma$, a space, such that $LUP(a,w)=\langle W(a,w),H(a,w),P(a,w)\rangle$, where:

  • $\emptyset \ne W(a,w)\subseteq W$,

  • H(a, w) is an algebra of subsets of W(a, w), i.e. a set of subsets of W(a, w) such that:

    • $W(a,w)\in H(a,w)$,

    • if $A,B\in H(a,w)$, then $W(a,w){\setminus } A\in H(a,w)$ and $A\cup B\in H(a,w)$,

  • P(a, w) is a set of finitely additive probability measures defined on H(a, w), i.e. for every $\mu (a,w)\in P(a,w)$, $\mu (a,w):H(a,w)\longrightarrow [0,1]$ and the following conditions hold:

    • $\mu (a,w)(W(a,w))=1$,

    • $\mu (a,w)(A\cup B)=\mu (a,w) (A)+\mu (a,w) (B)$, whenever $A\cap B=\emptyset$.

• $\upsilon : W\times \mathcal L\longrightarrow \{true,false\}$ provides for each world $w\in W$ a two-valued evaluation of the primitive propositions.

Now we define satisfiability of the formulas from $For_{{\mathsf {ILUPP}}}$ in the worlds of ${\mathsf {ILUPP}}$-structures. As we mentioned in the introduction, for any set P of probability measures defined on given algebra H, the lower probability measure $P_\star$ and the upper probability measure $P^\star$ are defined by

• $P_\star (X)=\inf \{\mu (X)\mid \mu \in P\}$ and

• $P^\star (X)=\sup \{\mu (X)\mid \mu \in P\}$,

for every $X\in H$. It is easy to check that

$$\begin{aligned} P_\star (X)=1-P^\star (X^c), \end{aligned}$$

(1)

for every $X\in H$. In the context of the definition of an ${\mathsf {ILUPP}}$-structure, we will denote $P_\star (a,w)([\alpha ]^a_{M,w})=\inf \{\mu ([\alpha ]^a_{M,w})\mid \mu \in P(a,w)\}$ and $P^\star (a,w)([\alpha ]^a_{M,w})=\sup \{\mu ([\alpha ]^a_{M,w})\mid \mu \in P(a,w)\}$, where $[\alpha ]^a_{M,w}=\{u\in W(a,w)\mid M,u\models \alpha \}$.

Definition 3

(Satisfiability relation) For every ${\mathsf {ILUPP}}$ structure $M= \langle W,LUP,\upsilon \rangle$ and every $w\in W$, the satisfiability relation $\models$ fulfills the following conditions:

• if $p\in \mathcal L$, $M,w\models p$ iff $\upsilon (w)(p)=true$,

• $M,w\models \lnot \alpha$ iff it is not the case that $M,w\models \alpha$,

• $M,w\models \alpha \wedge \beta$ iff $M,w\models \alpha$ and $M,w\models \beta$,

• $M,w\models U^a_{\ge s}\alpha$ iff $P^\star (a,w)([\alpha ]^a_{M,w})\ge s$,

• $M,w\models L^a_{\ge s}\alpha$ iff $P_\star (a,w)([\alpha ]^a_{M,w})\ge s$.

We will omit M when it’s clear from context. Obviously, the operators indexed by groups satisfy the conditions:

• $M,w\models L^G_{\ge s}\alpha$ iff $M,w\models L^a_{\ge s}\alpha$ for all $a\in G$,

• $M,w\models U^G_{\ge s}\alpha$ iff $M,w\models U^a_{\ge s}\alpha$ for some $a\in G$.

Remark 1

Our logic has two types of basic operators for describing lower and upper probabilities. However, from the semantical point of view, lower probabilities can be inferred from upper probabilities, according to the Eq. (1). That fact will impact the presentation of the results in this paper. For example, in the proofs that use induction on the complexity of a formula to prove its semantical properties, the case when the formula is of the form $L^a_{\ge s}\alpha$ is an easy consequence of the case when we consider $U^a_{\ge s}\alpha$ (as an illustration, see the last paragraph of the proof of Theorem 2). Another consequence of the Eq. (1) is that the canonical model (Definition 1), used for the proof of completeness, can be defined using upper probabilities only.

It can be shown that satisfiability of the operators indexed by groups can be characterized by the set of probability measures that collect all the measures of individual members of the group. Indeed, if P(G, w) denotes the set $\bigcup _{a\in G} P(a,w)$, we can observe that

• $M,w\models U^G_{\ge s}\alpha$ iff $P^\star (G,w)([\alpha ]^a_{M,w})\ge s$,

• $M,w\models L^G_{\ge s}\alpha$ iff $P_\star (G,w)([\alpha ]^a_{M,w})\ge s$.

It is clear from these two conditions that the behavior of the operators indexed by groups is similar to behavior of operators for individual agents. Indeed, they also represent upper and lower probability of a set of probabilities.

Note that this semantical interpretation of satisfiability does not use the fact that G is finite, and it will also be applicable in Sect. 6, where we will consider infinite groups of agents.

The possible problem with Definition 3 is that it might happen that for some M, w , a and $\alpha$ the set $[\alpha ]^a_{M,w}$ doesn’t belong to W(a, w). For that reason, we will consider only so called measurable structures.

Definition 4

(Measurable structure) The structure M is measurable if for every $a\in \varSigma$ and every $w\in W$, $H(a,w)=\{[\alpha ]_w\mid \alpha \in For_{{\mathsf {ILUPP}}}\}$. The class of all measurable structures of the logic ${\mathsf {ILUPP}}$ will be denoted by ${\mathsf {ILUPP}}_{Meas}$.

Next we define satisfiability of an ${\mathsf {ILUPP}}$-formula.

Definition 5

(Satisfiability of a formula) A formula $\alpha \in For_{{\mathsf {ILUPP}}}$ is satisfiable if there is a world w in an ${\mathsf {ILUPP}}_{Meas}$-model M such that $w\models \alpha$; $\alpha$ is valid if it is satisfied in every world in every ${\mathsf {ILUPP}}_{Meas}$-model M. A set of formulas T is satisfiable if there is a world w in an ${\mathsf {ILUPP}}_{Meas}$-model M such that $w\models \alpha$ for every $\alpha \in T$.

3 Decidability of ${\mathsf {ILUPP}}$

In this section, we prove our main technical result. Recall the satisfiability problem: given an ${\mathsf {ILUPP}}$-formula $\alpha$, we want to determine if there exists a world w in an ${\mathsf {ILUPP}}_{Meas}$-model M such that $w\models \alpha$. Decidability for ${\mathsf {ILUPP}}$ will be proved in two steps:

• first, we show that an ${\mathsf {ILUPP}}$-formula is satisfiable iff it is satisfiable in a measurable structures with a finite number of worlds,

• second, we show that we can consider only finite measurable structures, i.e., measurable structure with finite number of worlds and with finite sets of probability measures in every world and for every agent, and

• third, we reduce the satisfiability problem in those finite models to a decidable linear programming problem.

In the first part of the proof, we will use the method of filtration (Hughes and Cresswell 1984). Like the previous papers on the logical formalization of upper and lower probabilities (Halpern and Pucella 2002; Savić et al. 2017a), we also use the characterization theorem by Anger and Lembcke (1985). It uses the notion of (n, k)-cover.

Definition 6

((n, k)-cover) A set A is said to be covered n times by a multiset $\{\{A_1,\ldots ,A_m\}\}$ of sets if every element of A appears in at least n sets from $A_1,\ldots ,A_m$, i.e., for all $x\in A$, there exists $i_1,\ldots ,i_n$ in $\{1,\ldots ,m\}$ such that for all $j\le n$, $x\in A_{i_j}$. An (n, k)-cover of (A, W) is a multiset $\{\{A_1,\ldots ,A_m\}\}$ that covers Wk times and covers A$n+k$ times.

Now we can state the characterization theorem.

Theorem 1

(Anger and Lembcke 1985) Let W be a set, H an algebra of subsets of W, and f a function $f:H\longrightarrow [0,1]$. There exists a set P of probability measures such that $f=P^\star$ iff f satisfies the following three properties:

• (1) $f(\emptyset )=0$,

• (2) $f(W)=1$,

• (3) for all natural numbers m, n, k and elements $A_1,\ldots ,A_m$ in H, if the multiset $\{\{A_1,\ldots ,A_m\}\}$ is an (n, k)-cover of (A, W), then $k+nf(A)\le \sum _{i=1}^m f(A_i)$.

Let $SF(\alpha )$ denote the set of all subformulas of a formula $\alpha$, i.e.

$$\begin{aligned} SF(\alpha )=\{\beta \ | \ \beta \ \mathrm{is}\, \mathrm{a }\, \mathrm{subformula} \, \mathrm{of }\, \alpha \}. \end{aligned}$$

Theorem 2

If a formula $\alpha$ is satisfiable, then it is satisfiable in an ${\mathsf {ILUPP}}_{Meas}$-model with at most $2^{|SF(\alpha )|}$ worlds.

Proof

Suppose that a formula $\alpha$ holds in some world of the model $M=\langle W,LUP,\upsilon \rangle$ and let $k=|SF(\alpha )|$. By $\approx$, we will denote an equivalence relation over $W^2$, such that

$$\begin{aligned} w\approx u\ \text {if and only if for every}\ \beta \in SF(\alpha ), w\models \beta \ \text {iff}\ u\models \beta . \end{aligned}$$

Since there are finitely many subformulas of $\alpha$, we know that the quotient set

$$\begin{aligned} W_{/\approx }=\{C_{w_i}\mid w_i\in W\} \end{aligned}$$

is finite, where

$$\begin{aligned} C_{w_i}=\{u\in W\mid u\approx w_i\} \end{aligned}$$

is the class of equivalence of $w_i$. More precsely,

$$\begin{aligned} |W_{/\approx }|\le 2^k. \end{aligned}$$

Next, from each class of equivalence $C_{w_i}$, we choose an element $w_i$.

Consider a tuple $\overline{M}=\langle \overline{W}, \overline{LUP}, \overline{\upsilon }\rangle$, where:

• $\overline{W}=\{w_1, w_2, \ldots \}$,

• For every a and for every $w_i$$\overline{LUP} (a,w_i)=\langle \overline{W} (a,w_i), \overline{H} (a,w_i), \overline{P}(a,w_i)\rangle$ is defined as follows:

  • $\overline{W} (a,w_i)=\{w_j\in \overline{W}\mid (\exists u\in C_{w_j})u\in W(a,w_i)\}$

  • $\overline{H} (a,w_i)=2^{\overline{W} (a,w_i)}$

  • $\overline{P}(a,w_i)$ is any set of finitely additive measures, such that for every $D\in \overline{H} (a,w_i)$, $\overline{P}^\star (a,w_i)(D)=P^\star (a,w_i)(\bigcup _{w_j\in D}(C_{w_j}\cap W(a,w_i)))$

• $\overline{\upsilon }(w_i)(p)=\upsilon (w_i)(p)$, for every primitive proposition $p\in \mathcal L$.

First, we have to prove that $\overline{P}^\star (a,w_i)$ satisfies the conditions (1)–(3) from Theorem 1, which will guarantee the existence of the sets $\overline{P}(a,w_i)$, for every agent a and each $w_i\in \overline{W}$.

• (1) $\overline{P}^\star (a,w_i)(\emptyset )=P^\star (a,w_i)(\bigcup _{w_j\in \emptyset }(C_{w_j}\cap W(a,w_i)))=P^\star (a,w_i)(\emptyset )=0$;

• (2) $\overline{P}^\star (a,w_i)(\overline{W} (a,w_i))=P^\star (a,w_i)(\bigcup _{w_j\in \overline{W}(a,w_i)}(C_{w_j}\cap W(a,w_i)))= P^\star (a,w_i) (W(a,w_i))=1$;

• (3) Let $\{\{D_1,\ldots ,D_m\}\}$ be an (n, k)-cover of $(D,\overline{W}(a,w_i))$. That means:

  • (i) every element from D appears in at least $n+k$ sets from $D_1,\ldots ,D_m$;

  • (ii) every element from $\overline{W}(a,w_i)$ appears in at least k sets from $D_1,\ldots ,D_m$.

  Therefore,

  • (iii) every element from $(\bigcup _{u\in D}(C_u\cap W(a,w_i))$ appears in at least $n+k$ sets from   $\bigcup _{u\in D_1}(C_u\cap W(a,w_i)),\ldots ,\bigcup _{u\in D_m}(C_u\cap W(a,w_i))$;

  • (iv) every element from $W(a,w_i)$ appears in at least k sets from $\bigcup _{u\in D_1}(C_u\cap W(a,w_i)),\ldots ,\bigcup _{u\in D_m}(C_u\cap W(a,w_i))$.

  Hence, by definition, we obtain that a multiset

  $$\begin{aligned} \left\{ \left\{ \bigcup _{u\in D_1}(C_u\cap W(a,w_i)),\ldots ,\bigcup _{u\in D_m}(C_u\cap W(a,w_i))\right\} \right\} \end{aligned}$$

  is an (n, k)-cover of

  $$\begin{aligned} \left( \bigcup _{u\in D}(C_u\cap W(a,w_i)), W(a,w_i)\right) . \end{aligned}$$

  Hence, using the fact that $P^\star (a,w_i)$ is an upper probability, from Theorem 1, we have that

  $$\begin{aligned} k+nP^\star (a,w_i)\left( \bigcup _{u\in D}(C_u\cap W(a,w_i))\right) \le \sum _{j=1}^m P^\star (a,w_i)\left( \bigcup _{u\in D_j}(C_u\cap W(a,w_i))\right) , \end{aligned}$$

  and therefore

  $$\begin{aligned} k+n\overline{P}^\star (a,w_i)(D)\le \sum _{j=1}^m\overline{P}^\star (a,w_i)(D_j). \end{aligned}$$

Using induction on the complexity of a formula from the set $SF(\alpha )$, we can prove that for every $w\in \overline{W}$ and every $\beta \in SF(\alpha )$,

$$\begin{aligned} M,w\models \beta \quad \text {if and only if}\quad \overline{M},w\models \beta . \end{aligned}$$

If a formula is a propositional letter or obtained using Boolean connectives, the claim is trivial. So, let us consider the case when $\beta = U_{\ge s}^a\gamma$:

$$\begin{aligned} M,w\models U_{\ge s}^a\gamma \quad \quad&\text {iff} \\ P^\star (a,w)(\{u\in W(a,w)\mid M,u\models \gamma \})\ge s\quad \quad&\text {iff} \\ P^\star (a,w)\left( \bigcup \limits _{M,u\models \gamma }C_u\cap W(a,w)\right) \ge s\quad \quad&\text {iff (ind. hyp.)} \\ \overline{P}^\star (a,w)(\{u\in \overline{W}^\star (a,w)\mid \overline{M},u\models \gamma \})\ge s\quad \quad&\text {iff} \\ \overline{M},w\models U_{\ge s}^a\gamma .\quad \quad&\end{aligned}$$

At the end, let $\beta = L_{\ge s}^a\gamma$:

$$\begin{aligned} M,w\models L_{\ge s}^a\gamma \quad \quad&\text {iff} \\ P_\star (a,w)(\{u\in W(a,w)\mid M,u\models \gamma \})\ge s\quad \quad&\text {iff (Eq.~(1))} \\ 1-P^\star (a,w)(\{u\in W(a,w)\mid M,u\models \lnot \gamma \})\ge s\quad \quad&\text {iff } \\ 1-P^\star (a,w)\left( \bigcup \limits _{M,u\models \lnot \gamma }C_u\cap W(a,w)\right) \ge s\quad \quad&\text {iff (ind. hyp.)} \\ \overline{P}^\star (a,w)(\{u\in \overline{W}^\star (a,w)\mid \overline{M},u\models \lnot \gamma \})\le 1-s\quad \quad&\text {iff} \\ \overline{M},w\models U_{\le 1-s}^a\lnot \gamma \quad \quad&\text {iff} \\ \overline{M},w\models L_{\ge s}^a\gamma .\quad \quad&\end{aligned}$$

$\square$

In the second part of the proof, we use the following result of Halpern and Pucella (2002).

Theorem 3

(Halpern and Pucella 2002) Let P be a set of probability measures defined on an algebra H over a finite set W. Then there exists a set $P'$ of probability measures such that, for each $X\in H$, $P^*(X)=(P')^*(X)$. Moreover, there is a probability measure $\mu _X\in P'$ such that

$$\begin{aligned} \mu _X(X)=P^*(X). \end{aligned}$$

As a direct consequence of Theorems 2 and 3, we obtain the following result.

Lemma 1

If a formula $\alpha$ is satisfiable, then it is satisfiable in an ${\mathsf {ILUPP}}_{Meas}$-model with at most $2^{|SF(\alpha )|}$ worlds and for every agent $a\in \varSigma$ and every $w\in W$, $H(a,w)=2^{W(a,w)}$ and

$$\begin{aligned} |P(a,w)|= |H(a,w)|. \end{aligned}$$

Furthermore, for each $X\in H(a,w)$, there exists a $\mu _X\in P(a,w)$ such that

$$\begin{aligned} \mu _X(a,w)(X)=P^*(a,w)(X). \end{aligned}$$

This lemma plays an important role in our proof of decidability. In the proof we will use the following notation: If $\alpha$ is an arbitrary formula, then

$$\begin{aligned} SF(\alpha )=\{\beta _1,\ldots ,\beta _k\}. \end{aligned}$$

In every $w\in W$, exactly one of the formulas of the following form:

$$\begin{aligned} \pm \beta _1\wedge \cdots \wedge \pm \beta _k \end{aligned}$$

(2)

holds, where $\pm \beta _i$ denotes $\beta _i$ or $\lnot \beta _i$. We will call that formula the characteristic formula for a world w. Also by $\beta \in (\alpha _j)^+$ we will denote that $\beta$ is a conjunct in $\alpha _j$ and by $\beta \in (\alpha _j)^-$ we will denote that $\lnot \beta$ is a conjunct in $\alpha _j$.

Theorem 4

Satisfiability problem for ${\mathsf {ILUPP}}_{Meas}$ is decidable.

Proof

Let $M=\langle W,LUP,\upsilon \rangle$ be an ${\mathsf {ILUPP}}_{Meas}$-model and $\alpha$ an arbitrary formula. If k is the cardinality of the set $SF(\alpha )$, by Lemma 1 we know that there exists an ${\mathsf {ILUPP}}_{Meas}$-model $\overline{M}$ with

• (1) at most $2^k$ worlds and

• (2) at most $2^{2^k}$ probabilistic measures (for any agent and any world) such that for each measurable set X, there exists a probabilistic measure $\mu _X$ with

  $$\begin{aligned} \mu _X(a,w)(X)=P^*(a,w)(X), \end{aligned}$$

such that $\alpha$ holds in some world of the model $\overline{M}$ iff $\alpha$ holds in some world of a model M. Let us denote by ${\mathsf {ILUPP}}_{Meas}(k)$ the set of all measurable models which satisfy the conditions (1) and (2). Clearly, in order to check if $\alpha$ is satisfiable, it is sufficient to check if $\alpha$ is satisfied in a model from ${\mathsf {ILUPP}}_{Meas}(k)$.

For every $l\le 2^k$, we will consider models with

• l worlds, $w_1,\ldots , w_l$, and

• for every agent a and every world w, sets of probability measures P(a, w), such that $|P(a,w)|=2^{|W(a,w)|}$, for every $W(a,w)\subseteq \{w_1,\ldots w_l\}$.

Recall that in each of these worlds, exactly one characteristic formula holds. Thus, without loss of generality, in this proof we identify worlds with their corresponding characteristic formulas. We will denote by $\alpha _i$ the characteristic formula for a world $w_i$.

Note that it is not the case that any formula of the form (2) is a characteristic formula of some world, since it might be propositionally inconsistent. We can formally check if the formula $\alpha _i$ of the form (2) is propositionally consistent using the following test:

• (a) In $\alpha _i$ we replace every occurrence of a formula starting with a probabilistic operator with an atomic proposition (all the occurrences of the same formula are assigned the same atomic proposition). Then we obtain a propositional formula, $\alpha _i'$. Using any algorithm for propositional satisfiability we check whether $\alpha _i'$ is satisfiable. If $\alpha _i'$ passes the test, then $\alpha _i$ is consistent.

We check if $\alpha$ is satisfied in a model from ${\mathsf {ILUPP}}_{Meas}(k)$ using the following procedure:

• (1) The procedure sets:

  • The number of worlds l such that $1\le l\le 2^k$ (i.e., $W=\{w_1,\ldots ,w_l\}$);

  • l formulas $\alpha _1,\ldots ,\alpha _l$ (not necessarily different) of the form

    $$\begin{aligned} \pm \beta _1\wedge \cdots \wedge \pm \beta _k, \end{aligned}$$

    where $SF(\alpha )=\{\beta _1,\ldots ,\beta _k\}$ such each formula passes the consistency test (a), and such that $\alpha$ is a conjunct of at least one $\alpha _i$;

  • an arbitrary subset of worlds $W(a,w_i)\subseteq \{w_1,\ldots w_l\}$, for every agent a and every $w_i\in W$;

• (2) Using the test described below, the procedure checks if there is a model $\overline{M}=\langle W,LUP,\upsilon \rangle$ of $\alpha$ from ${\mathsf {ILUPP}}_{Meas}(k)$ with the set of worlds $W=\{w_1,\ldots ,w_l\}$ and their corresponding characteristic formulas $\alpha _1,\ldots ,\alpha _l$, and such that LUP contains all $W(a,w_i)$’s

• (3) If the test succeeds, the formula $\alpha$ is satisfiable, and the procedure terminates, otherwise procedure sets different values at step (1) and repeats the test.

• (4) If the test fails for all the possibilities for l, $\alpha _1,\ldots ,\alpha _l$ and $W(a,w_i)$’s (for every a and $w_i$), the formula $\alpha$ is not satisfiable.

Now it remains to describe the test (from step 2) which, for given

• number of worlds l ($1\le l\le 2^k$),

• characteristic formulas $\alpha _1,\ldots ,\alpha _l$ of l worlds, and

• sets of worlds $W(a,w_i)\subseteq \{w_1,\ldots w_l\}$

checks if there is a model of $\alpha$ from ${\mathsf {ILUPP}}_{Meas}(k)$, where $W=\{w_1,\ldots w_l\}$, with those characteristic formulas of worlds and those $W(a,w_i)$’s in LUP. In the test we do not determine probability values precisely; we simply check if there are probability measures such that the probabilistic constraints are satisfied in corresponding worlds.

The test translates the problem to the problem of satisfiability of a set of linear equations and inequalities. Since the models from ${\mathsf {ILUPP}}_{Meas}(k)$ have finite sets of worlds, all the subsets of $W(a,w_i)$ will be measurable. Also, note that every $\mu (a, w_i)\in P(a,w_i)$ is of the form $\mu _X$ (recall that $\mu _X$ is such that $\mu _X(a,w)(X)=P^*(a,w)(X)$). The test considers the following set of linear equations and inequalities:

• (1) $y_{w_i,w_j}^{X,a}\ge 0$, for each $\mu _X (a, w_i)\in P(a,w_i)$ (i.e., for every $X\subseteq W(a,w_i)$) and $j=1,\ldots , l$;

• (2) $\sum \nolimits _{w_j\in W(a,w_i)} y_{w_i,w_j}^{X,a}=1$, for every $\mu (a,w_i)\in P(a,w_i)$ (i.e., for every $X\subseteq W(a,w_i)$);

• (3) $\sum \nolimits _{w_j\in X} y_{w_i,w_j}^{X,a}\ge \sum \nolimits _{w_j\in X} y_{w_i,w_j}^{Y,a}$, for every $X,Y\subseteq W(a,w_i)$;

• (4) $\sum \nolimits _{w_j:\beta \in (\alpha _j)^+}y_{w_i,w_j}^{X,a}\ge s$, if $U_{\ge s}^a\beta \in \alpha _i$,   $X=\{w_j\mid \beta \in (\alpha _j)^+\};$

• (5) $\sum \nolimits _{w_j:\beta \in (\alpha _j)^+}y_{w_i,w_j}^{X,a}< s$, if $\lnot U_{\ge s}^a\beta \in \alpha _i$,   $X=\{w_j\mid \beta \in (\alpha _j)^+\}$;

• (6) $\sum \nolimits _{w_j:\beta \in (\alpha _j)^-}y_{w_i,w_j}^{X,a}\le 1-s$, if $L_{\ge s}^a\beta \in \alpha _i$,   $X=\{w_j\mid \beta \in (\alpha _j)^-\}$;

• (7) $\sum \nolimits _{w_j:\beta \in (\alpha _j)^-}y_{w_i,w_j}^{X,a}> 1-s$, if $\lnot L_{\ge s}^a\beta \in \alpha _i$, $X=\{w_j\mid \beta \in (\alpha _j)^-\}$,

where $y_{w_i,w_j}^{X,a}$ represents $\mu _X (a,w_i)(\{w_j\})$.

• The first inequality states that all the measures must be nonnegative.

• The second equality assures that the probability of the set of all possible worlds has to be equal to 1.

• The third inequality corresponds to the fact that $\mu _X(a,w)(X)=P^*(a,w)(X)$ and therefore

  $$\begin{aligned} \mu _X(a,w)(X)\ge \mu (a,w)(X),\ \text {for all}\ \mu (a,w)\in P(a,w). \end{aligned}$$

• For the fourth and fifth inequality, note that if $X=\{w_j\mid \beta \in (\alpha _j)^+\}$

  $$\begin{aligned} \sum \limits _{w_j:\beta \in (\alpha _j)^+}\mu _{X} (a,w_i)(\{w_j\})=P^* (a,w_i)([\beta ]_{w_i}^a), \end{aligned}$$

  so these inequalities reflect the appropriate constraints.

• In order to understand sixth and seventh inequality, first recall the equality connecting upper and lower probabilty:

  $$\begin{aligned} P^*([\lnot \beta ]_{w_i}^a)=1-P_*([\beta ]_{w_i}^a). \end{aligned}$$

  Next, note that if $X=\{w_j\mid \beta \in (\alpha _j)^-\}$

  $$\begin{aligned} \sum \limits _{w_j:\beta \in (\alpha _j)^-}\mu _{X} (a,w_i)(\{w_j\})=P^* (a,w_i)([\lnot \beta ]_{w_i}^a). \end{aligned}$$

  Consequently, if

  $$\begin{aligned} P_*([\beta ]_{w_i}^a)\ge s, \end{aligned}$$

  then

  $$\begin{aligned} P^*([\lnot \beta ]_{w_i}^a)\le 1-s, \end{aligned}$$

  and similarly for the case when $P_*([\beta ]_{w_i}^a)< s$.

The equations and inequalities 1–7 form a finite system of linear equalities and inequalities and it is well known that solving this system is decidable. If this system has a solution, then there exists a probabilistic space in each world and for every agent. Indeed, it can be defined in the following way:

$$\begin{aligned} \mu _X (a,w_i)(S)= \sum _{w_j\in S}y_{w_i,w_j}^{X,a} \end{aligned}$$

for every $S\subseteq W(a,w_i)$. The opposite also holds: if the system doesn’t have solutions, then the probabilistic spaces (in each world and for every agent) cannot exist. Indeed, otherwise we could use the probability measures $\mu _X (a,w_i)$ to define the solution of the system in the following way: $y_{w_i,w_j}^{X,a}=\mu _X (a,w_i)(\{w_j\})$.

Also note that because of the condition (a) above, we know that a valuation can be defined. Namely, there are no classical propositional contradictions in characteristic formulas and therefore there exists a valuation that gives adequate truth values to the propositional letters that appear in formulas and for all the other variables we can set arbitrary truth value, e.g. $\bot$. Moreover, in every world w of the model, the characteristic formula of the world holds in w. Since $\alpha$ is a conjunct of at least one of the corresponding characteristic formulas, we have that $\alpha$ is satisfiable.

Note that in the previously described method we consider only finitely many systems of linear equation and inequalities. Therefore, the satisfiability problem is decidable. $\square$

Furthermore, $\alpha$ is valid if and only if $\lnot \alpha$ is not ${\mathsf {ILUPP}}_{Meas}$-satisfiable, so we have also that problem of a validity of a formula is decidable as well.

4 A Complete Axiomatization of ${\mathsf {ILUPP}}$

Having settled the decidability issue for the logic ${\mathsf {ILUPP}}$, we turn to the problem of developing an axiomatic system for the logic ${\mathsf {ILUPP}}$. That system will be denoted by $Ax_{{\mathsf {ILUPP}}}$.

We start with the observation that, like any other real-valued probabilistic logic, ${\mathsf {ILUPP}}$ is not compact. Indeed, consider the set of formulas $T=\{\lnot U_{=0}\alpha \}\cup \{U_{<\frac{1}{n}}\alpha \mid n$ is a positive integer $\}.$ Obviously, every finite subset of T is ${\mathsf {ILUPP}}_{Meas}$-satisfiable, but the set T is not. Consequently, any finitary axiomatic system would be incomplete (van der Hoek 1997). In order to achieve completeness, we use two infinitary rules of inference, with countably many premises and one conclusion.

In order to axiomatize upper and lower probabilities, we need to completely characterize them with a small number of properties. There are many complete characterizations in the literature, and the earliest appears to be by Lorentz (1952). We will use Theorem 1 from the previous section.

For the logic ${\mathsf {ILUPP}}$, we use the axiomatic system for the logic ${\mathsf {LUPP}}$ from Savić et al. (2017a). We only need to modify the form of the axioms due to presence of multiple agents. Apart from that, it should be also mentioned that the instances of axioms are different, since in Savić et al. (2017a) the operators of upper and lower probability are applied to classical formulas only, while here their nesting is allowed.

Axiom schemes

• (A1) all instances of the classical propositional tautologies

• (A2) $U_{\le 1}^a\alpha \wedge L_{\le 1}^a\alpha$

• (A3) $U_{\le r}^a\alpha \rightarrow U_{<s}^a\alpha$, $s>r$

• (A4) $U_{<s}^a\alpha \rightarrow U_{\le s}^a\alpha$

• (A5) $(U_{\le r_1}^a\alpha _1\wedge \cdots \wedge U_{\le r_m}^a\alpha _m)\rightarrow U_{\le r}^a\alpha$, if $\alpha \rightarrow \bigvee _{J\subseteq \{1,\ldots ,m\}, |J|=k+n}\bigwedge _{j\in J}\alpha _j$ and $\bigvee _{J\subseteq \{1,\ldots ,m\}, |J|=k}\bigwedge _{j\in J}\alpha _j$ are instances of the classical propositional tautologies, where $r=\frac{\sum _{i=1}^m r_i-k}{n}$, $n\ne 0$

• (A6) $\lnot (U_{\le r_1}^a\alpha _1\wedge \cdots \wedge U_{\le r_m}^a\alpha _m)$, if $\bigvee _{J\subseteq \{1,\ldots ,m\}, |J|=k}\bigwedge _{j\in J}\alpha _j$ is an instance of the classical propositional tautology and $\sum _{i=1}^m r_i<k$

• (A7) $L_{=1}^a (\alpha \rightarrow \beta )\rightarrow (U_{\ge s}^a\alpha \rightarrow U_{\ge s}^a\beta )$

Inference Rules

• (1) From $\alpha$ and $\alpha \rightarrow \beta$ infer $\beta$

• (2) From $\alpha$ infer $L_{\ge 1}^a\alpha$

• (3) From the set of premises

  $$\begin{aligned} \left\{ \alpha \rightarrow U_{\ge s-\frac{1}{k}}^a\beta \mid k\in \mathbb {N}, \ge \frac{1}{s}\right\} \end{aligned}$$

  infer $\alpha \rightarrow U_{\ge s}^a\beta$

• (4) From the set of premises

  $$\begin{aligned} \left\{ \alpha \rightarrow L_{\ge s-\frac{1}{k}}^a\beta \mid k\in \mathbb {N},k\ge \frac{1}{s}\right\} \end{aligned}$$

  infer $\alpha \rightarrow L_{\ge s}^a\beta$.

The axioms A5 and A6 together capture the third condition from the Theorem 1. Indeed, as explained in Savić et al. (2017a), “$\{\{A_1,\ldots ,A_m\}\}$ covers a set An times” can be formally written as $A\subseteq \bigcup _{J\subseteq \{1,\ldots ,m\},|J|=n}\bigcap _{j\in J}A_j.$ Thus, the condition that $\alpha \rightarrow \bigvee _{J\subseteq \{1,\ldots ,m\}, |J|=k+n}\bigwedge _{j\in J}\alpha _j$ is an instance of a propositional tautology ensures that $[\alpha ]$ is covered $n+k$ times by a multiset $\{\{[\alpha _1],\ldots ,[\alpha _m]\}\}$, while the condition that $\bigvee _{J\subseteq \{1,\ldots ,m\}, |J|=k}\bigwedge _{j\in J}\alpha _j$ is a propositional tautology gives us that $W=[\top ]$ is covered k times by a multiset $\{\{[\alpha _1],\ldots ,[\alpha _m]\}\}$.

The rules (3) and (4) are infinitary rules of inference and intuitively state that if an upper/lower probability is arbitrary close to a rational number s then it is at least s.

Now we define some proof theoretical notions.

• $\vdash \alpha$ ($\alpha$ is a theorem) iff there is an at most denumerable sequence of formulas $\alpha _1,\alpha _2,\ldots ,\alpha$, such that every $\alpha _i$ is an axiom or it is derived from the preceding formulas by an inference rule;

• $T\vdash \alpha$ ($\alpha$ is derivable from T) if there is an at most denumerable sequence of formulas $\alpha _1,\alpha _2,\ldots ,\alpha$, such that every $\alpha _i$ is an axiom or a formula from the set T, or it is derived from the preceding formulas by an inference rule, with the exception that Inference Rule 2 can be applied only to the theorems;

• T is consistent if there is at least one formula $\alpha \in For_{{\mathsf {ILUPP}}}$ that is not deducible from T, otherwise T is inconsistent;

• T is maximal consistent set if it is consistent and for every $\alpha \in For_{{\mathsf {ILUPP}}}$, either $\alpha \in T$ or $\lnot \alpha \in T$;

• T is deductively closed if for every $\alpha \in For_{{\mathsf {ILUPP}}}$, if $T\vdash \alpha$, then $\alpha \in T$.

Note that T is inconsistent iff $T\vdash \bot$. Also, it is easy to check that every maximal consistent set is deductively closed.

Due to similarity between this axiomatic system and the axiomatization from Savić et al. (2017a), many parts of the proof of completeness theorem are similar to the proofs that we already presented in Savić et al. (2017a), but there are also several differences, since the sets of formulas are not the same and the models are different. In the rest of this section, we present novel proofs and also reuse some ideas from Savić et al. (2017a) for readability, while we omit some parts that are identical to the proofs from Savić et al. (2017a).

Theorem 5

(Deduction Theorem) Let $\alpha ,\beta \in For_{{\mathsf {ILUPP}}}$ and T a set of formulae. Then $T,\alpha \vdash \beta$ implies $T\vdash \alpha \rightarrow \beta .$

Proof

By transfinite induction on the length of the proof of $\beta$. The cases when $\vdash \beta$, $\beta =\alpha$ or $\beta$ is obtained by modus ponens are standard. So, let $\beta =L^a_{\ge 1}\gamma$ be obtained from $T\cup \{\alpha \}$ by an application of Rule (2). Since the application of the inference Rule (2) is restricted to theorems only, we have:

• (1) $\vdash \gamma$

• (2) $T\vdash \gamma$

• (3) $T\vdash L^a_{\ge 1}\gamma$   by Rule (2)

• (4) $T\vdash L^a_{\ge 1}\gamma \rightarrow (\alpha \rightarrow L^a_{\ge 1}\gamma )$   propositional reasoning

• (5) $T\vdash \alpha \rightarrow L^a_{\ge 1}\gamma$   by Rule (1).

Now, let us consider the case where $\beta = \beta _1\rightarrow L^a_{\ge s}\gamma$ is obtained from $T\cup \{\alpha \}$ by an application of Rule (4). Then:

• (1) $T,\alpha \vdash \beta _1\rightarrow L^a_{\ge s-\frac{1}{k}}\gamma$, for all $k\ge \frac{1}{s}$

• (2) $T\vdash \alpha \rightarrow (\beta _1\rightarrow L^a_{\ge s-\frac{1}{k}}\gamma )$, by the induction hypothesis

• (3) $T\vdash (\alpha \wedge \beta _1)\rightarrow L^a_{\ge s-\frac{1}{k}}\gamma$, propositional reasoning

• (4) $T\vdash (\alpha \wedge \beta _1)\rightarrow L^a_{\ge s}\gamma$, by Rule (4)

• (5) $T\vdash \alpha \rightarrow \beta$, propositional reasoning.

Finally, the case where $\beta = \beta _1\rightarrow U^a_{\ge s}\gamma$ is obtained from $T\cup \{\alpha \}$ by an application of Rule (3) is analogous.

It is easy to check that the axiomatic system $Ax_{{\mathsf {ILUPP}}}$ is sound with respect to the class of ${\mathsf {ILUPP}}_{Meas}$-models.

We prove that the axiomatization $Ax_{{\mathsf {ILUPP}}}$ is complete, using a Henkin-like construction. Due to the presence of infinitary rules, the standard completion technique (Lindenbaum’s theorem) has to be modified in the following way: if the current theory is inconsistent with the current formula and that formula can be derived by one of infinitary inference rules, than one of the premises must be blocked (see the proof of Theorem 6).

Definition 1

(Canonical Model) Canonical model $M_{Can}=\langle W,LUP,\upsilon \rangle$ where:

• $W=\{w \mid w$ is a maximal consistent set of formulas$\}$,

• for every world w and every propositional letter p, $\upsilon (w)(p)=true$ iff $p\in w$,

• for every $a\in \varSigma$ and $w\in W$, $LUP(a,w)=\langle W(a,w),H(a,w),P(a,w)\rangle$ is defined in the following way:

  • $W(a,w)=W$,

  • $H(a,w)=\{\{u\mid u\in W(a,w),\alpha \in u\}\mid \alpha \in For_{{\mathsf {ILUPP}}}\}$,

  • P(a, w) is any set of probability measures such that $P^\star (a,w)(\{u\mid u\in W(a,w),\alpha \in u\})=\sup \{s\mid U_{\ge s}\alpha \in w\}$.

Lemma 2

For every $a \in \varSigma$, every $w\in W$ and every formula $\alpha$,

$$\begin{aligned} \{u\mid u\in W(a,w),\alpha \in u\}=[\alpha ]^a_w. \end{aligned}$$

Proof

We prove the statement by proving that $\alpha \in u$ iff $u\models \alpha$ by induction on the length of $\alpha$. If $\alpha =p$ the claim follows by definition of the canonical model. Cases when $\alpha =\lnot \beta$ or $\alpha =\beta \wedge \gamma$ are trivial. Let us consider the case when $\alpha =U^a_{\ge s}\beta$. If $\alpha \in u$ then

$$\begin{aligned} \sup \{r\mid U^a_{\ge r}\beta \in u\}= P^\star (a,u)(\{v\mid v\in W(a,u),\beta \in v\})\ge s, \end{aligned}$$

and so $u\models \alpha$. Now, suppose that $u \models U^a_{\ge s}\beta$, i.e.

$$\begin{aligned}\sup \{r\mid U^a_{\ge r}\beta \in u\}\ge s.\end{aligned}$$

• (a) If $\sup \{r\mid U^a_{\ge r}\beta \in u\}>s$, then by the properties of supremum and monotonicity of $P^\star (a,u)$ we obtain $U_{\ge s}\alpha \in u$.

• (b) If $\sup \{r\mid U^a_{\ge r}\beta \in u\}=s$, then, as a direct consequence of inference Rule 3, we have that $U^a_{\ge s}\alpha \in u$.

The case when $\alpha =L^a_{\ge s}\beta$ can be proved using Eq. (1). $\square$

Lemma 3

$M_{Can}$ is a well defined measurable structure.

Proof

From the Lemma 2 and the fact that $P^\star (a,w)$ is an upper probability measure [(the proof that $P^\star (a,w)$ is an upper probability measure follows from Theorem 1 and the axioms A5 and A6 and it is essentially the same as the proof of the Lemma 3 in Savić et al. (2017a)] we obtain that $M_{Can}$ is a well defined measurable structure. $\square$

Theorem 6

(Lindenbaum’s theorem) Every consistent set of formulas can be extended to a maximal consistent set.

We assume an enumeration $\alpha _0,\alpha _1,\ldots$ of all formulas and define the chain of sets $T_i$, $i=0,1,2,\ldots$ and the set $T^\star$ in the following way:

• (1) $T_0=T$,

• (2) for every $i\ge 0$,

  • (a) if $T_i\cup \{\alpha _i\}$ is consistent, then $T_{i+1}=T_i\cup \{\alpha _i\}$, otherwise

  • (b) if $\alpha _i$ is of the form $\beta \rightarrow U_{\ge s}^a\alpha$, then $T_{i+1}=T_i\cup \{\lnot \alpha _i,\beta \rightarrow \lnot U_{\ge s-\frac{1}{n}}^a\alpha \}$, for some positive integer n, so that $T_{i+1}$ is consistent, otherwise

  • (c) if $\alpha _i$ is of the form $\beta \rightarrow L_{\ge s}^a\alpha$, then $T_{i+1}=T_i\cup \{\lnot \alpha _i,\beta \rightarrow \lnot L_{\ge s-\frac{1}{n}}^a\alpha \}$, for some positive integer n, so that $T_{i+1}$ is consistent, otherwise

  • (d) $T_{i+1}=T_i\cup \{\lnot \alpha _i\}$.

• (3) $T^\star =\bigcup _{i=0}^\infty T_i$.

The proof that $T^\star$ is a maximal consistent set is based on the following observations:

(i):

Natural numbers (n), from the steps 2(b) and 2(c) of the construction exist; this follows from the Theorem 5.

(ii):

Each $T_i$ is consistent, by construction.

(iii):

$T^\star$ does not contain all the formulas, by construction, using the fact that all $T_i$’s are consistent.

(iv):

For every formula $\alpha$, either $\alpha \in T^\star$ or $\lnot \alpha \in T^\star$, by construction [(steps (1) and (2)].

(v):

For every formula $\alpha$, if $T^\star \vdash \alpha$, then $\alpha \in T^\star$. The proof of this fact is by the induction on the length of the inference. Suppose that the sequence $\gamma _1,\gamma _2,\ldots ,\alpha$ is the proof of $\alpha$ from $T^\star$. We show only the case when the sequence is countably infinite. The idea is to prove that, for every i, if $\gamma _i$ is obtained by an application of an arbitrary inference rule, and all the premises belong to $T^\star$, then, also $\gamma _i\in T^\star$. Let us consider the infinitary Rule 4. Let $\gamma _i=\beta \rightarrow L^a_{\ge s}\alpha$ be obtained from the set of premises $\{\gamma _i^k= \beta \rightarrow L^a_{\ge s_k}\alpha \mid s_k=s-\frac{1}{k}, k>\frac{1}{s}, k\in \mathbb {N}\}$. By the induction hypothesis, we have that $\gamma _i^k\in T^\star$, for every k. If $\gamma _i\notin T^\star$, by step (3)(b) of the construction, there are some l and j so that

$$\begin{aligned} \lnot (\beta \rightarrow L^a_{\ge s}\alpha ),\ \beta \rightarrow \lnot L^a_{\ge s-\frac{1}{l}}\alpha \in T_j. \end{aligned}$$

Thus, we have that for some $j'\ge j$:

–:

$\beta \wedge \lnot L^a_{\ge s}\alpha \in T_{j'}$,

–:

$\beta \in T_{j'}$,

–:

$\lnot L^a_{\ge s-\frac{1}{l}}\alpha$, $L^a_{\ge s-\frac{1}{l}}\alpha \in T_{j'}$.

Contradiction with the consistency of a set $T_{j'}$. Similarly can be proved for the Inference Rule (3) and all the other cases are easier.

(vi):

Step (iv) guarantees that $T^\star$ is maximal and from (v) and (iii) we get that $T^\star$ is a deductively closed set that does not contain all the formulas, hence consistent. $\square$

Theorem 7

(Strong completeness) If $\alpha$ is a formula, and T is a set of formulas of the logic ${\mathsf {ILUPP}}$, then $T\vdash \alpha$ iff $T\models \alpha$.

Sketch of the proof

First we point out that the theorem follows from soundness of the axiomatic system $Ax_{{\mathsf {ILUPP}}}$, and the following usual formulation of strong completeness:

• Every consistent set of formulas T is satisfiable.

• Recall that we extended T to the maximal consistent set $T^\star$. We showed that for every formula $\alpha$, and every $w\in W$, $w\models \alpha$ iff $\alpha \in w$. Since $T^\star \in W$, we obtain $M_{Can}, T^\star \models T$.$\square$

5 The First-Order Logic ${\mathsf {ILUPFO}}$

In this section we briefly discuss the first-order case avoiding repetition of technical details mentioned for the propositional case.

The language of the logic ${\mathsf {ILUPFO}}$ consists of a denumerable set of variables $Var=\{x,y,z,\ldots \}$, classical propositional connectives, universal quantifier $\forall$, for every integer $k\ge 0$, denumerably many function symbols $F_0^k, F_1^k, \ldots$ of arity k, denumerably many relation symbols $P_0^k, P_1^k, \ldots$ of arity k, the list of upper probability operators $U_{\ge s}^a$ and the list of lower probability operators $L_{\ge s}^a$. Functions of arity 0 will be called constants. Terms are defined as usual, as well as the notion of term that is free for a variable.

The set of formulas is the smallest set containing atomic formulas and that is closed under following formation rules: if $\alpha ,\beta$ are formulas, then $L_{\ge s}^a\alpha$, $U_{\ge s}^a\alpha$, $\lnot \alpha$, $\alpha \wedge \beta$, $(\forall x)\alpha$ are formulas as well.

An ${\mathsf {ILUPFO}}$-structure is a tuple $\mathcal M=\langle W,D,I,LUP\rangle$, where:

• W and LUP are defined as in the propositional case,

• D associates a non-empty domain D(w) with every world $w\in W$,

• I associates an interpretation I(w) with every world $w\in W$ such that:

  • $I(w)(F_i^k):D(w)^k\rightarrow D(w)$, for all i and k,

  • $I(w)(P_i^k)\subseteq D(w)^k$, for all i and k.

Let $\mathcal M=\langle W,D,I,LUP\rangle$ be an ${\mathsf {ILUPFO}}$-structure. A variable valuation$\upsilon$ assigns to every variable some element of the corresponding domain to every world $w\in W$, i.e. $\upsilon (w)(x)\in D(w)$. For $\upsilon$, $w\in W$ and $d\in D(w)$ we define $\upsilon _w [d/x]$ is a valuation same as $\upsilon$ except that $\upsilon _w [d/x](w)(x)=d$. The value of a termt, denoted by $I(w)(t)_\upsilon$ is defined as follows:

• if t is a variable x, then $I(w)(x)_\upsilon =\upsilon (w)(x)$, and

• if $t=F_i^m(t_1,\ldots ,t_m)$, then

  $$\begin{aligned} I(w)(t)_\upsilon =I(w)(F_i^m)(I(w)(t_1)_\upsilon ,\ldots ,I(w)(t_m)_\upsilon ). \end{aligned}$$

We consider a class of ${\mathsf {ILUPFO}}$ models that satisfy:

• all the worlds from a model have the same domain, i.e., for all $v,w\in W$, $D(v)=D(w)$,

• the terms are rigid, i.e., for every model their meanings are the same in all the worlds.

The truth value of a formula $\alpha$ in a world $w\in W$ of a model $\mathcal M=\langle W,D,I,LUP\rangle$ for a given valuation $\upsilon$, denoted by $I(w)(\alpha )_\upsilon$ is defined as follows:

• if $\alpha =P_i^m(t_1,\ldots ,t_m)$, then $I(w)(\alpha )_\upsilon =true$ if $\langle I(w)(t_1)_\upsilon ,\ldots ,I(w)(t_m)_\upsilon \rangle \in I(w)(P_i^m)$, otherwise $I(w)(\alpha )_\upsilon =false$,

• if $\alpha =\lnot \beta$, then $I(w)(\alpha )_\upsilon =true$ if $I(w)(\beta )_\upsilon =false$, otherwise $I(w)(\alpha )_\upsilon =false$,

• if $\alpha =\beta \wedge \gamma$, then $I(w)(\alpha )_\upsilon =true$ if $I(w)(\beta )_\upsilon =true$ and $I(w)(\gamma )_\upsilon =true$,

• if $\alpha =U_{\ge s}^a\beta$, then $I(w)(\alpha )_\upsilon =true$ if $P^\star (w,a)(\{u\in W(w,a)\mid I(u)(\beta )_\upsilon =true\})\ge s$, otherwise $I(w)(\alpha )_\upsilon =false$,

• if $\alpha =L_{\ge s}^a\beta$, then $I(w)(\alpha )_\upsilon =true$ if $P_\star (w,a)(\{u\in W(w,a)\mid I(u)(\beta )_\upsilon =true\})\ge s$, otherwise $I(w)(\alpha )_\upsilon =false$,

• if $\alpha =(\forall x)\beta$, then $I(w)(\alpha )_\upsilon =true$ if for every $d\in D(w)$, $I(w)(\beta )_{\upsilon _w[d/x]}=true$, otherwise $I(w)(\alpha )_\upsilon =false$.

A formula $\alpha$ holds in a world w from a model $\mathcal M=\langle W,D,I,LUP\rangle$, denoted by $\mathcal M,w\models \alpha$, if for every valuation $\upsilon$, $I(w)(\alpha )_\upsilon =true$. If $d\in D(w)$, we use $\mathcal M,w\models \alpha (d)$ to denote that $I(w)(\alpha (x))_{\upsilon _w[d/x]}=true$, for every valuation $\upsilon$.

A sentence $\alpha$ is satisfiable if there is a world w in an ${\mathsf {ILUPFO}}$-model $\mathcal M$ such that $\mathcal M,w\models \alpha$. A sentence $\alpha$ is valid if it is satisfied in every world in every ${\mathsf {ILUPFO}}$-model $\mathcal M$. A set of sentences T is satisfiable if there is a world w in an ${\mathsf {ILUPFO}}$-model $\mathcal M$ such that $\mathcal M,w\models \alpha$ for every $\alpha \in T$.

We will use the notation ${\mathsf {ILUPFO}}_{Meas}$ to denote the class of all fixed domain measurable models with rigid terms, where by measurable model we mean that the set $\{u\in W(w,a)\mid I(u)(\alpha )_\upsilon =true\}$ of all worlds from W(w, a) that satisfy $\alpha$ is measurable.

Axiomatic system for the logic ${\mathsf {ILUPFO}}$ contains all the axioms and inference rules from the Sect. 4 plus the following axiom schemes:

• (A8) $(\forall x) (\alpha \rightarrow \beta )\rightarrow (\alpha \rightarrow (\forall x)\beta )$, where the variable x doesn’t occur free in $\alpha$

• (A9) $(\forall x)\alpha (x)\rightarrow \alpha (t)$, where $\alpha (t)$ is obtained by substitution of all free occurrences of x in $\alpha (x)$ by the term t which is free for x in $\alpha (x)$

and the inference rule:

• (5) From $\alpha$ infer $(\forall x)\alpha$.

In the completeness proof we can follow the ideas from the propositional case. Deduction theorem holds for $Ax_{{\mathsf {ILUPFO}}}$. Namely, the facts that our infinitary inference rules have implicative form, and that the application of Rule 3 is restricted to theorems only guarantee the proof. Also, we need a special kind of maximal consistent sets called saturated sets. T is saturated if it is maximally consistent and satisfies the following condition:

         if $\lnot (\forall x)\alpha (x)\in T$, then for some term t, $\lnot \alpha (t)\in T$.

Definition 7

(Canonical model) A canonical model $\mathcal M_{Can}=\langle W,D,I,LUP\rangle$ is a tuple such that:

• W is the set of all saturated sets of formulas,

• D is the set of all variable-free terms,

• for every $w\in W$, I(w) is an interpretation such that:

  • for every function symbol $F_i^m$, $I(w)(F_i^m):D^m\rightarrow D$ such that for all variable-free terms $t_1,\ldots , t_m$, $I(w)(F_i^m):\langle t_1,\ldots , t_m\rangle \mapsto F_i^m (t_1,\ldots , t_m)$,

  • for every relation symbol $P_i^m$, $I(w)(P_i^m)=\{\langle t_1,\ldots , t_m\rangle \mid P_i^m (t_1,\ldots , t_m)\in w\}$, for all variable-free terms $t_1,\ldots , t_m$,

• for $a\in \varSigma$ and $w\in W$, $LUP(w,a)=\langle W(w,a),H(w,a),P(w,a)\rangle$ is defined:

  • $W(w,a)=W$,

  • $H(w,a)=\{\{u\mid u\in W(w,a),\alpha \in u\}\mid \alpha \in For_{{\mathsf {ILUPFO}}}\}$,

  • P(w, a) is any set of probability measures such that $P^\star (w,a)(\{u\mid u\in W(w,a),\alpha \in u\})=\sup \{s\mid U_{\ge s}^a\alpha \in w\}$.

Analogously as in the propositional case it can be proved that the canonical model is indeed a model via: For every formula $\alpha$ and every $w\in W$, $\alpha \in w$ iff $w\models \alpha$.

Theorem 8

(Lindenbaum’s theorem) Every consistent set of formulas can be extended to a saturated set.

Sketch of the proof

Consider a consistent set T and let $\alpha _0,\alpha _1,\ldots$ be an enumeration of all formulas from $For_{{\mathsf {ILUPFO}}}$. Let $T^\star$ denote the set of sentences obtained by the steps (1)–(3) of the Theorem 6 with one additional requirement in the step (2):

• if the set $T_{i+1}$ is obtained by adding a formula of the form $\lnot (\forall x)\beta (x)$ to the set $T_{i}$, then for some $c\in C$ (C is a countably infinite set of new constant symbols), $\lnot \beta (c)$ is also added to $T_{i+1}$, so that $T_{i+1}$ is consistent.

The new requirement produces consistent sets as well: suppose that for some $i>0$ the formula $\alpha _i$ is of the form $(\forall x)\beta (x)$ and that $T_i\cup \{(\forall x)\beta (x)\}$ is not consistent. Since $T_i$ is consistent, same holds for $T_i\cup \{\lnot (\forall x)\beta (x)\}$. If there is a constant $c\in C$ such that $\lnot \beta (c)\in T_i$, then obviously $T_i\cup \{(\forall x)\beta (x), \lnot \beta (c)\}$ is consistent. Suppose that there is no such c. Since the set T does not contain constants from C, and $T_i\cup \{\lnot (\forall x)\beta (x)\}$ is obtained by adding only finitely many formulas to the set T, there must be at least one constant $c\in C$ such that c does not appear in $T_i\cup \{\lnot (\forall x)\beta (x)\}$. If $T_i\cup \{\lnot (\forall x)\beta (x),\lnot \beta (c)\}$ is not consistent, then $T_i, \lnot (\forall x)\beta (x)\vdash \beta (c)$, and since c does not appear in $T_i\cup \{\lnot (\forall x)\beta (x)\}$, we obtain $T_i, \lnot (\forall x)\beta (x)\vdash (\forall x)\beta (x)$. Thus, $T_i\vdash (\forall x)\beta (x)$. It follows that the set $T_i$ is not consistent, a contradiction.

At the end, we have to show that $T^\star \vdash \alpha$ implies $\alpha \in T^\star$, to prove that $T^\star$ is consistent, while the construction guarantees that $T^\star$ is both maximal and saturated. The only case that does not appear in the proof of the Theorem 6 concerns the situation when $T^\star \vdash (\forall x)\beta (x)$ is obtained from $T^\star \vdash \beta (x)$ by the inference Rule 5. Since $\beta (x)$ has one free variable, and $T_i$ and $T^\star$ are sets of sentences, $\beta (x)$ does not belong to $T^\star$. However, by classical reasoning, we have $T^\star \vdash \beta (c)$, for every constant $c\in C$, and from the induction hypothesis $\beta (c)\in T^\star$. If $(\forall x)\beta (x)\notin T^\star$, the construction of the set $T^\star$ guarantees that there has to be some $i > 0$ such that $\beta (c),\lnot \beta (c)\in T_i$ for some $c\in C$. Contradiction. $\square$

Theorem 9

(Strong completeness) Every consistent set of formulas T is ${\mathsf {ILUPFO}}_{Meas}$-satisfiable.

6 Adding Infinite Number of Agents

In this section we extend the logics ${\mathsf {ILUPP}}$ and ${\mathsf {ILUPFO}}$ by considering a countable set of agents $\varSigma$. As previously pointed out by Halpern and Shore (2004), in many applications where the set of agents is not known in advance, and its cardinality has no a priori upper bound, it is easiest to model the set of agents as an infinite set.

In the rest of the section, we focus on extending ${\mathsf {ILUPP}}$; nevertheless, combining this section with the first-order extension results from the previous section will straightforwardly lead to the extension of ${\mathsf {ILUPFO}}$.

In order to keep the language countable, we will consider a countable set $\mathcal G$ of subsets of $\varSigma$. We do not pose any constraint about the elements of $\mathcal G$ (like closeness under intersection etc.). We use the same operators $L^G_{\ge s}$ and $U^G_{\ge s}$ as before, now allowing that G is any member of $\mathcal G$. Their semantical definition remains unchanged. However, the formulas of the form $L^G_{\ge s}\alpha$ and $U^G_{\ge s}\alpha$ now cannot be introduced as abbreviation, since we don’t have infinite disjunctions and conjunctions in syntax. Therefore, we formally:

(a):

extend the language with the operators $L^G_{\ge s}$ and $U^G_{\ge s}$, where $G\in \mathcal G$,

(b):

extend the definition of satisfiability in order to capture the new operators:

• $M,w\models L^G_{\ge s}\alpha$ iff $M,w\models L^a_{\ge s}\alpha$ for all $a\in G$,

• $M,w\models U^G_{\ge s}\alpha$ iff $M,w\models U^a_{\ge s}\alpha$ for some $a\in G$.

The extension of the logic ${\mathsf {ILUPP}}$ poses new axiomatization challenges. The fact that there is an infinite group of agents $G\in \mathcal {G}$ is an additional source of non-compactness of the logic. Indeed, the sets $\{ L_{\ge s}^a\beta \mid a\in G \} \cup \{ L_{<s}^G\beta \}$ and $\{ U_{< s}^a\beta \mid a\in G \} \cup \{ U_{\ge s}^G\beta \}$ are finitely satisfiable, but unsatisfiable sets of formulas. For that reason, we will use additional inference rules, in order to ensure inconsistency of those sets and to obtain strong completeness.

Note that, once we allow infinite groups of agents, we cannot use the formulas $L_{\ge s}^G\alpha \leftrightarrow \bigwedge _{a \in G}L_{\ge s}^a\alpha$ and $U_{\ge s}^G\alpha \leftrightarrow \bigvee _{a \in G}U_{\ge s}^a\alpha$, as we did in Sect. 2, to capture semantical definitions above. Instead, we extend the axiomatization of ${\mathsf {ILUPP}}$ with the axioms

• (A10) $L_{\ge s}^G\beta \rightarrow L_{\ge s}^a\beta$, if $a\in G$,

• (A11) $U_{\ge s}^a\beta \rightarrow U_{\ge s}^G\beta$, if $a\in G$,

and the inference rules

• (6) From the set of premises

  $$\begin{aligned} \{\alpha \rightarrow L_{\ge s}^a\beta \mid a\in G\} \end{aligned}$$

  infer $\alpha \rightarrow L_{\ge s}^G\beta$

• (7) From the set of premises

  $$\begin{aligned} \{\alpha \rightarrow U_{< s}^a\beta \mid a\in G\} \end{aligned}$$

  infer $\alpha \rightarrow U_{< s}^G\beta$.

We will prove that this axiomatization is strongly complete. In the completeness proof we can follow the ideas from Sect. 4. However, we need to extend the proofs of Theorem 5, Lemma 2 and Theorem 6.

In Theorem 5, we prove that $T,\alpha \vdash \beta$ implies $T\vdash \alpha \rightarrow \beta$, using the induction on the length of inference. Now we have two new inference rules. Here we consider the rule (6), while the proof for (7) is similar.

Assume that $T,\alpha \vdash \beta$ is obtained by the inference rule (6). Then $\beta$ is of the form $\alpha _1\rightarrow L_{\ge s}^G\beta _1$, and we have $T,\alpha \vdash \alpha _1\rightarrow L_{\ge s}^a\beta _1$ for all $a\in G$. Consequently, $T\vdash (\alpha \wedge \alpha _1)\rightarrow L_{\ge s}^a\beta _1$ for all $a\in G$, by the induction hypothesis and simple propositional reasoning (i.e., $(p \rightarrow (q \rightarrow r)) \longleftrightarrow ((p \wedge q) \rightarrow r)$). By the rule (6) we obtain $T\vdash (\alpha \wedge \alpha _1)\rightarrow L_{\ge s}^G\beta _1$, or, equivalently, $T\vdash \alpha \rightarrow (\alpha _1\rightarrow L_{\ge s}^G\beta _1)$. Thus, $T\vdash \alpha \rightarrow \beta$.

Next, in the proof of Lemma 2 we need to extend the proof that $\alpha \in u$ iff $u\models \alpha$. The proof was by induction on the complexity of $\alpha$. Since we now have a larger set of formulas, we need to consider the two additional cases in the proof: when $\alpha$ is of the form $L_{\ge s}^G\beta$ and when it is $U_{\ge s}^G\beta$. We assume that the operators of the group are of higher complexity then the operators of individual agents, for example $L_{\ge s}^G\beta$ is more complex then $U_{\ge s}^a\beta$. It is sufficient to show that for every maximal consistent set $T^\star$ the following conditions hold:

• (1) $L_{\ge s}^G\beta \in T^\star$ iff $\{L_{\ge s}^a\beta \ | \ a\in G\} \subseteq T^\star$,

• (2) $U_{\ge s}^G\beta \in T^\star$ iff $U_{\ge s}^a\beta \in T^\star$ for some $a\in G$.

Note that (1) follows directly from (A10) and the inference rule (6), and that ($\Leftarrow$) part of (2) follows from (A11). Let us prove ($\Rightarrow$) part of (2). Suppose that $U_{\ge s}^G\beta \in T^\star$ and $U_{\ge s}^a\beta \notin T^\star$ for every $a\in G$. By Maximality of $T^\star$, we have $\{U_{< s}^a\beta \ | \ a\in G\} \subseteq T^\star$. Then $T^\star \vdash U_{< s}^G\beta$ by the rule (7); a contradiction.

Finally, we need to modify the completion technique in the proof of Theorem 6. Recall that the completion of T is defined through an iterative process, assuming an enumeration $\alpha _0,\alpha _1,\ldots$ of all formulas. In the presence of the new rules, two new cases should be considered in the step (2), when $T_i\cup \{\alpha _i\}$ is inconsistent:

• (e) if $\alpha _i$ is of the form $\alpha \rightarrow L_{\ge s}^G\beta$, then $T_{i+1}=T_i\cup \{\lnot \alpha _i, \alpha \rightarrow L_{< s}^a\beta \}$, for some agent $a\in G$ such that $T_{i+1}$ is consistent,

• (f) if $\alpha _i$ is of the form $\alpha \rightarrow U_{< s}^G\beta$, then $T_{i+1}=T_i\cup \{\lnot \alpha _i,\alpha \rightarrow U_{\ge s}^a\beta \}$, for some agent $a\in G$ such that $T_{i+1}$ is consistent.

First, we need to show that each of the two conditions is correctly formulated, i.e., that there exists an agent $a\in G$ such that $T_{i+1}$ is consistent. This follows from Deduction theorem. For example, let us consider (e): if $T_{i+1}=T_i\cup \{\lnot \alpha _i, \alpha \rightarrow L_{< s}^a\beta \}$ is inconsistent for all $a\in G$, then $T_i\cup \{\lnot \alpha _i \} \vdash \lnot (\alpha \rightarrow L_{< s}^a\beta )$ for all $a\in G$. By (A1) we obtain $T_i\cup \{\lnot \alpha _i \} \vdash \alpha \rightarrow L_{\ge s}^a\beta$ for all $a\in G$, therefore $T_i\cup \{\lnot \alpha _i \} \vdash \alpha \rightarrow L_{\ge s}^G\beta$ by the inference rule (6).

Second, we need to prove that after adding the new inference rules, $T^\star$ is still deductively closed, i.e. $T^\star \vdash \alpha$ implies $\alpha \in T^\star$ (condition v) of the proof). Let us prove that $T^\star$ is closed under the rule (6). Let $\{\alpha \rightarrow L_{\ge s}^a\beta \mid a\in G\}\in T^\star$. Let $\alpha \rightarrow L_{\ge s}^G\beta =\alpha _i$, and suppose that $\alpha \rightarrow L_{\ge s}^G\beta \notin T^\star$. Then from the condition (e) we obtain $\lnot (\alpha \rightarrow L_{\ge s}^G\beta )\in T_{i+1}$; consequently, $T_{i+1}\vdash \alpha$. The same condition also ensures $\alpha \rightarrow L_{< s}^a\beta \in T_{i+1}$, for some agent $a\in G$. Recall that $\alpha \rightarrow L_{\ge s}^a\beta =\alpha _j\in T^\star$. Let j be the positive integer such that $\alpha \rightarrow L_{\ge s}^a\beta =\alpha _j$. Then $T_{\max \{i+1,j\}}\vdash \alpha$, $T_{\max \{i+1,j\}}\vdash \alpha \rightarrow L_{\ge s}^a\beta$ and $T_{\max \{i+1,j\}}\vdash \alpha \rightarrow L_{< s}^a\beta$, so $T_{\max \{i+1,j\}}\vdash \bot$; a contradiction. The proof that $T^\star$ is closed under the rule (7) is similar.

At the end of this section, we discuss the decidability issue. We can prove that this logic is decidable, provided that we can check whether the sets that are obtained by finite set operations on elements of $\mathcal G$ are empty or not. The similar assumption is posed by Halpern and Shore (2004), where it is also observed that possibility of deciding the cardinality of the set $G{\setminus } (G_1\cup \cdots \cup G_n)$ in general depends on the way how $G,G_1,\ldots ,G_n$ are presented and that if $G,G_1,\ldots ,G_n$ are recursive sets, deciding if $G{\setminus } (G_1\cup \cdots \cup G_n)$ is empty may not even be recursive. If we assume that we have oracles for testing whether those sets are empty or not, we can, given a formula $\alpha$, detect all the nonempty sets obtained by applying set operations on groups mentioned in $\alpha$.³ Then we can replace all the agents that have same membership functions in those sets (i.e., that belong to exactly the same groups) by a single representative of the set. In that way, we modify $\alpha$ by replacing each infinite set of agents from $\alpha$ with a finite set. Then we can use finite conjunctions and disjunction to eliminate sets of agents, using the tautologies $L_{\ge s}^G \beta \leftrightarrow \bigwedge _{a \in G}L_{\ge s}^a \beta$ and $U_{\ge s}^G \beta \leftrightarrow \bigvee _{a \in G}U_{\ge s}^a \beta$. In that way we obtain a formula of the logic ${\mathsf {ILUPP}}$ and we can apply the procedure from Sect. 3 to check its satisfiability.

7 ${\mathsf {ILUPP}}$ and ${\mathsf {ILUPFO}}$ as Generalizations of Probabilistic Logics

In this section we prove that the logics ${\mathsf {ILUPP}}$ and ${\mathsf {ILUPFO}}$ in a sense contain the logics ${\mathsf {LPP1}}$ and ${\mathsf {LFOP1}}$ (respectively) for reasoning about sharp probabilities (Ognjanović and Rašković 2000; Ognjanović et al. 2016). The two logics presented here have the similar semantical structure as the logics ${\mathsf {LPP1}}$ and ${\mathsf {LFOP1}}$, since they both use Kripke-like structures. It is intuitively clear that the semantics of our logics are more general, since reasoning about upper and lower probabilities requires sets of probability measures, while in the logics for reasoning about sharp probabilities one measure per possible world is sufficient (and thus they are isomorphic to the “sets of” probability measures which are actually singletons). On the other hand, the axiomatic systems are quite different. Here we will focus on the two proof theoretical aspects of the generalization: first, which axioms should be added to our logics (both ${\mathsf {ILUPP}}$ and ${\mathsf {ILUPFO}}$) to reduce the proposed class of models to the class of models isomorphic to the one for corresponding logic for sharp probabilities (${\mathsf {LPP1}}$ and ${\mathsf {LFOP1}}$, respectively), and second, how we can use the added axioms to formally obtain the axiomatizations of ${\mathsf {LPP1}}$ and ${\mathsf {LFOP1}}$.

In the rest of the section we will focus on relation between the logics ${\mathsf {ILUPP}}$ and ${\mathsf {LPP1}}$, but we stress that, similarly as in the previous section, analogous reasoning leads to the same relation in the first-order case, namely between the logics ${\mathsf {ILUPFO}}$ and ${\mathsf {LFOP1}}$. First we state only those properties of the logic ${\mathsf {LPP1}}$ important for this section [for more details about the logic ${\mathsf {LPP1}}$, as well as for the logic ${\mathsf {LFOP1}}$ we refer the reader to Ognjanović and Rašković (2000), Ognjanović et al. (2016)].

The language of the logic ${\mathsf {LPP1}}$ extends the classical propositional language with the list of operators $P_{\ge s}$, where s is a rational number from the [0, 1]. Concerning the syntax, besides the classical propositional formulas, formulas of the form $P_{\ge s}\alpha$ are also included. For example, $p\wedge P_{\le \frac{1}{2}}q$ and $P_{=\frac{1}{3}}P_{\ge 1}p$ are well defined formulas. ${\mathsf {LPP1}}$-structures are defined as triples $M=\langle W,Prob,\nu \rangle$, where:

• W is a non empty set of worlds

• Prob is a probability assignment which assigns to every $w\in W$ a probability space, such that $Prob(w) = \langle W(w), H(w),\mu (w)\rangle$, where:

  • W(w) is a non empty subset of W,

  • H(w) is an algebra of subsets of W(w) and

  • $\mu (w) : H(w)\rightarrow [0,1]$ is a finitely additive probability measure.

• $\nu$ provides for each world w an evaluation of the primitive propositions.

Satisfiability of a formula is defined as expected for the classical propositional formulas and

$$\begin{aligned} M,w\models P_{\ge s}\alpha \ \text {iff}\ \mu (\{v\in W(w)\mid v\models \alpha \})\ge s. \end{aligned}$$

Axiomatization of the logic ${\mathsf {LPP1}}$ is the following:

• (P1) all substitutional instances of the classical propositional tautologies,

• (P2) $P_{\ge 0}\alpha$,

• (P3) $P_{\le r}\alpha \rightarrow P_{<s}\alpha$, $s>r$,

• (P4) $P_{<s}\alpha \rightarrow P_{\le s}\alpha$,

• (P5) $(P_{\ge t}\alpha \wedge P_{\ge s}\beta \wedge P_{\ge 1}(\lnot \alpha \vee \lnot \beta ))\rightarrow P_{\ge min\{1,t+s\}}(\alpha \vee \beta )$,

• (P6) $(P_{\le t}\alpha \wedge P_{< s}\beta )\rightarrow P_{<t+s}(\alpha \vee \beta )$, $t+s\le 1$.

Inference Rules

• (1) Modus Ponens,

• (2) from $\alpha$ infer $P_{\ge 1}\alpha$,

• (3) from the set of premises

  $$\begin{aligned} \left\{ A\rightarrow P_{\ge s-\frac{1}{k}}\alpha \mid k\ge \frac{1}{s}\right\} \end{aligned}$$

  infer $A\rightarrow P_{\ge s}\alpha$.

Soundness and strong completeness theorems for the logic ${\mathsf {LPP1}}$ are proved (for more details see Ognjanović et al. 2016, chapter 4).

We will now focus on the relationship between ${\mathsf {ILUPP}}$ and ${\mathsf {LPP1}}$. First, since the logic ${\mathsf {LPP1}}$ is not a multi-agent logic we put that the set of agents $\varSigma$ is a singleton set (so instead of $U_{\ge r}^a\alpha$ we will write $U_{\ge r}\alpha$).

Then, it is clear that the subclass of the ${\mathsf {ILUPP}}$-structures that contains those structures where the set of finitely additive probability measures is a singleton set is isomorphic to the class of ${\mathsf {LPP1}}$-structures. Therefore, we add the following axiom:

$$\begin{aligned} (A12)\quad U_{\ge r}\alpha \rightarrow L_{\ge r}\alpha . \end{aligned}$$

(3)

We will denote ${\mathsf {ILUPP}}$+Axiom A12 by ${\mathsf {ILUPP}}^{Ext}.$

Let us recall note that it is shown in Savić et al. (2017a) (Proposition 1) that the following formula is a theorem in our axiomatization:

$$\begin{aligned} \vdash U_{\le r}\alpha \rightarrow L_{\le r}\alpha . \end{aligned}$$

(4)

From (3) and (4) follows that U and L have the same behavior in the sense that for every formula $\alpha$ and every $r\in S$

$$\begin{aligned} \vdash U_{\ge r}\alpha \leftrightarrow L_{\ge r}\alpha . \end{aligned}$$

(5)

This means that in ${\mathsf {ILUPP}}^{Ext}$ one type of operators is sufficient, since changing one type of operator with other will lead to an equivalent formula. For example, if we replace all the operators for lower probability with the operators of upper probability in

$$\begin{aligned} \alpha \equiv L_{\ge \frac{1}{3}}U_{\le \frac{1}{2}}L_{= 1}p, \end{aligned}$$

we will obtain the formula

$$\begin{aligned} \beta \equiv U_{\ge \frac{1}{3}}U_{\le \frac{1}{2}}U_{= 1}p \end{aligned}$$

which is equivalent to $\alpha$. This holds for any formula and can be proved in a straightforward manner by the induction on the complexity of a formula. This fact allows us, without loss of generality, to consider only formulas with the U operators in ${\mathsf {ILUPP}}^{Ext}$.

Our goal is to prove that the set of theorems of the logic ${\mathsf {LPP1}}$ is a subset of the set of theorems of the logic ${\mathsf {ILUPP}}^{Ext}$. Therefore, we will prove that all the axioms and inference rules of the logic ${\mathsf {LPP1}}$ can be inferred in the logic ${\mathsf {ILUPP}}^{Ext}$, where P is replaced by U.

Also notice that from the semantical point of view, addition of the axiom A12 guarantees that in an ${\mathsf {ILUPP}}$-structure the set of finitely additive probability measures is a singleton set and therefore has the same form as the ${\mathsf {LPP1}}$-structure.

The axioms (P1)–(P4) correspond to the axioms (A1)–(A4). It is also clear that the inference rules coincide as well. Our goal is to prove that the appropriate counterparts of the axioms (P5) and (P6), i.e.,

• (U5) $(U_{\ge t}\gamma \wedge U_{\ge s}\beta \wedge U_{\ge 1}(\lnot \gamma \vee \lnot \beta ))\rightarrow U_{\ge min\{1,t+s\}}(\gamma \vee \beta )$,

• (U6) $(U_{\le t}\gamma \wedge U_{< s}\beta )\rightarrow U_{<t+s}(\gamma \vee \beta )$, $t+s\le 1$,

follow from the axiomatization of ${\mathsf {ILUPP}}^{Ext}$, while in the inference the essential role play the axioms:

• (A5) $(U_{\le r_1}^a\alpha _1\wedge \cdots \wedge U_{\le r_m}^a\alpha _m)\rightarrow U_{\le r}^a\alpha$, if $\alpha \rightarrow \bigvee _{J\subseteq \{1,\ldots ,m\}, |J|=k+n}\bigwedge _{j\in J}\alpha _j$ and $\bigvee _{J\subseteq \{1,\ldots ,m\}, |J|=k}\bigwedge _{j\in J}\alpha _j$ are tautologies, where $r=\frac{\sum _{i=1}^m r_i-k}{n}$, $n\ne 0$

• (A6) $\lnot (U_{\le r_1}^a\alpha _1\wedge \cdots \wedge U_{\le r_m}^a\alpha _m)$, if $\bigvee _{J\subseteq \{1,\ldots ,m\}, |J|=k}\bigwedge _{j\in J}\alpha _j$ is a tautology and $\sum _{i=1}^m r_i<k$.

In order to prove that we need the following Lemma:

Lemma 4

${\mathsf {ILUPP}}^{Ext}\vdash (U_{\le t}\gamma \wedge U_{\le s}\beta )\rightarrow U_{\le t+s}(\gamma \vee \beta )$, $t+s\le 1$.

Proof

We will show that for $t+s\le 1$

$$\begin{aligned} (U_{\le t}\gamma \wedge U_{\le s}\beta )\rightarrow U_{\le t+s}(\gamma \vee \beta ) \end{aligned}$$

(6)

can be infered from A5. Consider the axiom A5 for:

• $m=2;\ n=1, k=0$; $r_1=t;\ r_2=s$;

• $\alpha _1=\gamma$;   $\alpha _2=\beta$;   $\alpha =\gamma \vee \beta$.

In this case we obtain $r=t+s$ and therefore the Axiom A5 has exactly the shape of the formula (6). We need also to check whether the formulas

$$\begin{aligned} \alpha \rightarrow \displaystyle {\bigvee _{J\subseteq \{1,2\}, |J|=1}}\bigwedge _{j\in J}\alpha _j \end{aligned}$$

and

$$\begin{aligned} \bigvee _{J\subseteq \{1,2\}, |J|=0}\bigwedge _{j\in J}\alpha _j \end{aligned}$$

are tautologies. The first formula has the form $\gamma \vee \beta \rightarrow \gamma \vee \beta$ which is clearly a tautology, while the second formula has the form $\bigwedge _{j\in \emptyset }\alpha _j$, and $\bigwedge _{j\in \emptyset }\alpha _j=\top$ by definition and hence a tautology. $\square$

Theorem 10

The set of theorems of the logic ${\mathsf {LPP1}}$ is a subset of the set of theorems of the logic ${\mathsf {ILUPP}}^{Ext}$.

Proof

As already stated, we need only to prove that:

• (a) ${\mathsf {ILUPP}}^{Ext}\vdash (U_{\ge t}\gamma \wedge U_{\ge s}\beta \wedge U_{\ge 1}(\lnot \gamma \vee \lnot \beta ))\rightarrow U_{\ge min\{1,t+s\}}(\gamma \vee \beta )$,

• (b) ${\mathsf {ILUPP}}^{Ext}\vdash (U_{\le t}\gamma \wedge U_{< s}\beta )\rightarrow U_{<t+s}(\gamma \vee \beta )$, $t+s\le 1.$

Proof of (a). Recall that the formula

$$\begin{aligned} (U_{\ge t}\gamma \wedge U_{\ge s}\beta \wedge U_{\ge 1}(\lnot \gamma \vee \lnot \beta ))\rightarrow U_{\ge min\{1,t+s\}}(\gamma \vee \beta ) \end{aligned}$$

can be written as:

$$\begin{aligned} (U_{\le 1-t}\lnot \gamma \wedge U_{\le 1-s}\lnot \beta \wedge U_{\le 0}(\gamma \wedge \beta ))\rightarrow U_{\le 1-min\{1,t+s\}}\lnot (\gamma \vee \beta ). \end{aligned}$$

Now, consider the axiom A5 for:

• $m=3;\ n=k=1$; $r_1=1-t;\ r_2=1-s;\ r_3=0$;

• $\alpha _1=\lnot \gamma$;   $\alpha _2=\lnot \beta$;   $\alpha _3=\gamma \wedge \beta$;   $\alpha =\lnot (\gamma \vee \beta ).$

We obtain that $r=1-(t+s)$.

(i):

If $t+s>1$ then (Axiom A6, $\sum _{i=1}^m r_i<k$)

$$\begin{aligned} \vdash \lnot (U_{\le 1-t}\lnot \gamma \wedge U_{\le 1-s}\lnot \beta \wedge U_{\le 0}(\gamma \wedge \beta )) \end{aligned}$$

and hence

$$\begin{aligned} \vdash (U_{\le 1-t}\lnot \gamma \wedge U_{\le 1-s}\lnot \beta \wedge U_{\le 0}(\gamma \wedge \beta ))\rightarrow U_{\le 1-min\{1,t+s\}}\lnot (\gamma \vee \beta )). \end{aligned}$$

(ii):

If $t+s\le 1$, then $1-min\{1,t+s\}=1-(t+s)=r$ and it is left to check if

$$\begin{aligned} \alpha \rightarrow \displaystyle {\bigvee _{J\subseteq \{1,2,3\}, |J|=2}}\bigwedge _{j\in J}\alpha _j \end{aligned}$$

and

$$\begin{aligned} \bigvee _{J\subseteq \{1,2,3\}, |J|=1}\bigwedge _{j\in J}\alpha _j \end{aligned}$$

are tautologies. Namely, in this case, the first formula has the following form: $\lnot (\gamma \vee \beta )\rightarrow ((\lnot \gamma \wedge \lnot \beta )\vee (\lnot \gamma \wedge \gamma \wedge \beta )\vee (\lnot \beta \wedge \gamma \wedge \beta )),$ and the second formula: $\lnot \gamma \vee \lnot \beta \vee (\gamma \wedge \beta ).$ It is obvious that both of these formulas are tautologies and therefore is this part proved.

Proof of (b).

Let us show equivalently that ${\mathsf {ILUPP}}^{Ext}\vdash (U_{\le t}\gamma \wedge U_{\ge t+s}(\gamma \vee \beta ))\rightarrow U_{\ge s}\beta$:

• $\vdash U_{\ge t+s}(\gamma \vee \beta )\rightarrow U_{> t+s'}(\gamma \vee \beta )$, for all $s'<s$   (contraposition of A3)

• $U_{\le t}\gamma \wedge U_{\ge t+s}(\gamma \vee \beta )\vdash U_{\le t}\gamma \wedge U_{> t+s'}(\gamma \vee \beta )$, for all $s'<s$

• $U_{\le t}\gamma \wedge U_{\ge t+s}(\gamma \vee \beta )\vdash U_{\le t}\gamma \wedge U_{> s'}\beta$, for all $s'<s$   (by Lemma 4)

• $U_{\le t}\gamma \wedge U_{\ge t+s}(\gamma \vee \beta )\vdash U_{\ge s}\beta$   (by Inference Rule (3))

• $\vdash (U_{\le t}\gamma \wedge U_{\ge t+s}(\gamma \vee \beta ))\rightarrow U_{\ge s}\beta$   (by Deduction theorem)

$\square$

8 Conclusion

In this paper we present the proof-theoretical analysis of two logics which allow making statements about upper and lower probabilities. The introduced formalisms, the propositional logic ${\mathsf {ILUPP}}$ and its first-order extension ${\mathsf {ILUPFO}}$, can be used for reasoning not only about lower and upper probabilities an agent assigns to a certain event, but also about her uncertain belief about other agent’s imprecise probabilities. The languages of our logics are modal languages which extend classical propositional/first-order languages with the unary operators $U^a_{\ge r}$ and $L^a_{\ge r}$, where a is an agent and r ranges over the unit interval of rational numbers. The corresponding semantics consist of the measurable Kripke models with sets of finitely additive probability measures attached to each possible world.

We prove that the proposed axiomatic systems are strongly complete with respect to the class of measurable models. Since the logics are not compact, the axiomatizations contain infinitary rules of inference. In Savić et al. (2017a) it is shown that the same axiomatic systems (the only difference is that in Savić et al. (2017a) only one agent is considered) is sound and complete for the logics without nesting of probabilistic operators. This situation is not an exception. For example, modal system K is sound and complete with respect to the class of all modal models, but also with respect to the class of all irreflexive models (Hughes and Cresswell 1984).

We provided the extensions of the proposed axiomatizations in order to properly capture the notions of lower and upper probability of an infinite set of agents. We also showed that the logics ${\mathsf {ILUPP}}$ and ${\mathsf {ILUPFO}}$ generalize the logics for reasoning about sharp probabilities from Ognjanović and Rašković (2000), Ognjanović et al. (2016).

We also prove that the satisfiability problem for ${\mathsf {ILUPP}}$ logic is decidable. In the proof, we use the method of filtration (Hughes and Cresswell 1984) to show that if a formula is satisfiable in a world w of an ${\mathsf {ILUPP}}$ structure, then it is satisfiable in a finite structure. We also use a reduction to linear programming to deal with infinitely many probability measures definable on finite algebras, and to solve the satisfiability problem in a finite number of steps.

We propose two topics for future work. First, we would like to investigate an alternative to the approach of upper and lower probability of a group presented here. We assumed that the agents share their sets of probabilities in order to obtain a larger set, available to all the members of the group. Alternatively, we wish to investigate the scenario in which they share their constraints, i.e., a group accepts those probability measures which satisfy lower and upper constraints of all the members of the group (i.e., $L_{\ge s}^G\alpha$ would be defined as a disjunction, and $U_{\ge s}^G\alpha$ as a conjunction). Note that this approach leads to an debatable consequence: consider the group $G=\{a,b\}$, where both lower and upper probability of $\alpha$ are $\frac{1}{2}$ for the agent a, while they are both $\frac{1}{3}$ for b; then lower probability of $\alpha$ wrt. G would be greater then the corresponding upper probability. This indicates that this approach is sensible if the formulas capture agents’ imprecise knowledge about an objective probability, in which case there shouldn’t be inconsistencies between the knowledge of different agents. In terms of semantics, the upper and lower probabilities of different agents should be all satisfied by a probability measure.

Second, we will investigate complexity of satisfiability problem for the logic ${\mathsf {ILUPP}}$. Such a method is already developed in Kokkinis (2017) for probabilistic logics with iterations of standard probability operators. Note that the fact that ${\mathsf {ILUPP}}$ is a generalization of the logic ${\mathsf {LPP1}}$ already leads to a complexity bound for ${\mathsf {ILUPP}}$. Namely, it was shown in Kokkinis (2017) that the satisfiability problem for the logic ${\mathsf {LPP1}}$ is ${\mathsf {PSPACE}}$-complete, thus a lower complexity bound for ${\mathsf {ILUPP}}$ is ${\mathsf {PSPACE}}$.