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

A LOGIC FOR REASONING ABOUT QUALITATIVE PROBABILITY

Angelina Ilić-Stepić

Communicated by Žarko Mijajlović

Abstract. We offer extended completeness theorem for probabilistic logic that combines higher-order probabilities (nesting of probability operators) and the qualitative probability operator.

1. Introduction

Qualitative reasoning uses binary relations on events (formulas) instead of exact numerical representations of realizations of events (probabilities, degrees of belief etc). For example, an agent (or expert in some field) will often state something like “A is at least as probable as B", or “A is more probable than B" without any explicit reference to the values of probabilities corresponding to A and B.

There are many relevant papers regarding the subject of qualitative reasoning. For the possibility theory (qualitative possibility and necessity relations), we refer the reader to [1, 2, 3, 5, 8]; for qualitative probability and probabilistic logic in general, we refer the reader to [4, 6, 7, 9, 10, 11, 12, 13, 14, 15, 16, 19, 20, 21, 22, 23, 24].

Here we present a probabilistic logic that combines higher order probabilities (nesting of probability operators) and the qualitative probability operator. The main result is the proof of the extended completeness theorem (every consistent set of formulas is satisfiable) for the introduced logic. Our methodology is based on the results presented in [12, 15, 16]. Syntactically, instead of countably many probability operators of the form P_{⩾r}A (it reads “the probability of A is at least r"), we use rational numbers from the real unit interval as truth constants (similarly as in [18]) and the qualitative probability operator ⪰. For instance, the above P_{⩾r}A we formally express by A ⪰ r, where r is the name for r ∈ [0, 1] ∩ ℚ. Due to the modal nature of ⪰, the standard probabilistic Kripke structures were used for the definition of satisfiability.

2010 Mathematics Subject Classification: 03B50.

The rest of the paper is organized as follows: syntax and semantics are discussed in Section 2; axioms and inference rules are given in Section 3; extended completeness theorem is proved in Section 4; decidability of the introduced logic is proved in Section 5; concluding remarks are in the last section.

2. Syntax and semantics

Let I denotes the set of all rational numbers from the unit interval. We use L_{⪰} to denote our logic. The language of the logic consists of:

• a denumerable set Var = {p, q, r …}

• classical connectives ¬ and ∧

• a binary operator ⪰ The set For_{L_{⪰}} of formulas is defined as follows:

Definition 2.1. (For_{L_{⪰}} )

• If p ∈ Var, then p is formula.

• If α, β are formulas and r ∈ I, then (¬α), (α ∧ β), (α ⪰ r) and (α ⪰ β) are formulas.

The other classical connectives (∨, →, ↔) can be defined as usual. We use notation r ⪯ α for α ⪰ r. We also denote (¬α) ⪰ 1 − r by α ⪯ r, α ⪯ r ∧ ¬(r ⪯ α) by α ≺ r and ¬(α ⪯ r) by α ≻ r. Therefore, r ⪰ α means α ⪯ r. Similarly if α and β are formulas, then we use notation α ⪯ β for β ⪰ α, α ≻ β denotes ¬(α ⪯ β) and α ≺ β means β ≻ α. We also denote α ⪰ β ∧ β ⪰ α by α ≍ β. Finally, we use ⊥ do denote α ∧ ¬α.

Definition 2.2. An L_{⪰} model is a structure M = ⟨W, Prob, v⟩ where: • W is a nonempty set of elements called worlds.

• Prob is probability assignment which assigns to every w ∈ W a probability

space Prob(w) = ⟨W (w), H(w), μ(w)⟩, where:

− W (w) is a nonempty subset of W

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

− μ(w) : H(w) → [0, 1] is a finitely additive probability measure, and • v : W × Var → {⊤, ⊥} is a valuation which associates with every world

w ∈ W a truth assignment v(w) on the propositional letters.

Definition 2.3. Let M = ⟨W, Prob, v⟩ be an L_{⪰} model and w ∈ W. The satisfiability relation is inductively defined as follows:

• If p ∈ Var, then (w, M) ⊨ p iff v(w)(p) = ⊤.

• If α ∈ For_{L_{⪰}} , then (w, M) ⊨ ¬α iff it is not (w, M) ⊨ α.

• If α, β ∈ For_{L_{⪰}} , then (w, M) ⊨ α ∧ β iff (w, M) ⊨ α and (w, M) ⊨ β.

• If α ∈ For_{L_{⪰}} and r ∈ I, then (w, M) ⊨ α ⪰ r iff μ(w)({w′ ∈ W (w) | w′ ⊨ α}) ⩾ r.

• If α, β ∈ For_{L_{⪰}} , then (w, M) ⊨ α ⪰ β iff μ(w)({w′ ∈ W (w) | w′ ⊨ α}) ⩾ μ(w)({w′ ∈ W (w) | w′ ⊨ β})

In the sequel, we will omit M from (w, M) ⊨ α and write w ⊨ α if M is clear from the context. In an L_{⪰} model M = ⟨W, Prob, v⟩ the set {w′ ∈ W (w) | w′ ⊨ α} is denoted by [α]_{M,w} or just by [α]_{w}.

A set of formulas T is L_{⪰} satisfiable if there is a world w in an L_{⪰} model M such that for every formula α ∈ T, w ⊨ α. A formula α is L_{⪰} satisfiable if the set {α} is L_{⪰} satisfiable. A formula α is L_{⪰} valid in an L_{⪰} model M = ⟨W, Prob, v⟩ (denoted by ⊨_{M} α) if it is satisfiable in each world of M. A formula α is L_{⪰} valid (denoted by ⊨ α) if it is satisfiable in each world in each model.

3. Axiomatization

The axiom system AX_{L_{⪰}} involves eleven axiom schemas:

A1: Substitutional instances of tautologies.

A2: α ⪰ 0

A3: α ⪰ s → α ⪰ r, s ⩾ r

A4: α ⪰ β ∨ β ⪰ α

A5: α ⪰ β ∧ β ⪰ γ → α ⪰ γ A6: α ⪰ β ∧ β ≻ γ → α ≻ γ A7: (α ⪰ r ∧ β ⪰ s ∧ (α ∧ β ≍ 0)) → (α ∨ β ⪰ r + s) A8: α ⪯ r ∧ β ⪯ s → α ∨ β ⪯ r + s A9: α ⪯ r ∧ β ≺ s → α ∨ β ≺ r + s, r + s ⩽ 1 A10: α ≺ r → α ⪯ r A11: α ⪰ s → α ≻ r, s > r

and inference rules:

(1) From α and α → β infer β

(2) From α infer α ≍ 1

(3) From α → (β ⪰ r − 1/n), for every n ∈ N, n ⩾ \frac{1}{r}, infer α → (β ⪰ r)

(4) From γ → (β ⪰ r → α ⪰ r), for every r ∈ I, infer γ → (α ⪰ β) We denote this axiomatic system by Ax_{L_{⪰}} . A formula α is a theorem (⊢ α) if there is an at most denumerable sequence (called proof) of formulas α_{0}, α_{1}, …, α such that every α_{i} is an axiom or it is derived from the preceding formulas by an inference rule. A formula α is deducible from the set T of formulas (denoted T ⊢_{Ax_{L_{⪰}}} α) if there is an at most denumerable sequence (called proof) 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, with the exception that Rule 2 can be applied only to theorems. T ⊬_{Ax_{L_{⪰}}} α means that T ⊢_{Ax_{L_{⪰}}} α does not hold. A set of formulas T is consistent if there is at least one formula α such that T ⊬_{Ax_{L_{⪰}}} α. A consistent set T of formulas is said to be maximal consistent if for every formula α either α ∈ T or ¬α ∈ T. A set T is deductively closed if for every formula α if T ⊢ α, then α ∈ T.

4. Soundness and completeness

Theorem 4.1 (Deduction theorem). If T is a set of formulas and T ∪{α} ⊢ β, then T ⊢ α → β

Proof. We use transfinite induction of the length of the inference. There are the following cases:

Case 1: β is obtained from γ and γ → β by an application of Rule 1. Then, by induction hypothesis T ⊢ α → γ and T ⊢ α → (γ → β). Since (α → (γ → β)) → ((α → γ) → (α → β)) is tautology, using Rule 1 two times we obtain T ⊢ α → β.

Case 2: Let β be formula (γ ≍ 1) obtained from γ. In that case γ must be a theorem and therefore β is theorem. Then, from ⊢ β → (α → β), using Rule 1 we obtain T ⊢ α → β.

Case 3: Suppose that β = γ → (δ ⪰ r) is obtained from T, α by an application of Rule 3. Then:

T, α ⊢ γ → (δ ⪰ r − 1/n) for every n ⩾ \frac{1}{r} T ⊢ α → (γ → (δ ⪰ r − 1/n)) for every n ⩾ \frac{1}{r}, by the induction hypothesis T ⊢ (α ∧ γ) → (δ ⪰ r − 1/n) for every n ⩾ \frac{1}{r}

by classical tautology (α → (β → γ)) ↔ ((α ∧ β) → γ) T ⊢ (α ∧ γ) → (δ ⪰ r), by Rule 3. T ⊢ α → (γ → δ ⪰ r) T ⊢ α → β. Case 4: Suppose that β = γ → (δ ⪰ ϵ) is obtained from T, α by an application

of Rule 4. Then:

T, α ⊢ γ → (δ ⪰ r → ϵ ⪰ r) for every r ∈ I T, α ⊢ (γ ∧ (δ ⪰ r)) → ϵ ⪰ r for every r ∈ I T ⊢ α → ((γ ∧ (δ ⪰ r)) → ϵ ⪰ r) for every r ∈ I, by the case 3 T ⊢ α → (γ → (δ ⪰ r → ϵ ⪰ r)) for every r ∈ I T ⊢ (α ∧ γ) → (δ ⪰ r → ϵ ⪰ r) for every r ∈ I T ⊢ (α ∧ γ) → (δ ⪰ ϵ) by the Rule 4. T ⊢ α → (γ → (δ ⪰ ϵ)) T ⊢ α → β □

Theorem 4.2. Every consistent set can be extended to a maximal consistent set.

Proof. Let T be a consistent theory (set of formulas) and let θ_{0}, θ_{1}, … be an enumeration of all formulas. We define a sequence of theories T_{i} in the following way:

(1) T_{0} = T

(2) For every n ⩾ 0,

(a) If T_{n} ∪ θ_{n} is consistent, then T_{n+1} = T_{n} ∪ θ_{n}.

(b) Otherwise, if θ_{n} is formula θ → A ⪰ r, then T_{n+1} = T_{n} ∪ {¬θ_{n}, θ → A ≺ r − 1/n\}, for some integer n, n > \frac{1}{r} so that T_{n+1} is consistent.

(c) Otherwise, if θ_{n} is formula γ → (ϵ ⪰ δ), then T_{n+1} = T_{n} ∪ {¬θ_{n}, γ → (δ ⪰ r ∧ ϵ ≺ r)}, for some r ∈ I so that T_{n+1} is consistent.

(d) Otherwise, T_{n+1} = T_{n} ∪ {¬θ_{n}}.

The sets obtained by the steps 1 and 2a are obviously consistent. The step 2d produces consistent sets, too. For, if T_{n}, θ_{n} ⊢⊥, by Deduction Theorem we have T_{n} ⊢ ¬θ_{n}, and since T_{n} is consistent so is T_{n} ∪ {¬θ_{n}}.

Let us first consider step 2b. Suppose that for every integer n, n > \frac{1}{r}, T_{n+1} = T_{n} ∪ {¬(θ → α ⪰ r), θ → α ≺ r − 1/n} is inconsistent. Then:

T_{n}, ¬(θ → α ⪰ r), θ → α ≺ r − 1/n ⊢⊥ for every integer n, n > \frac{1}{r}. T_{n}, ¬(θ → α ⪰ r) ⊢ (θ → α ≺ r − 1/n) →⊥ for every integer n, n > \frac{1}{r}, by Deduction theorem. T_{n}, ¬(θ → α ⪰ r) ⊢ ¬(θ → α ≺ r − 1/n) for every integer n, n > \frac{1}{r}. T_{n}, ¬(θ → α ⪰ r) ⊢ θ ∧ ¬(α ≺ r − 1/n) for every integer n, n > \frac{1}{r}, by classical reasoning. T_{n}, ¬(θ → α ⪰ r) ⊢ θ ∧ (α ⪰ r − 1/n) for every integer n, n > \frac{1}{r}. T_{n}, ¬(θ → α ⪰ r) ⊢ θ → (α ⪰ r − 1/n) for every integer n, n > \frac{1}{r}, by classical tautology α ∧ β → (α → β) T_{n}, ¬(θ → α ⪰ r) ⊢ θ → (α ⪰ r) by Rule 3 T_{n} ⊢ ¬(θ → α ⪰ r) → (θ → (α ⪰ r)), by Deduction theorem. T_{n} ⊢ (θ → α ⪰ r), by classical reasoning, which contradicts consistency of T_{n}

since T_{n} ∪ {θ → (α ⪰ r)} is not consistent.

Next, consider step 2c. Suppose that for every r ∈ I set

T_{n+1} = T_{n} ∪ {¬(γ → (ϵ ⪰ δ)), γ → (δ ⪰ r ∧ ϵ ≺ r)}

is inconsistent. Then:

T_{n}, ¬(γ → (ϵ ⪰ δ)), {γ → (δ ⪰ r ∧ ϵ ≺ r)} ⊢⊥, for every r ∈ I, r > 0. T_{n}, ¬(γ → (ϵ ⪰ δ)) ⊢ (γ → (δ ⪰ r ∧ ϵ ≺ r)) →⊥, for every r ∈ I, r > 0, by Deduction theorem. T_{n}, ¬(γ → (ϵ ⪰ δ)) ⊢ ¬(γ → (δ ⪰ r ∧ ϵ ≺ r)), for every r ∈ I, r > 0. T_{n}, ¬(γ → (ϵ ⪰ δ)) ⊢ (γ ∧ ¬(δ ⪰ r ∧ ϵ ≺ r)) for every r ∈ I, r > 0. T_{n}, ¬(γ → (ϵ ⪰ δ)) ⊢ (γ ∧ (¬(δ ⪰ r) ∨ ¬(ϵ ≺ r))) for every r ∈ I, r > 0. T_{n}, ¬(γ → (ϵ ⪰ δ)) ⊢ γ ∧ (δ ⪰ r → ϵ ⪰ r) for every r ∈ I, r > 0, by classical reasoning. T_{n}, ¬(γ → (ϵ ⪰ δ)) ⊢ γ → (δ ⪰ r → ϵ ⪰ r) for every r ∈ I, r > 0, by classical tautology (α ∧ β) → (α → β) T_{n}, ¬(γ → (ϵ ⪰ δ)) ⊢ γ → (ϵ ⪰ δ), by Rule 4 T_{n} ⊢ ¬(γ → (ϵ ⪰ δ)) → (γ → (ϵ ⪰ δ)), by Deduction theorem. T_{n} ⊢ γ → (ϵ ⪰ δ), by classical reasoning, which contradicts consistency of T_{n}

since T_{n} ∪ {γ → (ϵ ⪰ δ)} is not consistent.

Let T^{∗} = ⋃ _{n<ω} T_{n}. We have to prove that T^{∗} is maximal consistent. The steps 2a–2d guarantee that for every formula θ, θ or ¬θ belongs to T^{∗}, i.e.,

that T^{∗} is maximal. On the other hand, there is no formula θ, such that θ and ¬θ belongs to T^{∗}. To prove that, suppose that θ = θ_{n} and ¬θ = θ_{m} for some n and m. If θ, ¬θ ∈ T^{∗}„ then also θ, ¬θ ∈ T_{max (n,m)+1} , a contradiction with the consistency if T_{max (n,m)+1} .

We continue by showing that T^{∗} is deductively closed, and since it does not contain all formulas, it follows that T^{∗} is consistent.

Next, we can show that if for some n, T_{n} ⊢ θ, it must be θ ∈ T^{∗}. Suppose that it is not the case. Then, ¬θ ∈ T^{∗} so there must be some k such that T_{k} ⊢ θ and T_{k} ⊢ ¬θ which contradicts the consistency of T_{k}.

Let the sequence θ_{1}, θ_{2} …θ form a proof of θ in T^{∗}. If the sequence is finite, there must be a set T_{n} such that T_{n} ⊢ θ and θ ∈ T^{∗}. Thus suppose that the sequence is countably infinite. We can show that for every n, if θ_{n} is obtained by an application of an inference rule, and all premises belong to T^{∗}, then there must be θ_{n} ∈ T^{∗}. If the rule is a finitary one, then there must be a set T_{m} which contains all premises and T_{m} ⊢ θ_{n}. Reasoning as above, we conclude that θ_{n} ∈ T^{∗}.

So, let us now consider the infinitary rules. Let θ_{m} = α → (β ⪰ r) be obtained from the set of premises {θ_{m}^{n} | n > 1/r} by Rule 3, where θ_{m}^{n} is the formula α → (β ⪰ r − 1/n). Suppose that θ_{m} ∉ T^{∗}. By the induction hypothesis, θ_{m}^{n} ∈ T^{∗} for every n. By the step 2b of the construction there must be some n and some l such that α → (β ≺ r − 1/n) belongs to T_{l}. It follows that there must be some j such that α → (β ≺ r − 1/n) and α → (β ⪰ r − 1/n) belongs to T_{j}. Then T_{j} ⊢ α →⊥ and T_{j} ⊢ α → (β ⪰ r). It follows that θ_{m} ∈ T^{∗}, a contradiction.

Let θ_{m} = γ → (α ⪰ β) be obtained from the set of premises {θ_{m}^{r} | r ∈ I} by Rule 4, where θ_{m}^{r} is the formula γ → (β ⪰ r → α ⪰ r). Suppose that θ_{m} ∉ T^{∗}. By the induction hypothesis, θ_{m}^{r} ∈ T^{∗} for every r. By the step 2c of the construction there must be some r and some l such that γ → (β ⪰ r ∧ α ≺ r) belongs to T_{l}. It follows that there must be some j such that γ → (β ⪰ r → α ⪰ r} and γ → (β ⪰ r ∧ α ≺ r) belongs to T_{j}. Then T_{j} ⊢ γ →⊥ and T_{j} ⊢ γ → (α ⪰ β). It follows that θ_{m} ∈ T^{∗}, a contradiction. □

Theorem 4.3. Let α, β ∈ For_{L_{⪰}} , r, s ∈ I and suppose that T is a maximal consistent set of formulas. Then:

(1) T ⊢ α ⪰ β → (β ⪰ r → α ⪰ r); (2) α ∧ β ∈ T iff α ∈ T and β ∈ T.

Proof. (1) T ⊢ α ⪰ β ∧ β ⪰ r → α ⪰ r by A5

T ⊢ ¬(α ⪰ β ∧ β ⪰ r) ∨ α ⪰ r
T ⊢ ¬(α ⪰ β) ∨ (¬(β ⪰ r) ∨ α ⪰ r)
T ⊢ α ⪰ β → (β ⪰ r → α ⪰ r) by classical reasoning.

(2) Suppose that α ∈ T and β ∈ T. Then:

T ⊢ α T ⊢ β T ⊢ α ∧ β and since T is deductively closed α ∧ β ∈ T.

Let α ∧ β ∈ T. Then:

T ⊢ α ∧ β T ⊢ (α ∧ β) → α T ⊢ (α ∧ β) → β and using Rule 1 T ⊢ α T ⊢ β and since T is deductively closed α ∈ T and β ∈ T. □

Let the tuple M = ⟨W, Prob, v⟩ be defined as follows:

• W is the set of all maximal consistent set of formulas,

• If α ∈ For_{L_{⪰}} , then [α] = {w ∈ W | α ∈ W }

• v is a valuation which associated with every world w ∈ W a truth assignment v(w) : Var → {⊤, ⊥} such that for every p ∈ Var, v(w)(p) = ⊤ iff p ∈ w.

• For every world w ∈ W, Prob(w) is defined as follows: − W (w) = W − H(w) is a class of all sets of the form [α] = {w ∈ W | α ∈ w} for all α ∈ For_{L_{⪰}} − μ(w)([α]) = sup{r | α ⪰ r ∈ w}

Theorem 4.4. Let M = ⟨W, Prob, v⟩ be defined as above. Then the following hold for every w ∈ W.

(1) if ⊢ α ≍ β, then μ(w)([α]) = μ(w)([β]).

(2) μ(w)([α]) ⩾ 0, α ∈ For_{L_{⪰}}
(3) μ(w)([¬α]) = 1 − μ(w)([α])
(4) if ⊢ α ∧ β ≍ 0, then μ(w)([α ∨ β]) = μ(w)([α]) + μ(w)([β]).
(5) If ⊢ α → β, then μ(w)([α]) ⩽ μ(w)([β]).
(6) ⊢ α ⪰ β iff μ(w)([α]) ⩾ μ(w)([β]).
(7) If ⊢ (α ↔ β) ≍ 1, then μ(w)([α]) = μ(w)([β]).
(8) If [α] = [β], then ⊢ α ↔ β.
(9) If [α] = [β], then μ(w)([α]) = μ(w)([β]).
Proof. (1) ⊢ α ≍ β i.e.,

⊢ α ⪰ β ∧ β ⪰ α

⊢ α ⪰ β by classical reasoning.

⊢ α ⪰ β → (β ⪰ r → α ⪰ r) for every r ∈ I, by Theorem 4.3, so ⊢ β ⪰ r → α ⪰ r, for every r ∈ I.

Therefore if β ⪰ r ∈ w, then α ⪰ r ∈ w. In the same way we can conclude the opposite, i.e., if α ⪰ r ∈ w, then β ⪰ r ∈ w. Thus {r |α ⪰ r ∈ w} = {r | β ⪰ r ∈ w} and consequently sup{r | α ⪰ r ∈ w} = sup{r | β ⪰ r ∈ w}.

(2) Obvious, according to A2.

(3) Let r = sup{t | α ⪰ t ∈ w}. If r = 1, then α ⪰ 1 ∈ w, i.e., (¬α) ⪯ 0 ∈ w. Then, by A2, (¬α) ⪰ 0 ∈ w. If for some s > 0, (¬α) ⪰ s ∈ w, then by A11 (¬α) ≻ 0 ∈ w, a contradiction. Therefore μ(w)[¬α] = 0.

Suppose that r < 1. Then, for every r′ ∈ (r, 1], ¬(α ⪰ r′) ∈ w, i.e., α ≺ r′ ∈ T. By A10, α ⪯ r′ ∈ w so (¬α) ⪰ 1 − r′ ∈ w. If there exists r′′ ∈ [0, r) such that (¬α) ⪰ 1 − r′′ ∈ w, then ¬(α ≻ r′′) ∈ w which is a contradiction. Therefore, sup{t | (¬α) ⪰ t ∈ w} = 1 − sup{t | α ⪰ t ∈ w}.

(4) By A7, μ(w)([α ∨ β]) ⩾ r + s for any r and s such that α ⪰ r ∈ w and β ⪰ s ∈ w. Therefore μ(w)([α ∨ β]) ⩾ sup{r | α ⪰ r ∈ w} + sup{s | β ⪰ s ∈ w} so μ(w)([α ∨ β]) ⩾ μ(w)([α]) + μ(w)([β]).

Suppose that μ(w)([α]) = r_{0} and μ(w)([β]) = s_{0}. If r_{0} + s_{0} = 1, then equality obviously hold. Let r_{0} + s_{0} < 1. Suppose that r_{0} + s_{0} < μ(w)([α ∨ β]). Then, r_{0} + s_{0} < t_{0} = sup{t | α ∨ β ⪰ t ∈ w}. If t′ ∈ (r_{0} + s_{0}, t_{0}) is any rational number, then α ∨ β ⪰ t′ ∈ w. Let r′ > r_{0} and s′ > s_{0} be rational numbers such that r′+ s′ = t′ < 1, α ≺ r′ ∈ w and β ≺ s′ ∈ w. By A10, α ⪯ r′ ∈ w and finally, by A9, α ∨ β ≺ r′+ s′ ∈ w, i.e., α ∨ β ≺ t′ ∈ w, which is a contradiction.

(5) Let ⊢ α → β. Suppose the contrary, i.e., μ(w)([α]) > μ(w)([β]). Then there exists r ∈ I such that α ⪰ r ∈ w and β ⪰ r ∉ w. Therefore β ≺ r ∈ w. Then:

⊢ α → β by assumption ⊢ α → β ≍ 1 by Rule 2.

⊢ ¬α ∨ β ⪰ 1 by classical tautology ⊢ α ∧ β → α. Therefore ⊢ ¬α ∨ β ⪰ 1 ∧ ¬α ⪯ 1 − r ∧ β ≺ r ⊢ ¬α ⪯ 1 − r ∧ β ≺ r → ¬α ∨ β ⪰ 1 by classical tautology α ∧ β → (α → β). Applying A9 we have: ⊢ ¬α ⪯ 1 − r ∧ β ≺ r → ¬α ∨ β ≺ 1, a contradiction.

(6) (⇐) Let μ(w)(α)⩾μ(w)(β). Then sup{r |α ⪰ r ∈ w} ⩾ sup{r |β ⪰ r ∈ w}. Suppose that α ⪰ β ∉ w. Then there exists r_{0} ∈ I such that β ⪰ r_{0} ∧ α ≺ r_{0} ∈ w. Therefore, sup{r | α ⪰ r ∈ w} ⩾ sup{r | β ⪰ r ∈ w} ⩾ r_{0}, so there exists r ⩾ r_{0} such that α ⪰ r ∈ w. However, by A3 ⊢ α ⪰ r → α ⪰ r_{0} and therefore by Rule 1, ⊢ α ⪰ r_{0}, a contradiction.

(⇒). Let ⊢ α ⪰ β. Then: ⊢ α ⪰ β → (β ⪰ r → α ⪰ r) for every r ∈ I, by Theorem 4.3. ⊢ (β ⪰ r → α ⪰ r) for every r ∈ I, by Rule 1. So, for every r ∈ I, if β ⪰ r ∈ w, then α ⪰ r ∈ w and consequently sup{r | α ⪰

r ∈ w} ⩾ sup{r | B ⪰ r ∈ w}, i.e., μ(w)(α) ⩾ μ(w)(β).

(7) Suppose the contrary, for example μ(w)([α]) > μ(w)([β]). Then there exists r ∈ I such that α ⪰ r ∈ w and β ⪰ r ∉ w. Therefore β ≺ r ∈ w. Then:

⊢ α ↔ β ≍ 1, i.e., ⊢ α ↔ β ⪰ 1 ∧ 1 ⪰ α ↔ β ⊢ α ↔ β ⪰ 1, by classical tautology α ∧ β → α ⊢ (¬α ∨ β) ∧ (¬β ∨ α) ⪰ 1. Therefore, by (6), μ(w)[((¬α ∨ β) ∧ (¬β ∨ α))] ⩾ 1. Since ⊢ (¬α ∨ β) ∧ (¬β ∨ α) → (¬α ∨ β), according to (5), we have that

μ(w)[((¬α ∨ β) ∧ (¬β ∨ α))] ⩽ μ(w)[(¬α ∨ β)]. Therefore, μ(w)(¬α ∨ β) ⩾ 1. Now, according to (6), ⊢ ¬α ∨ β ⪰ 1. The rest of the proof is the same as in (5).

(8) Suppose that [α] ⊆ [β]. Then {w | α ∈ w} ⊆ {w | β ∈ w}, i.e., for every w, if α ∈ w, then β ∈ w. Therefore, if w is a maximal consistent set, then, if w ⊢ α, then w ⊢ β, i.e., w ⊢ α → β. According to this, there is no maximal consistent set w such that ¬(α → β) ∈ w. Therefore, α ∧ ¬β is inconsistent so α ∧ ¬β ⊢ ⊥ i.e., ⊢ α → β. If [α] = [β], then [α] ⊆ [β] and [β] ⊆ [α] so ⊢ α → β and β → α and therefore ⊢ α ↔ β.

(9) If [α] = [β], then by 8, ⊢ α ↔ β, so applying Rule 2 we have ⊢ α ↔ β ≍ 1. Therefore, according to (7) we have μ(w)([α]) = μ(w)([β]). □

Theorem 4.5. A set of formulas is consistent with respect to L_{⪰} iff it has an L_{⪰} model.

Proof. (⇐) Since L_{⪰} is sound, a satisfiable set of formulas is consistent. (⇒). In order to prove this direction we construct a canonical model M =

⟨W, Prob, v⟩ as above and show, by induction on complexity of formulas, that for every world w and every formula α, w ⊨ α iff α ∈ w.

• w ⊨ p iff v(w)(p) = ⊤ iff p ∈ w (by definition of canonical model).

• w ⊨ ¬α iff it is not w ⊨ α iff α ∉ w iff ¬α ∈ w.

• w ⊨ α ∧ β iff w ⊨ α and w ⊨ β iff α ∈ w and β ∈ w iff α ∧ β ∈ w (by Theorem 3).

• Let α ⪰ r ∈ w. Then sup{s | α ⪰ s ∈ w} ⩾ r, i.e., μ(w)[α] ⩾ r and therefore w ⊨ α ⪰ r. Let w ⊨ α ⪰ r. Then sup{s | α ⪰ s ∈ w} ⩾ r. If sup{s|α ⪰ s ∈ w} = r, then according to Rule 3 and the fact that w is deductively closed, w ⊢ α ⪰ r, i.e., α ⪰ r ∈ w. Otherwise, if sup{s | α ⪰ s ∈ w} = μ(w)([α]) > r, then according to the properties of supremum and monotonous of function μ(w), α ⪰ r ∈ w.

• Suppose that α ⪰ β ∈ w. Then w ⊢ α ⪰ β and according to Theorem 4.3 and Rule 1 for every r ∈ I, w ⊢ β ⪰ r → α ⪰ r. Then, for every r ∈ I, if β ⪰ r ∈ w, then α ⪰ r ∈ w. Therefore, sup{s | α ⪰ s ∈ w} ⩾ sup{s | β ⪰ s ∈ w}, i.e., μ(w)([α]) ⩾ μ(w)([β]) so w ⊨ α ⪰ β.

Let w ⊨ α ⪰ β. Therefore μ(w)([α]) ⩾ μ(w)([β]), i.e., sup{s | α ⪰ s ∈ w} ⩾ sup{s | β ⪰ s ∈ w}. Then, according to the properties of supremum, for every r ∈ I, if β ⪰ r ∈ w, then α ⪰ r ∈ w. Now, for every, r ∈ I, w ⊢ β ⪰ r → α ⪰ r. Therefore, according to Rule 4, w ⊢ α ⪰ β, i.e., α ⪰ β ∈ w. □

5. Decidability

In this section we are analyzing decidability of the satisfiability problem for the class L_{⪰} .

Theorem 5.1. If a formula α is satisfiable, then it is satisfiable in an L_{⪰} model with a finite number of worlds. The number of worlds in that model is at most 2^{k}, where k denotes the number of subformulas of α.

Proof. Suppose that α holds in a world of an L_{⪰} model M= ⟨W, Prob, v⟩. Let Subf(α) denote the set of all subformulas of α and k = | Subf(α)|. Let ≈ denote the equivalence relation over W^{2}, such that w ≈ u iff for every β ∈ Subf(α), w ⊨ β iff u ⊨ β. The quotient set W_{/≈} is finite. From every class C_{i} we choose an element and denote it w_{i}. We consider the model M^{∗} = ⟨W^{∗}, Prob^{∗}, v^{∗}⟩, where:

• W^{∗} = {w_{i}}.

• Prob^{∗} is defined as follows:

− W^{∗} = {w_{j} ∈ W^{∗} : (∃u ∈ C_{w_{j}} )u ∈ W (w_{i})} − H^{∗}(w_{i}) is the powerset of W^{∗}(w_{i}), − μ^{∗}(w_{i})(w_{j}) = μ(w_{i})(C_{w_{j}} ), and for any D ⊂ H^{∗}(w_{i}), μ^{∗}(w_{i})(D) =

∑ _{w_{j} ∈D} μ^{∗}(w_{i})(w_{j}),

• v^{∗}(w_{i})(p) = v(w_{i})(p), for every p ∈ Var.

For every w_{i}, μ^{∗}(w_{i}) is finitely additive probability measure, since

μ^{∗}(w_{i})(W^{∗}(w_{i})) = ∑ _{w_{j} ∈W^{∗} (w_{i} )} μ^{∗}(w_{i})(w_{j}) = ∑ _{C_{w_{j}} ∈W_{/≈}} μ^{∗}(w_{i})(C_{w_{j}} ) = 1.

According to the definition of model M^{∗}, it is obvious that it is an L_{⪰} model. We can now show that for every β ∈ Subf(α), β is satisfiable in M iff it

is satisfiable in M^{∗}. If β ∈ Var, (M, w) ⊨ β iff for w_{i} ∈ C_{w}, (M, w_{i}) ⊨ β iff (M^{∗}, w_{i}) ⊨ β. The cases related to ∧ and ¬ can be proved as usual. We will prove the cases when β is a formula of the form γ ⪰ r and γ ⪰ δ.

• (M, w) ⊨ γ ⪰ r iff for w_{i} ∈ C_{w}, (M, w_{i}) ⊨ γ ⪰ r iff

r ⩽ μ(w_{i})([γ]_{M,w} ) = ∑_{C_{u} :(M,u)⊨γ} μ(w_{i})(C_{u}) = ∑_{C_{u} :(M^{∗} ,u)⊨γ} μ^{∗}(w_{i})(C_{u}) = μ^{∗}(w_{i})([γ]_{M^{∗} ,w} )

iff (M^{∗}, w_{i}) ⊨ γ ⪰ r.
• (M, w) ⊨ γ ⪰ δ iff
for w_{i} ∈ C_{w}, (M, w_{i}) ⊨ γ ⪰ δ iff μ(w_{i})([δ]_{M,w} ) ⩽ μ(w_{i})([γ]_{M,w} ) iff

∑ _{C_{u} :(M,u)⊨δ} μ(w_{i})(C_{u}) ⩽ ∑ _{C_{u} :(M,u)⊨γ} μ(w_{i})(C_{u}) iff
∑ _{C_{u} :(M^{∗} ,u)⊨δ} μ^{∗}(w_{i})(C_{u}) ⩽ ∑ _{C_{u} :(M^{∗} ,u)⊨γ} μ^{∗}(w_{i})(C_{u}) iff
μ^{∗}(w_{i})([δ]_{M^{∗} ,w} ) ⩽ μ^{∗}(w_{i})([γ]_{M^{∗} ,w} ) iff (M^{∗}, w_{i}) ⊨ γ ⪰ δ.

Finally, it is clear that the number of different classes in W_{/≈} is at most 2^{k}, and the same holds for the number of worlds in M^{∗}. □

Theorem 5.2 (Decidability theorem). The logic L_{⪰} is decidable.

Proof. As it is noted above, a formula α is L_{⪰} -satisfiable iff it is satisfiable in an L_{⪰} model with at most 2^{k} world, where k denotes the numbers of subformulas of α. The next procedure decides the satisfiability problem.

Let Subf(α) = {β_{1}, …, β_{n}, γ_{1}, …, γ_{m}}, and k = n + m. In every world w from M exactly one of the formulas of the form δ_{w} = β_{1} ∧ ⋯∧ β_{n} ∧ ¬γ_{1} ∧ ⋯∧ ¬γ_{m} holds. For every l ⩽ 2^{k} we will consider l formulas of the above form. The chosen formulas are not necessarily different, but at least one of the formulas must contain the examined formula α. Using probabilistic constraints (i.e., formulas of the form β ⪰ r, ¬(β ⪰ r), β ⪰ γ, ¬(β ⪰ γ)) from the formulas we shall examine whether there is an L_{⪰} model M with l worlds such that for some world w from the model w ⊨ α. We do not try to determine probabilities precisely, we just check whether there are probabilities such that probabilistic constraints are satisfied in the corresponding world. To do that, for every world w_{i}, i < l, we consider a system of linear equalities and inequalities of the form (we write β ∈ δ_{w} to denote that β occurs positively in the top conjunction of δ_{w}, i.e., if δ_{w} can be seen as ⋀ _{i} δ_{i}, then for some i, β = δ_{i}):

∑ _{j=1}^{l} μ(w_{i})(w_{j}) = 1
μ(w_{i})(w_{j}) ⩾ 0 for every world w_{j}
∑ _{w_{j:β∈δw_{j}}}^{l} μ(w_{i})(w_{j}) ⩾ r for every β ⪰ r ∈ δ_{w_{i}}
∑ _{w_{j:β∈δw_{j}}}^{l} μ(w_{i})(w_{j}) < r for every ¬(β ⪰ r) ∈ δ_{w_{i}}
∑ _{w_{j:β∈δw_{j}}}^{l} μ(w_{i})(w_{j}) ⩾ ∑ _{w_{j:γ∈δw_{j}}}^{l} μ(w_{i})(w_{j}) for every β ⪰ γ ∈ δ_{w_{i}}
∑ _{w_{j:β∈δw_{j}}}^{l} μ(w_{i})(w_{j}) < ∑ _{w_{j:γ∈δw_{j}}}^{l} μ(w_{i})(w_{j}) for every ¬(β ⪰ γ) ∈ δ_{w_{i}}

The first two rows correspond to the general constraints: the probability of the set of all worlds must be 1, while the probability of every measurable set of worlds must be nonnegative. The last four rows correspond to the probabilistic constraints because ∑ _{w_{j:β∈δw_{j}}}^{l} μ(w_{i})(w_{j}) = μ(w_{i})([β]_{w_{i}} ).

Such a system is solvable iff there is a probability μ(w_{i}) satisfying all probabilistic constraints that appear in δ_{w_{i}} . Note that there are finitely many such systems that can be solved in a finite number of steps.

If the above test is positively solved, there is an L_{⪰} model in which every world w_{i} ⊨ δ_{w_{i}} . Since α belongs to at least one of the formulas δ_{w_{i}} , we have that α is satisfiable. If the test fails, and there is another possibility of choosing l and the set of formulas δ_{w}, we continue with the procedure, otherwise we conclude that α is not satisfiable.

It is easy to see that the procedure terminates in a finite number of steps. Thus the satisfiability problem for the class L_{⪰} is decidable. Since, ⊨ α iff ¬α is not satisfiable, the L_{⪰} - validity problem is also decidable. □

6. Concluding remarks

We have introduced a probabilistic logic that combines higher order probabilities and the qualitative probability operator. The main result is the proof of the extended completeness theorem for the introduced logic.

Our work is closely related to the methodology presented in [12, 15, 16]. The first two of those papers provide formalism that can handle higher-order probabilities and the technique for construction of the canonical model. The last paper gives the formalism that can handle simple probabilities and the qualitative probability, where nesting of operators is not allowed.

The results presented here can be generalized in such a way that they will allow a complete axiomatization of both qualitative probability and higher-order conditional probabilities.

References

[1] C. Boutilier, Modal logics for qualitative possibility theory, Int. J. Approx. Reasoning 10, 173–201, 1994.

[2] D. Dubois, Belief structures, possibility theory and decomposable confidence relations on finite sets, Comput. Artif. Intell. 5(5) (1986), 403–416.

[3] D. Dubois, H. Prade, Qualitative possibility functions and integrals, In: E. Pap, editor, Handbook of measure theory, North-Holland, 1499–1522, 2002.

[4] R. Fagin, J. Halpern, N. Megiddo, A logic for reasoning about probabilities, Inf. Comput. 87(1–2) (1990), 78–128.

[5] L. Farinas del Cerro, A. Herzig, A modal analysis of possibility theory, FAIR 1991, Lect. Notes Comput. Sci. 535, 11–18, 1991.

[6] L. Godo, E. Marchioni, Coherent conditional probability in a fuzzy logic setting, Log. J. IGPL 14(3) (2006), 457–481.

[7] D. Lehmann, Generalized qualitative probability: Savage revisited; in: E. Horvitz and F. Jensen (eds), Procs. 12th Conf. Uncertainty in Artificial Intelligence (UAI-96), pp. 381–388, 1996.

[8] D. Lewis, Counterfactuals, Basil Blackwell, London, 1973.

[9] E. Marchioni, L. Godo, A Logic for Reasoning about Coherent Conditional Probability: A Modal Fuzzy Logic Approach; in J. Leite and J. Alferes (eds), 9th European Conf. Jelia’04, Lect. Notes Artif. Intell. 3229, 213–225, 2004.

[10] L. Narens, On qualitative axiomatizations for probability theory, J. Philos. Log. 9:2 (1980), 143–151.

[11] N. Nilsson, Probabilistic logic, Artif. Intell. 28 (1986), 71–87.

[12] Z. Ognjanović, M. Rašković, A logic with higher order probabilities, Publ. Inst. Math., Nouv. Sér. 60(74) (1996), 1–4.

[13] Z. Ognjanović, M. Rašković, Some first-order probability logics, Theor. Comput. Sci. 247(1–2) (2000), 191–212.

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

[15] Z. Ognjanović, N. Ikodinović, A logic with higher order conditional probabilities, Publ. Inst. Math., Nouv. Sér. 82(96) (2007), 141–154.

[16] Z. Ognjanović, A. Perović, M. Rašković, Logic with the qualitative probability operator, Log. J. IGPL 16(2) (2008), 105–120.

[17] J. Paris, A. Vencovska, Proof systems for probabilistic uncertain reasoning, J. Symb. Log. 63:3 (1998), 1007–1039.

[18] J. Pavelka, On fuzzy logic I, II, III, Z. Math. Logik Grundlagen Math. 25(1979), 45–52, 119–134, 447–464.

[19] A. Perović, Z. Ognjanović, M. Rašković, Z. Marković, A probabilistic logic with polynomial weight formulas; in: S. Hartmann and G. Kern-Isberner (eds.) FoIKS 2008 Lect. Notes Comput. Sci. 4932, 239–252, 2008.

[20] M. Rašković, Classical logic with some probability operators, Publ. Inst. Math., Nouv. Sér. 53(67) (1993), 1–3.

[21] M. Rašković, Z. Ognjanović, A first order probability logic LP_{Q}, Publ. Inst. Math., Nouv. Sér. 65(79) (1999), 1–7.

[22] M. Rašković, Z. Marković, Z. Ognjanović, A logic with approximate conditional probabilities that can model default reasoning, Int. J. Approx. Reasoning 49(1) (2008), 52–66.

[23] 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.

[24] M. P. Wellman, Some varieties of qualitative probability, Proc. 5th Int. Conf. Information Processing and the Management of Uncertainty, Paris 1994.

Matematički fakultet (Received 18 06 2009) Studentski trg 16 11000 Beograd Serbia

angelina@matf.bg.ac.rs