PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 87(101) (2010), 85–96 DOI: 10.2298/PIM1001085D

A LOGIC WITH CONDITIONAL PROBABILITY OPERATORS

Dragan Doder, Bojan Marinković, Petar Maksimović, and Aleksandar Perović

Communicated by Žarko Mijajlović

Abstract. We present a sound and strongly complete axiomatization of a reasoning about linear combinations of conditional probabilities, including comparative statements. The developed logic is decidable, with a PSPACE containment for the decision procedure.

1. Introduction

The present paper constitutes an effort to proceed along the lines of the research presented in [1, 2, 3, 5, 6, 7], on the formal development of probabilistic logics, where probability statements are expressed by probabilistic operators expressing bounds on the probability of a propositional formula. It is an extension of [1], which was presented at the 13^{th} ESSLLI Student Session in Hamburg, 2008.

This extension consists of introducing multiple conditional probability operators CP_{i}, i ∈ I, where I is a finite nonempty set of indices. These operators can be thought of as agents, with each of them having his own independent assessment of the conditional probability of an event. For instance, we formally write the statement “The conditional probability of α given β viewed by agent i is at least the sum of conditional probabilities of α given γ viewed by agent j and twice γ given α viewed by agent k." as CP_{i}(α, β) ⩾ CP_{j} (α, γ) + \underline{2}· CP_{k}(γ, α). We also prove that the developed logic is decidable, and show how it can be used to represent evidence.

In the classical Kolmogorovian sense, the conditional event “α given β” can be considered only in the case when P (β) > 0, and for such a conditional event, we have that

P (α|β) = P (α ∧ β)P (β)^{−1} . (1.1)

2010 Mathematics Subject Classification: Primary: 03B48.

Partially supported by the Ministry of Science, Republic of Serbia - Project 144013: Representations of logical structures and their application in computer science.

This may introduce certain difficulties in the formal construction of probabilistic formulas. It would be much easier if P (α|β) was a well-defined term, regardless of the formulas α and β, and the possible value of P (β).

An elegant solution can be obtained by adopting the convention that ^{−1} is a total operation, so that we can extend Kolmogorov’s definition of conditional probability onto all events: P (α|β) = P (α ∧ β)P (β)^{−1} . In particular, if P (β) = 0, then P (α ∧ β) = 0, so P (α|β) = P (α ∧ β)P (β)^{−1} = 0 · P (β)^{−1} = 0.

From this we observe that the actual value of 0^{−1} is irrelevant for the computation of P (α|β), and that in the case when P (β) = 0, the conditional probability defined as above behaves correctly. For the sake of simplicity, we let 0^{−1} = 1.

The rest of the paper is organized as follows. In Section 2, the syntax of the logic is given and the class of measurable probabilistic models is described. Section 3 contains the corresponding axiomatization and introduces the notion of deduction. A proof of the completeness theorem is presented in Section 4, whereas the decidability of the logic is analyzed in Section 5. Representing evidence in the developed logic is discussed in Section 6, and concluding remarks are in Section 7.

2. Syntax and semantics

Let Var = {p_{n} | n < ω} be the set of propositional variables. The corresponding set of all propositional formulas over Var will be denoted by For_{C}, and is defined in the usual way. Propositional formulas will be denoted by α, β and γ, possibly with indices. Let I be a finite nonempty set of indices.

Definition 2.1. The set Term of all probabilistic terms is recursively defined as follows:

• Term(0) = \{\underline{s} | s ∈ ℚ\} ∪ \{CP_{i}(α, β) | α, β ∈ For_{C}, i ∈ I\}.

• Term(n + 1) = Term(n) ∪ \{(f + g), (\underline{s} · g), (−f) | f, g ∈ Term(n), s ∈ ℚ\}

• Term = ⋃ _{n=0}^{∞} Term(n).

Probabilistic terms will be denoted by f, g and h, possibly with indices. To simplify notation, we introduce the following convention: f + g is (f + g), f + g + h is ((f + g) + h). For n > 3, ∑ _{i=1}^{n} f_{i} is ((⋯ ((f_{1} + f_{2}) + f_{3}) + ⋯) + f_{n}). Similarly, −f is (−f) and f − g is (f + (−g)).

If α and β are propositional formulas, and i ∈ I, then the probabilistic term CP_{i}(α, β) reads “the conditional probability of α given β viewed by agent i". To simplify notation, we will write P_{i}(α) instead of CP_{i}(α, ⊤), where ⊤ is an arbitrary tautology instance.

Definition 2.2. A basic probabilistic formula is any formula of the form f ⩾ \underline{0}. Furthermore, we define the following abbreviations:

• f ⩽ \underline{0} is −f ⩾ \underline{0};  • f > \underline{0} is ¬(f ⩽ \underline{0});  • f < \underline{0} is ¬(f ⩾ \underline{0});
• f = \underline{0} is f ⩽ \underline{0} ∧ f ⩾ \underline{0};  • f ≠ \underline{0} is ¬(f = \underline{0});  • f ⩾ g is f − g ⩾ \underline{0}.

We define f ⩽ g, f > g, f < g, f = g and f ≠ g in a similar way.

A probabilistic formula is a Boolean combination of basic probabilistic formulas.

As in the propositional case, ¬ and ∧ are the primitive connectives, while all of the other connectives are introduced in the usual way. Probabilistic formulas will be denoted by ϕ, ψ and θ, possibly with indices. The set of all probabilistic formulas will be denoted by For_{P}.

By “formula" we mean either a classical formula or a probabilistic formula. We do not allow for the mixing of those types of formulas, nor for the nesting of the probability operators CP_{i}. Formulas will be denoted by Φ, Ψ and Θ, possibly with indices. The set of all formulas will be denoted by For.

We define the notion of a model as a special kind of Kripke model. Namely, a model M is any tuple ⟨W, H, {μ_{i}|i ∈ I}, v⟩ such that:

• W is a nonempty set. As usual, its elements will be called worlds.

• H is an algebra of sets over W.

• for each i ∈ I, μ_{i} : H −→ [0, 1] is a finitely additive probability measure.

• v : For_{C} ×W −→ {0, 1} is a truth assignment^{1} compatible with ¬ and ∧. That is, v(¬α, w) = 1 − v(α, w) and v(α ∧ β, w) = v(α, w) · v(β, w).

For a given model M, let [α]_{M} be the set of all w ∈ W such that v(α, w) = 1. If the context is clear, we will write [α] instead of [α]_{M}. We say that M is measurable if [α] ∈ H for all α ∈ For_{C}.

Definition 2.3. Let M = ⟨W, H, {μ_{i} | i ∈ I}, v⟩ be any measurable model.

We define the satisfiability relation ⊨ recursively as follows:

• M ⊨ α if v(α, w) = 1 for all w ∈ W.

• M ⊨ f ⩾ \underline{0} if f^{M} ⩾ 0, where f^{M} is recursively defined as follows:

– \underline{s}^{M} = s.
– CP_{i}(α, β)^{M} = μ_{i}([α ∧ β]) · μ_{i}([β])^{−1} , for any i ∈ I.
– (f + g)^{M} = f^{M} + g^{M}.
– (\underline{s} · g)^{M} = s · g^{M}.
– (−f)^{M} = −(f^{M}).

• M ⊨ ¬ϕ if M ⊭ ϕ.

• M ⊨ ϕ ∧ ψ if M ⊨ ϕ and M ⊨ ψ.

A formula Φ is satisfiable if there is a measurable model M such that M ⊨ Φ; Φ is valid if it is satisfied in every measurable model. We say that the set T of formulas is satisfiable if there is a measurable model M such that M ⊨ Φ for all Φ ∈ T.

Notice that the last two clauses of Definition 2.3 provide the validity of each tautology instance.

3. Axiomatization

In this section we will introduce the axioms and inference rules for our logic. The set of axioms of our axiomatic system, which we denote AX_{LPCP} , is divided into three groups: axioms for propositional reasoning, axioms for probabilistic reasoning and arithmetical axioms. Axioms for propositional reasoning:

A1. τ(Φ_{1}, …, Φ_{n}), where τ(p_{1}, …, p_{n}) ∈ For_{C} is any tautology and Φ_{i} are either all propositional or all probabilistic.

11 stands for “true", while 0 stands for “false"

Axioms for probabilistic reasoning (i ∈ I):

A2. P_{i}(α) ⩾ \underline{0}; A5. P_{i}(α ↔ β) = \underline{1} → P_{i}(α) = P_{i}(β);
A3. P_{i}(⊤) = \underline{1}; A6. P_{i}(α ∨ β) = P_{i}(α) + P_{i}(β) − P_{i}(α ∧ β);
A4. P_{i}(⊥) = \underline{0}; A7. P (β) = 0 → CP (α, β) = 0;
A8. (P_{i}(α ∧ β) ⩾ \underline{r} ∧ P_{i}(β) ⩽ \underline{s}) → CP_{i}(α, β) ⩾ \underline{r · s^{−1}} , s ≠ 0;
A9. (P_{i}(α ∧ β) > \underline{r} ∧ P_{i}(β) ⩽ \underline{s}) → CP_{i}(α, β) > \underline{r · s^{−1}} , s ≠ 0;
A10. (P_{i}(α ∧ β) ⩾ \underline{r} ∧ P_{i}(β) < \underline{s}) → CP_{i}(α, β) > \underline{r · s^{−1}} , s ≠ 0;
A11. (P_{i}(α ∧ β) ⩽ \underline{r} ∧ P_{i}(β) ⩾ \underline{s}) → CP_{i}(α, β) ⩽ \underline{r · s^{−1}} , s ≠ 0;
A12. (P_{i}(α ∧ β) < \underline{r} ∧ P_{i}(β) ⩾ \underline{s}) → CP_{i}(α, β) < \underline{r · s^{−1}} , s ≠ 0;
A13. (P_{i}(α ∧ β) ⩽ \underline{r} ∧ P_{i}(β) > \underline{s}) → CP_{i}(α, β) < \underline{r · s^{−1}} , s ≠ 0.

Arithmetical axioms:

A14. \underline{r} > \underline{s}, whenever r > s;  A23. \underline{s} · (f + g) = (\underline{s} · f) + (\underline{s} · g);
A15. \underline{r} ⩾ \underline{s}, whenever r ⩾ s;  A24. \underline{r} · (\underline{s} · f) = \underline{r · s}· f;
A16. \underline{s} · \underline{r} = \underline{sr};  A25. \underline{1} · f = f;
A17. \underline{s} + \underline{r} = \underline{s + r} ;  A26. f ⩾ g ∨ g ⩾ f;
A18. f + g = g + f;  A27. (f ⩾ g ∧ g ⩾ h) → f ⩾ h;
A19. (f + g) + h = f + (g + h);  A28. f ⩾ g → f + h ⩾ g + h;
A20. f + \underline{0} = f;  A29. (f ⩾ g ∧ \underline{s} > \underline{0}) → \underline{s} · f ⩾ \underline{s} · g;
A21. f − f = \underline{0};  A30. f = g → (ϕ(…, f, …) → ϕ(…, g, …)).

A22. (\underline{r} · f) + (\underline{s} · f) = \underline{r + s} · f;

Inference rules

R1. From Φ and Φ → Ψ infer Ψ.

R2. From α infer P_{i}(α) = \underline{1}, for all i ∈ I.

R3. From the set of premises \{ϕ → f ⩾ \underline{−n^{−1}} | n = 1, 2, 3, …\} infer ϕ → f ⩾ \underline{0}.

Let us briefly comment on the axioms and inference rules. The axioms A2-A6 provide the required properties of probability, the axioms A7–A13 capture the equality (1.1) using the fact that ℚ is dense in ℝ, while the axioms A14–A30 provide the properties required for computation. In the inference rules, R1 is modus ponens, R2 resembles necessitation, while R3 enforces that non-Archimedean probabilites are not permitted.

Definition 3.1. A formula Φ is deducible from a set T of sentences (T ⊢ Φ) if there is an at most countable sequence of formulas Φ_{0}, Φ_{1}, …, Φ, such that every Φ_{i} is an axiom or a formula from the set T, or it is derived from the preceding formulas by an inference rule. A formula Φ is a theorem (⊢ Φ) if it is deducible from the empty set. A set of sentences T is consistent if there is at least one formula from For_{C}, and at least one formula from For_{P} that are not deducible from T. Otherwise, T is inconsistent. A consistent set T of sentences is said to be maximally consistent if for every ϕ ∈ For, either ϕ ∈ T or ¬ϕ ∈ T. A set T is deductively closed if for every Φ ∈ For, if T ⊢ Φ, then Φ ∈ T.

Observe that the length of the inference may be any successor ordinal lesser than the first uncountable ordinal ω_{1}.

4. Completeness

In this section we will prove that the proposed axiomatization is sound and strongly complete with respect to the class of all measurable models.

Using a straightforward induction on the length of the inference, one can easily show that the above axiomatization is sound with respect to the class of all measurable models.

Theorem 4.1 (Deduction theorem). Suppose that T is an arbitrary set of formulas and that Φ, Ψ ∈ For. Then, T ⊢ Φ → Ψ iff T ∪ {Φ} ⊢ Ψ.

Proof. If T ⊢ Φ → Ψ, then clearly T ∪ {Φ} ⊢ Φ → Ψ, so, by modus ponens (R1), T ∪ {Φ} ⊢ Ψ. Conversely, let T ∪ {Φ} ⊢ Ψ. As in the classical case, we will use induction on the length of the inference to prove that T ⊢ Φ → Ψ. The proof differs from the classical one only in the cases when we apply the infinitary inference rule R3.

Suppose that Ψ is the formula ϕ → f ⩾ \underline{0} and T ⊢ Φ → (ϕ → f ⩾ \underline{−n^{−1}} ) for all n. Since the formula (p_{0} → (p_{1} → p_{2})) ↔ ((p_{0} ∧ p_{1}) → p_{2}) is a tautology, we obtain T ⊢ (Φ ∧ ϕ) → f ⩾ \underline{−n^{−1}} , for all n (A1). Now, by R3, T ⊢ (Φ ∧ ϕ) → f ⩾ \underline{0}. Hence, by the same tautology, T ⊢ Φ → Ψ. □

The next technical lemma will be used in the construction of a maximally consistent extension of a consistent set of formulas.

Lemma 4.1. Suppose that T is a consistent set of formulas. If T ∪\{ϕ → f ⩾ \underline{0}\} is inconsistent, then there exists a positive integer n such that T ∪\{ϕ → f < \underline{−n^{−1}} \} is consistent.

Proof. The proof is based on the reductio ad absurdum argument. Thus, let us suppose that T ∪ \{ϕ → f < \underline{−n^{−1}} \} is inconsistent for all n. Due to the Deduction theorem, we can conclude that T ⊢ ϕ → f ⩾ \underline{−n^{−1}} , for all n. By R3, T ⊢ ϕ → f ⩾ \underline{0}, so T is inconsistent; a contradiction. □

Definition 4.1. Suppose that T is a consistent set of formulas and that For_{P} = {ϕ_{i} | i = 0, 1, 2, 3, …}. We define a completion T^{∗} of T inductively as follows:

(1) T_{0} = T ∪ \{α ∈ For_{C} | T ⊢ α\} ∪ \{P_{i}(α) = \underline{1} | T ⊢ α, i ∈ I\}.

(2) If T_{i} ∪ {ϕ_{i}} is consistent, then T_{i+1} = T_{i} ∪ {ϕ_{i}}.
(3) If T_{i} ∪ {ϕ_{i}} is inconsistent, then:
(a) If ϕ_{i} has the form ψ → f ⩾ \underline{0}, then T_{i+1} = T_{i} ∪ \{ψ → f < \underline{−n^{−1}} \},

where n is a positive integer such that T_{i+1} is consistent. The existence of such an n is provided by Lemma 4.1.

(b) Otherwise, T_{i+1} = T_{i}.

(4) T^{∗} = ⋃ _{n∈ω} T_{n}.

Obviously, each T_{i} is consistent. In the next theorem we will prove that T^{∗} is deductively closed, consistent and maximal with respect to For_{P}.

Theorem 4.2. Suppose that T is a consistent set of formulas and that T^{∗} is constructed as above. Then:

(1) T^{∗} is deductively closed, id est, T^{∗} ⊢ Φ implies Φ ∈ T^{∗}.

(2) There is ϕ ∈ For_{P} such that ϕ ∉ T^{∗}.

(3) There is α ∈ For_{C} such that α ∉ T^{∗}.

(4) For each ϕ ∈ For_{P}, either ϕ ∈ T^{∗}, or ¬ϕ ∈ T^{∗}.

Proof. We will prove only the first clause, since the remaining clauses can be proved in the same way as in the classical case. In order to do so, it is sufficient to prove the following four claims:

(i): Each instance of any axiom is in T^{∗}. (ii): If Φ ∈ T^{∗} and Φ → Ψ ∈ T^{∗}, then Ψ ∈ T^{∗}. (iii): If α ∈ T^{∗}, then P_{i}(α) = 1 ∈ T^{∗}, for all i ∈ I. (iv): If \{ϕ → f⩾\underline{−n^{−1}} | n = 1, 2, 3, …\} is a subset of T^{∗}, then ϕ → f ⩾ \underline{0} ∈ T^{∗}.

(i): If Φ ∈ For_{C}, then Φ ∈ T_{0}. Otherwise, there exists a nonnegative integer i, such that Φ = ϕ_{i}. Since ⊢ ϕ_{i}, T_{i} ⊢ ϕ_{i} as well, and so ϕ_{i} ∈ T_{i+1} .

(ii): If Φ, Φ → Ψ ∈ For_{C}, then Ψ ∈ T_{0}. Otherwise, let Φ = ϕ_{i}, Ψ = ϕ_{j}, and Φ → Ψ = ϕ_{k}. Then, Ψ is a deductive consequence of each T_{l}, where l ⩾ max(i, k) + 1. Let ¬Ψ = ϕ_{m}. If ϕ_{m} ∈ T_{m+1} , then ¬Ψ is a deductive consequence of each T_{n}, where n ⩾ m + 1. So, for every n ⩾ max(i, k, m) + 1, T_{n} ⊢ Ψ ∧ ¬Ψ, a contradiction. Thus, ¬Ψ ∉ T^{∗}. On the other hand, if also Ψ ∉ T^{∗}, we have that T_{n} ∪ {Ψ} ⊢ ⊥, and T_{n} ∪ {¬Ψ} ⊢ ⊥, for n ⩾ max(j, m) + 1, a contradiction with the consistency of T_{n}. Thus, Ψ ∈ T^{∗}.

(iii): If α ∈ T^{∗}, then α ∈ T_{0}, so P_{i}(α) = \underline{1} ∈ T_{0} for all i ∈ I.

(iv): Suppose that \{ϕ → f ⩾ \underline{−n^{−1}} | n = 0, 1, 2, …\} is a subset of T^{∗}. We want to prove that ϕ → f ⩾ \underline{0} ∈ T^{∗}. The proof uses the reductio ad absurdum argument. So, let ϕ → f ⩾ \underline{0} = ϕ_{i} and let us suppose that T_{i} ∪ \{ϕ_{i}\} is inconsistent. By 3.(a) of Definition 4.1, there is a positive integer n such that

T_{i+1} = T_{i} ∪ \{ϕ → f < \underline{−n^{−1}} \}

and T_{i+1} is consistent. Then, for all sufficiently large k, T_{k} ⊢ ϕ → f < \underline{−n^{−1}} and T_{k} ⊢ ϕ → f ⩾ \underline{−n^{−1}} , so T_{k} ⊢ ϕ → ψ for all ψ ∈ For_{P}. In particular, T_{k} ⊢ ϕ → f ⩾ \underline{0}, i. e. T_{k} ⊢ ϕ_{i} for all sufficiently large k. But, ϕ_{i} ∉ T^{∗}, so ϕ_{i} is inconsistent with all T_{k}, k ⩾ i. It follows that each T_{k} is inconsistent for sufficiently large k, a contradiction.

Thus, T_{i} ∪ \{ϕ_{i}\} is consistent, so ϕ → f ⩾ \underline{0} ∈ T_{i+1} . □

For the given completion T^{∗}, we define a canonical model M^{∗} as follows:

• W is the set of all functions w : For_{C} −→ {0, 1} with the following properties: – w is compatible with ¬ and ∧.

– w(α) = 1 for each α ∈ T^{∗}.

• v : For_{C} ×W −→ {0, 1} is defined by v(α, w) = 1 iff w(α) = 1.

• H = {[α] | α ∈ For_{C}}.

• μ_{i} : H −→ [0, 1] is defined by μ_{i}([α]) = sup\{s ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{i}(α) ⩾ \underline{s}\}, for all i ∈ I.

Lemma 4.2. M^{∗} is a measurable model.

Proof. We need to prove that H is an algebra of sets and that each μ_{i} is a finitely additive probability measure. It is easy to see that H is an algebra of sets, since [α] ∩ [β] = [α ∧ β], [α] ∪ [β] = [α ∨ β] and H ∖ [α] = [¬α]. Concerning μ_{i}, the nonnegativity (μ_{i}([α]) ⩾ 0) is the consequence of A2 and the definition of μ_{i}, while μ_{i}(W) = 1 follows from A3, since W = [⊤]. We will give the proof of finite additivity.

Let μ_{i}([α]) = a, μ_{i}([β]) = b and μ_{i}([α ∧ β]) = c. We claim that

μ_{i}([α ∨ β]) = a + b − c.

Since ℚ is dense in ℝ, we may choose an increasing sequence \underline{a}_{0} < \underline{a}_{1} < \underline{a}_{2} < ⋯ and a decreasing sequence \overline{a}_{0} > \overline{a}_{1} > \overline{a}_{2} > ⋯in ℚ such that lim \underline{a}_{n} = lim \overline{a}_{n} = a. Using the definition of μ_{i} and Theorem 4.2(4), we obtain that T^{∗} ⊢ P_{i}(α) ⩾ \underline{a}_{n} and that T^{∗} ⊢ P_{i}(ϕ) < \overline{a}_{n}, for all n.

We may also choose increasing sequences (\underline{b}_{n})_{n∈ω} and (\underline{c}_{n})_{n∈ω} , and decreasing sequences (\overline{b}_{n})_{n∈ω} and (\overline{c}_{n})_{n∈ω} in ℚ, such that lim \underline{b}_{n} = lim \overline{b}_{n} = b and lim \underline{c}_{n} = lim \overline{c}_{n} =c. So, T^{∗} ⊢ P_{i}(β) ⩾ \underline{b}_{n}∧P_{i}(β) < \overline{b}_{n} and T^{∗} ⊢ P_{i}(α∧β) ⩾ \underline{c}_{n}∧P_{i}(α∧β) < \overline{c}_{n}.

Using the arithmetical axioms, we have

T^{∗} ⊢ P_{i}(α) + P_{i}(β) − P_{i}(α ∧ β) ⩾ \underline{a}_{n} + \underline{b}_{n} − \overline{c}_{n},
T^{∗} ⊢ P_{i}(α) + P_{i}(β) − P_{i}(α ∧ β) < \overline{a}_{n} + \overline{b}_{n} − \underline{c}_{n}

for all n. Using A6 and A30, we obtain that T^{∗} ⊢ P_{i}(α ∨ β) ⩾ \underline{a}_{n} + \underline{b}_{n} − \overline{c}_{n} and that T^{∗} ⊢ P_{i}(α ∨ β) < \overline{a}_{n} + \overline{b}_{n} − \underline{c}_{n}, for all n.

Finally, from

μ_{i}([α ∨ β]) = sup{r ∈ ℚ | T^{∗} ⊢ P_{i}(α ∨ β) ⩾ r}

and lim \underline{a}_{n} + \underline{b}_{n} − \overline{c}_{n} = lim \overline{a}_{n} + \overline{b}_{n} − \underline{c}_{n} = a + b − c, we obtain that μ_{i}([α ∨ β]) = a + b − c. □

Theorem 4.3 (Strong completeness theorem). Every consistent set of formulas has a measurable model.

Proof. Let T be a consistent set of formulas. We can extend it to a maximally consistent set T^{∗}, and define a canonical model M^{∗}, as above. By induction on the complexity of the formulas, we can prove that M^{∗} ⊨ Φ iff Φ ∈ T^{∗}.

To begin the induction, let Φ = α ∈ For_{C}. If α ∈ T^{∗}, i.e., T^{∗} ⊢ α, then, by definition of M^{∗}, M^{∗} ⊨ α. Conversely, if M^{∗} ⊨ α, by the completeness of classical propositional logic, T^{∗} ⊢ α, and α ∈ T^{∗}.

Let us suppose that f ⩾ \underline{0} ∈ T^{∗}. Then, using the axioms A16–A19, A22–A25 and A30, we can prove that

T^{∗} ⊢ f = \underline{s} + ∑_{i=1}^{m} \underline{s_{i}} · CP_{n_{i}} (α_{i}, β_{i}) and T^{∗} ⊢ \underline{s} + ∑_{i=1}^{m} \underline{s_{i}} · CP_{n_{i}} (α_{i}, β_{i}) ⩾ \underline{0},

for some s, s_{i} ∈ ℚ and some α_{i}, β_{i} ∈ For_{C}, n_{i} ∈ I. Moreover, according to the axioms A7, A16, A20 and A30, we may assume that T^{∗} ⊢ P_{n_{i}} (β_{i}) > \underline{0}.

(For example, let T^{∗} ⊢ f ⩾ \underline{0}, where f = \underline{4}CP_{1}(α_{1}, β_{1}) + \underline{3}(\underline{5}+ \underline{2}CP_{2}(α_{2}, β_{2})) + \underline{1}+ CP_{2}(α_{2}, β_{2}). Using the axioms A16, A17, A18,A19, A22, A23 and A24, we can prove that

T^{∗} ⊢ f = \underline{16} + \underline{4}CP_{1}(α_{1}, β_{1}) + \underline{7}CP_{2}(α_{2}, β_{2}),

T^{∗} ⊢ \underline{16} + \underline{4}CP_{1}(α_{1}, β_{1}) + \underline{7}CP_{2}(α_{2}, β_{2}) ⩾ \underline{0}. (4.1)

Moreover, if T^{∗} ⊢ P_{1}(β_{1}) = \underline{0}, then, by A7, T^{∗} ⊢ CP_{1}(α_{1}, β_{1}) = \underline{0}. Using A30, we obtain that T^{∗} ⊢ \underline{4}CP_{1}(α_{1}, β_{1}) = \underline{4} · \underline{0}. Since ⊢ \underline{0} = \underline{4} · \underline{0} (A16), it follows from A30 that T^{∗} ⊢ \underline{4}CP_{1}(α_{1}, β_{1}) = \underline{0} Finally, by (4.1), A20 and A30, we obtain that T^{∗} ⊢ \underline{16} + \underline{7}CP_{2}(α_{2}, β_{2}) ⩾ \underline{0}, and, similarly, that T^{∗} ⊢ f = \underline{16} + \underline{7}CP_{2}(α_{2}, β_{2}).)

Let a_{i} = μ_{n_{i}} ([α_{i} ∧ β_{i}]) and b_{i} = μ_{n_{i}} ([β_{i}]). We need to prove that

(4.2)  s + ∑_{i=1}^{m} s_{i} · a_{i} · b_{i}^{−1} ⩾ 0.

Note that T^{∗} ⊢ CP_{i}(α, β) ⩾ \underline{r} implies μ_{i}([α_{i} ∧ β_{i}])μ_{i}([β_{i}])^{−1} ⩾ r. Indeed, if μ_{i}([α_{i} ∧ β_{i}])μ_{i}([β_{i}])^{−1} < r, there exist a, b ∈ ℚ such that a > μ_{i}([α_{i} ∧ β_{i}]), b ⩽ μ_{i}([β_{i}]) and μ_{i}([α_{i} ∧ β_{i}])μ_{i}([β_{i}])^{−1} < \frac{a}{b} < r. Consequently, T^{∗} ⊢ P_{i}(α ∧ β) < \underline{a} and T^{∗} ⊢ P_{i}(β) ⩾ \underline{b}, hence, by A12, T^{∗} ⊢ CP_{i}(α, β) < \underline{a · b^{−1}}; a contradiction. Similarly, we can show that T^{∗} ⊢ CP_{i}(α, β) ⩽ \underline{r} implies μ_{i}([α_{i} ∧ β_{i}])μ_{i}([β_{i}])^{−1} ⩽ r. As a consequence, we have that μ_{i}([α_{i}]|[β_{i}]) = sup\{r ∈ ℚ | T^{∗} ⊢ CP_{n_{i}} (α, β) ⩾ \underline{r}\}.

So, we may choose increasing sequences (c_{i,k}^{inc})_{k∈ω} and decreasing sequences (c_{i,k}^{dec})_{k∈ω} in ℚ, such that limc_{i,k}^{inc} = limc_{i,k}^{dec} = a_{i}b_{i}^{−1} , for i ∈ {1, …, m}. Hence, T^{∗} ⊢ CP_{n_{i}} (α, β) ⩾ \underline{c_{i,k}^{inc}} ∧ CP_{n_{i}} (α, β) < \underline{c_{i,k}^{dec}}, for i ∈ \{1, …, m\} and k ∈ ω .

Without the loss of generality, suppose that T^{∗} ⊢ \underline{s_{i}} ⩾ \underline{0}, for 1 ⩽ i ⩽ l, and T^{∗} ⊢ \underline{s_{i}} < \underline{0}, for l < i ⩽ m. Then, by the arithmetical axioms,

T^{∗} ⊢ \underline{s} + ∑_{i=1}^{l} \underline{s_{i}} · \underline{c_{i,k}^{inc}} + ∑_{i=l+1}^{m} \underline{s_{i}} · \underline{c_{i,k}^{dec}} ⩽ \underline{s} + ∑_{i=1}^{m} \underline{s_{i}} · CP_{n_{i}} (α_{i}, β_{i}),

T^{∗} ⊢ \underline{s} + ∑_{i=1}^{l} \underline{s_{i}} · \underline{c_{i,k}^{dec}} + ∑_{i=l+1}^{m} \underline{s_{i}} · \underline{c_{i,k}^{inc}} ⩾ \underline{s} + ∑_{i=1}^{m} \underline{s_{i}} · CP_{n_{i}} (α_{i}, β_{i})

for all k. Consequently,

s + ∑_{i=1}^{m} s_{i} · a_{i} · b_{i}^{−1} = sup\{ r ∈ ℚ | T^{∗} ⊢ \underline{s} + ∑_{i=1}^{m} \underline{s_{i}} · CP_{n_{i}} (α_{i}, β_{i}) ⩾ \underline{r}\} .

Now, (4.2) follows from T^{∗} ⊢ \underline{s} + ∑ _{i=1}^{m} \underline{s_{i}} · CP_{n_{i}} (α_{i}, β_{i}) ⩾ \underline{0}.

For the other direction, let M^{∗} ⊨ f ⩾ \underline{0}. If f ⩾ \underline{0} ∉ T^{∗}, from the construction of T^{∗}, there is a positive integer n such that f < \underline{−n^{−1}} ∈ T^{∗}. Reasoning as above, we have that f^{M^{∗}} < 0, which is a contradiction. So, f ⩾ \underline{0} ∈ T^{∗}.

Let Φ = ¬ϕ ∈ For_{P}. Then M^{∗} ⊨ ¬ϕ iff M^{∗} ⊭ ϕ iff ϕ ∉ T^{∗} iff (by Theorem 4.2) ¬ϕ ∈ T^{∗}.

Finally, let Φ = ϕ∧ψ ∈ For_{P}. M^{∗} ⊨ ϕ∧ψ iff M^{∗} ⊨ ϕ and M^{∗} ⊨ ψ iff ϕ, ψ ∈ T^{∗} iff (by Theorem 4.2) ϕ ∧ ψ ∈ T^{∗}. □

5. Decidability

Theorem 5.1. Satisfiability of probabilistic formulas is decidable.

Proof. Up to equivalence, each probabilistic formula is a finite disjunction of finite conjunctions of literals, where a literal is either a basic probabilistic formula, or a negation of a basic probabilistic formula. Thus, it is sufficient to show the decidability of the satisfiability problem for the formulas of the form

(5.1)  ⋀_{i} f_{i} ⩾ \underline{0} ∧ ⋀_{j} g_{j} < \underline{0}.

Suppose that p_{1}, …, p_{n} are all of the propositional letters appearing in (5.1). Let A_{1}, …, A_{2^{n}} be all of the formulas of the form ±p_{1} ∧ ⋯∧ ±p_{n}, where +p = p and −p = ¬p. Clearly, A_{i} are pairwise disjoint and form a partition of ⊤. Furthermore, for each α appearing in (5.1) there is a unique set I_{α} ⊆ {1, …, 2^{n}} such that α ↔ ⋁ _{i∈I_{α}} A_{i} is a tautology. Now we can equivalently rewrite (5.1) as

⋀_{i} ∑_{i′} \underline{s_{ii′}} CP_{n_{i′}} ( ⋁_{k∈I_{α_{ii′}}} A_{k}, ⋁_{l∈I_{β_{ii′}}} A_{l}) ⩾ \underline{r}_{i}

∧ ⋀_{j} ∑_{j′} \underline{s_{jj′}} CP_{n_{j′}} ( ⋁_{k∈I_{α_{jj′}}} A_{k}, ⋁_{l∈I_{β_{jj′}}} A_{l}) < \underline{r}_{j} .

Let the set {i_{1}, …, i_{m}} ⊆ I be the set of all of the different conditional probability indices used in (5.1), and let σ_{i}(x_{(1,i_{1} )} , …, x_{(2^{n} ,i_{1} )} , …, x_{(1,i_{m} )} , …, x_{(2^{n} ,i_{m} )} ), δ_{j} (x_{(1,i_{1} )} , …, x_{(2^{n} ,i_{1} )} , …, x_{(1,i_{m} )} , …, x_{(2^{n} ,i_{m} )} ) be the formulas

∑_{i′} s_{ii′} · ( ∑_{k∈I_{α_{ii′}} ∩I_{β_{ii′}}} x_{(k,n_{i′} )} ) · ( ∑_{l∈I_{β_{ii′}}} x_{(l,n_{i′} )} ) ^{−1} ⩾ r_{i},

∑_{j′} s_{jj′} · ( ∑_{k∈I_{α_{jj′}} ∩I_{β_{jj′}}} x_{(k,n_{j′} )} ) · ( ∑_{l∈I_{β_{jj′}}} x_{(l,n_{j′} )} ) ^{−1} < r_{j} .

Furthermore, let χ(x_{(1,i_{1} )} , …, x_{(2^{n} ,i_{1} )} , …, x_{(1,i_{m} )} , …, x_{(2^{n} ,i_{m} )} ) be the formula

⋀_{h∈{1,...,m}} x_{(1,i_{h} )} + ⋯ x_{(2^{n} ,i_{h} )} = 1 ∧ ⋀_{k,h} x_{(k,i_{h} )} ⩾ 0.

Then, it is easy to see that (5.1) is satisfiable iff the sentence

(5.2) ∃x_{(1,i_{1} )} …∃x_{(2^{n} ,i_{1} )} …∃x_{(1,i_{m} )} …∃x_{(2^{n} ,i_{m} )} ( ⋀_{i} σ_{i}(x̄) ∧ ⋀_{j} δ_{j} (x̄) ∧ χ(x̄))

is satisfied in the ordered field of reals. Formally, the first order language of fields does not contain “^{−1} " and “−". However, both of intended functions are definable. For instance, “^{−1} " can be defined by the formula φ(x, y):

(x = 0 → y = 1) ∧ (x ≠ 0 → xy = 1),

since the first order sentence ∀x ∃_{1}y φ(x, y) is satisfied in every field. In particular, the formula ψ(…, x^{−1} , …) holds if and only if the formula ψ(…, y, …) ∧ φ(x, y) holds. So, (5.2) may be seen as a first order formula of the language of ordered fields L_{OF} – definitions by extensions, see [8].

By a well known result [9], satisfiability of sentences of L_{OF} in the ordered field of reals is decidable. □

Let us suppose that there is only one conditional probability operator, i.e., there is only one agent. It should be noted that this logic can be embedded into the logic described in [3], which has a PSPACE containment for the decision procedure. Also, the rewriting of formulas from our logic into that logic can be accomplished in linear time:

CP (α, β) is equivalent to \frac{ω(α ∧ β)}{ω(β)} ,

which is representable in [3]. Moreover, the generalization of the logic from [3] to a multi-agent case is straightforward.

Thus, we conclude that our logic is also decidable in PSPACE.

6. Representing evidence

In [4], Halpern and Pucella presented a first-order logic for reasoning about evidence. It includes propositional formulas on hypotheses H, observations O, probabilities P_{1} and P_{2} of formulas before and after the observation, the evidence E(o, h) provided by the observation o for the hypothesis h, and quantification by real-valued variables. They posed an open question whether it is possible to axiomatize their logic without resorting to quantification. Intuitively, the evidence function e represents the “weight" that an observation leads to the fulfillment of a hypothesis. In [4], it was shown that the evidence can be seen as a function which maps prior probability P_{1} to posterior probability P_{2}, using Dempster’s Rule of Combination. For more details, we refer reader to [4].

In this section we will show how evidence can be represented in the developed logic. We will introduce the following modifications:

(1) there is a finite number of propositional letters divided into two categories: Var = H ∪ O, where H = {h_{1}, …, h_{m}} are used to denote hypotheses, O = {o_{1}, …, o_{n}} are used to denote observations, and H ∩ O = ∅;

(2) there are only two conditional probability operators – CP_{1} and CP_{2}, which will be interpreted as prior and posterior conditional probabilities, respectively;

(3) there is an additional syntactic object – E(o, h), where o ∈ O, h ∈ H;

(4) the definition of Term(0) is adjusted accordingly to: Term(0) = \{\underline{s} | s ∈ ℚ} ∪ {CP_{i}(α, β) | α, β ∈ For_{C}, i ∈ I} ∪ {E(o, h) | o ∈ O, h ∈ H};

(5) The definition of a model is extended to: ⟨W, H, {μ_{i}|i ∈ I}, v, e⟩, where e : ({[o]|o ∈ O} × [{[h]|h ∈ H}]) → [0, 1] by the formula

e([o], [h]) = \frac{μ_{1}([o ∧ h]) · μ_{1}([h])^{−1}}{∑ _{k=1}^{m} μ_{1}([o ∧ h_{k}]) · μ_{1}([h_{k}])^{−1}} , for o ∈ O, h ∈ H ;

(6) The definition of satisfiability is extended to include: E(o, h)^{M} = (CP_{1}(o, h)^{M}) · (∑ _{k=1}^{m} CP_{1}(o, h_{k})^{M})^{−1} , for o ∈ O, h ∈ H;

(7) there are nine additional axioms:

A31. (⋁ _{i=1}^{m} h_{i}) ∧ (⋀ _{i≠j} (h_{i} → ¬h_{j})), A32. (⋁ _{i=1}^{n} o_{i}) ∧ (⋀ _{i≠j} (o_{i} → ¬o_{j})), A33. ⋀ _{i=1}^{n} (CP_{1}(o_{i}, h_{1}) + ⋯+ CP_{1}(o_{i}, h_{m}) > 0), A34. (CP_{1}(o_{i}, h_{j}) ⩾ r ∧ CP_{1}(o_{i}, h_{1}) + ⋯+ CP_{1}(o_{i}, h_{m}) ⩽ s) → E(o_{i}, h_{j}) ⩾ \frac{r}{s} , A35. (CP_{1}(o_{i}, h_{j}) ⩾ r ∧ CP_{1}(o_{i}, h_{1}) + ⋯+ CP_{1}(o_{i}, h_{m}) < s) → E(o_{i}, h_{j}) > \frac{r}{s} , A36. (CP_{1}(o_{i}, h_{j}) > r ∧ CP_{1}(o_{i}, h_{1}) + ⋯+ CP_{1}(o_{i}, h_{m}) ⩽ s) → E(o_{i}, h_{j}) > \frac{r}{s} , A37. (CP_{1}(o_{i}, h_{j}) ⩽ r ∧ CP_{1}(o_{i}, h_{1}) + ⋯+ CP_{1}(o_{i}, h_{m}) ⩾ s) → E(o_{i}, h_{j}) ⩽ \frac{r}{s} , A38. (CP_{1}(o_{i}, h_{j}) ⩽ r ∧ CP_{1}(o_{i}, h_{1}) + ⋯+ CP_{1}(o_{i}, h_{m}) > s) → E(o_{i}, h_{j}) < \frac{r}{s} , A39. (CP_{1}(o_{i}, h_{j}) < r ∧ CP_{1}(o_{i}, h_{1}) + ⋯+ CP_{1}(o_{i}, h_{m}) ⩾ s) → E(o_{i}, h_{j}) < \frac{r}{s} ,

(8) there is one additional inference rule:

R4: \frac{o_{i}}{P_{2}(h_{j}) = CP_{1}(h_{j} |o_{i})} , i ∈ \{1, …, n\}, j ∈ \{1, …, m\}.

It can be shown, very similarly to the already laid-out proofs, that the logic with these modifications in place is also strongly complete and decidable in PSPACE.

In this way, we have solved the problem of propositional axiomatization of reasoning about evidence, which was presented in [4].

7. Conclusion

In this paper, we introduced a sound and strongly-complete axiomatic system for the probabilistic logic with conditional probability operators CP_{i}, i ∈ I, which allows for linear combinations and comparative statements. As it was noticed in [10], it is not possible to give a finitary strongly complete axiomatization for such a system. In our case the strong completeness was made possible by adding an infinitary rule of inference.

The obtained formalism is quite expressive and allows for the representation of uncertain knowledge, where uncertainty is modelled by probability formulas, as well as for the representation of evidence. For instance, a conditional statement of the form “the sum of probabilities of α given β and γ given δ is at least 0.95, viewed by agent i" can be written as CP_{i}(α, β) + CP_{i}(γ, δ) ⩾ \underline{0.95}. A similar approach can be applied to de Finetti style conditional probabilities. Future research will also consider a possibility of dealing with probabilistic first-order formulas.

Acknowledgements. The authors would like to thank an anonymous referee, whose valuable comments, suggestions and insights have contributed to the detection of several errors and discrepancies in the earlier versions, as well as to the improvement of the quality of this paper.

References

[1] P. Maksimović, D. Doder, B. Marinković and A. Perović, A logic with a conditional probability operator; in: K. Balogh (ed.), Proc. 13^{th} ESSLLI Student Session, Hamburg, 2008, 105–114.

[2] Z. Ognjanović, M. Rašković and Z. Marković, Probability logics; in: Logic in computer science, Mathematički institut SANU, Beograd, 2009, 35–111, [3] R. Fagin, J. Y. Halpern and N. Megiddo, A logic for reasoning about probabilities, Inf. Comput.

87(1–2) (1990), 78–128.

[4] J. Y. Halpern and R. Pucella, A logic for reasoning about evidence J. Art. Intell. Res. (JAIR) 26 (2006), 1–34.

[5] T. Lukasiewicz, Probabilistic Default Reasoning with Conditional Constraints, Ann. Math. Art. Intell. 34(1–3) (2002), 35–88.

[6] M. Rašković, Z. Ognjanović and Z. Marković, A logic with Conditional Probabilities, Lect. Notes Comput. Sci. 3229, 2004, 226–238.

[7] Z. Ognjanović, Z. Marković and M. Rašković, Completeness Theorem for a Logic with imprecise and conditional probabilities, Publ. Inst. Math., Nouv. Sér. 78(92) (2005), 35–49.

[8] J. R. Shoenfield, Mathematical Logic, Peters, 2001.

[9] D. Marker, Model Theory: an Introduction, Springer-Verlag, 2002.

[10] W. van der Hoek, Some considerations on the logic P_{F} D: a logic combining modality and probability, J. Appl. Non-class. Log. 7(3) (1997), 287–307.

Faculty of Mechanical Engineering (Received 04 08 2009) University of Belgrade (Revised 26 03 2010) Kraljice Marije 16 11120 Belgrade Serbia

ddoder@mas.bg.ac.rs

Mathematical Institute SANU Kneza Mihaila 36 11001 Belgrade Serbia

  bojanm@mi.sanu.ac.rs
petarmax@mi.sanu.ac.rs

Faculty of Traffic Engineering University of Belgrade Vojvode Stepe 305 11000 Belgrade Serbia

pera@sf.bg.ac.rs