PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 78(92) (2005), 35–49

COMPLETENESS THEOREM FOR A LOGIC WITH IMPRECISE AND CONDITIONAL PROBABILITIES

Zoran Ognjanović, Zoran Marković and Miodrag Rašković

Communicated by Žarko Mijajlović

Abstract. We present a propositional probability logic which allows making formulas that speak about imprecise and conditional probabilities. A class of Kripke-like probabilistic models is defined to give semantics to probabilistic formulas. Every possible world of such a model is equipped with a probability space. The corresponding probabilities may have nonstandard values. The proposition “the probability is close to r” means that there is an infinitesimal ϵ, such that the probability is equal to r −ϵ (or r +ϵ). We provide an infinitary axiomatization and prove the corresponding extended completeness theorem.

1. Introduction

Although the problem of reasoning with uncertain knowledge is a very old problem dating, at least, from Leibnitz and Boole, formal systems for reasoning in the presence of uncertainty have been recognized as a useful tool in many fields of Computer Science and Artificial Intelligence only since the Nils Nilsson’s paper [16]. Using the semantical approach, Nilsson introduced some procedures for calculating the bounds on the absolute probability of a consequence given the probabilities of the premisses. It motivated many semantical and some proof-theoretical approaches to logics with absolute probabilities (see [2, 4, 5, 6, 9, 10, 15, 18, 19, 20], and the references given there). In the latter discussion on the subject [17] Nilsson argued that a more natural generalization of the classical modus ponens could be handled by conditional probabilities. However, there are not too many papers discussing conditional probabilities from the logical point of view [6, 7, 14, 22]. In [6] a logic which allows formal reasoning about conditional probabilities using the machinery of real closed fields is introduced. In [14], a fuzzy modal logic F CP (LΠ) is introduced along the ideas about coherent probabilities proposed by de Finetti. For each pair of classical propositional formulas α and β, the probability of the conditional event “α given β” is taken as the truth-value of the (fuzzy) modal proposition P (α | β). An axiomatic system is introduced and shown to be sound and complete with respect to the class of probabilistic Kripke structures induced by coherent conditional probabilities. A close approach can be found in [7], where a treatment of nonstandard conditional probability by means of fuzzy logic is given. One of the areas of application of probabilistic logics is the area of default reasoning, which for a while suffered from a lack of proper syntactic characterization. In the seminal paper [12] a set of properties which form a core of default reasoning and the corresponding formal system denoted P are proposed. Many semantics for default entailment have been introduced and proven to be characterized by P [8]. One such approach uses conditional probability to semantically characterize defaults [12], but in that context probability function with non-standard values has to be used. Another similar line of research concerns the study of conditionals (or counter-factuals) [3].

2000 Mathematics Subject Classification: Primary 03B70; Secondary 03B45, 68T37.

Key words and phrases: conditional probability logic, nonstandard values, Hardy field, completeness.

Partially supported by Ministarstvo nauke i zaštite životne okoline Republike Srbije.

In this paper we present a propositional probability logic LICP^{S} (L for logic, I for imprecise, CP for conditional probabilities, while S denotes a special countable set which will be discussed later on) and explore the issue of completeness. The logic allows making formulas that speak about imprecise and conditional probabilities. The corresponding language is obtained by adding probability operators to the classical propositional language. There are two kinds of new operators. The operators of the first type ({P_{⩾s}}_{s∈S}, for the probability of a single formula, and {CP_{⩾s}}_{s∈S}, {CP_{=s}}_{s∈S}, for the conditional probability) concern standard (”crisp”) probabilities with the intended meaning “the (conditional) probability is at least s” and “is s”, respectively. The operators of the second type (CP_{≈r}, P_{≈r}, where r belongs to the unit interval of rational numbers) concern imprecise probabilities with the intended meaning that “the (conditional) probability is close to r”. The set S mentioned above is the unit interval of a recursive nonarchimedean field containing all rational numbers. An example of such field is the Hardy field Q[ϵ], where ϵ is an infinitesimal. In this paper S is used to syntactically define the range of the probability functions that will appear in the interpretation. Thus, the proposition “the (conditional) probability is close to r” means that there is an infinitesimal ϵ_{0}, such that the (conditional) probability is equal to r − ϵ_{0} (or r + ϵ_{0}).

Probabilistic models based on Kripke models are used to give semantics to the formulas so that interpreted formulas are either true or false. Every world from a probability model is equipped with a probability space. The corresponding probability measures are defined on sets of subsets of possible worlds, while the range of the probabilities is the set S. More precisely, we consider the so called class of measurable models. A model is measurable if only sets of possible worlds definable by formulas are measurable. We give an infinitary axiomatic system for LICP^{S}. Here the terms finitary and infinitary concern the proof system only: our object language is countable, formulas are finite, while only proofs are allowed to be infinite. For that axiomatic system and the mentioned class of measurable probability models we prove the extended completeness theorem (‘every consistent set of formulas is satisfiable’). The reason for introducing infinitary rules is that for our logic the compactness theorem does not hold, i.e., there exists a countably infinite set of formulas that is unsatisfiable although every finite subset is satisfiable. For instance, consider {¬P_{=0}α} ∪ {P_{<ϵ^{n}}α : n is a positive integer}. It follows that it is not possible to give a usual finitary axiomatic system for LICP^{S} since the compactness theorem follows easily from the extended completeness theorem if the corresponding axiomatization is finitary. There are four infinitary rules in our system. One of them (Rule 3) enables us to syntactically define the range of the probability functions which will appear in the interpretation. A similar rule was given in [1] but restricted to rationals only.

We showed in [21, 22] how, thanks to our nonstandard probabilistic semantics, a restriction (denoted LP P^{S}) of LICP^{S} can be used to syntactically describe the behavior of the defaults in a probabilistic framework. LP P^{S} allows only one imprecise conditional probability operator CP_{≈1}, and does not allow iteration of probabilistic operators. The axioms and rules of the system P can be translated into LP P^{S}-valid formulas, so that the formula CP_{≈1}(β, α) syntactically describes the behavior of the default ’if α, then generally β’. Thus, the corresponding LP P^{S}- axiom system can be used to characterize the default consequence relation. In [13] a combination of probabilistic knowledge and default reasoning is considered. Since the axioms and rules of the system P are applied to probabilistic knowledge, and since LP P^{S} does not allow iteration of probabilistic operators, it is not possible to extend our approach from [21, 22] to the framework discussed there. Thus, we consider our logic LICP^{S} as a natural generalization of LP P^{S} which might be useful in characterization of the system proposed in [13].

2. Syntax

Let Q[0, 1] denote the set of all rational numbers from the unit interval. Let S be the unit interval of a recursive nonarchimedean field containing Q[0, 1]. An example of such field is the Hardy field Q[ϵ]. Q[ϵ] contains all rational functions of a fixed infinitesimal ϵ which belongs to a nonstandard elementary extension R^{∗} of the standard real numbers (see [11, 23]). A typical positive element of Q[ϵ] is of the form

ϵ^{k} \frac{∑_{i=0}^{n} a_{i}ϵ^{i}}{∑_{i=0}^{m} b_{i}ϵ^{i}} ,

where a_{0} · b_{0} ≠ 0.

The language of the logic consists of:

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

• classical connectives ¬, and ∧,

• a denumerable list of unary probabilistic operators (P_{⩾s})_{s∈S},

• a denumerable list of unary probabilistic operators (P_{≈r})_{r∈Q[0,1]},

• a denumerable list of binary probabilistic operators (CP_{⩾s})_{s∈S},

• a denumerable list of binary probabilistic operators (CP_{=s})_{s∈S} and

• a denumerable list of binary probabilistic operators (CP_{≈r})_{r∈Q[0,1]}.

The set of formulas is defined inductively as the smallest set containing propositional letters and closed under formation rules: if α and β are formulas, s ∈ S and r ∈ Q[0, 1], then ¬α, α ∧ β, P_{⩾s}α, P_{≈r}α, CP_{⩾s}(α, β), CP_{=s}(α, β) and CP_{≈r}(α, β) are formulas. Let For_{S} denote this set of formulas.

For example, (¬p ∧ P_{≈0.5}q) ∧ CP_{⩾1−2ϵ_{1}}(r ∧ q, CP_{=0.8}(r, p)) is a formula.

The other classical connectives (∨, →, ↔) can be defined as usual, while we denote ¬P_{⩾s}α by P_{<s}α, P_{⩾1−s}¬α by P_{⩽s}α, ¬P_{⩽s}α by P_{>s}α, P_{⩾s}α ∧ ¬P_{>s}α by P_{=s}α, ¬P_{=s}α by P_{≠s}α, ¬CP_{⩾s}(α, β) by CP_{<s}(α, β), CP_{<s}(α, β) ∨ CP_{=s}(α, β) by CP_{⩽s}(α, β), and CP_{⩾s}(α, β) ∧ ¬CP_{=s}(α, β) by CP_{>s}(α, β). Finally, we use ⊥ to denote ¬p ∧ p.

3. Semantics

The semantics for our logic will be based on the Kripke-style models.

Definition 3.1. An LICP^{S}-model is a structure M = ⟨W, Prob, v⟩ where: • W is a nonempty set of elements called worlds,

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

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

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

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

– μ(w) : H(w) → S is a finitely additive probability measure, and • v : W × Var → {true, false} is a valuation which associates with every world w ∈ W a truth assignment v(w) on the propositional letters.

Let M = ⟨W, Prob, v⟩ be an LICP^{S}-model, w, u ∈ W, p ∈ Var, α, β ∈ For_{S}, s ∈ S and r ∈ Q[0, 1]. The satisfiability relation ⊧ is inductively defined as follows:

(1) (w, M) ⊧ p if v(w)(p) = true,

(2) (w, M) ⊧ ¬α if it is not (w, M) ⊧ α,

(3) (w, M) ⊧ α ∧ β if (w, M) ⊧ α and (w, M) ⊧ β,

(4) (w, M) ⊧ P_{⩾s}α if μ(w)({u ∈ W (w) : (u, M) ⊧ α}) ⩾ s,

(5) (w, M) ⊧ P_{≈r}α if for every integer n > 0, μ(w)({u ∈ W (w) : (u, M) ⊧ α}) ∈ [max{0, r − 1/n}, min{1, r + 1/n}],

(6) (w, M) ⊧ CP_{⩾s}(α, β) if either μ(w)({u ∈ W (w) : (u, M) ⊧ β}) = 0 or μ(w)(\{u ∈ W (w) : (u, M) ⊧ β\}) > 0 and \frac{μ(w)(\{u∈W (w):(u,M)⊧α∧β\})}{μ(w)(\{u∈W (w):(u,M)⊧β\})} ⩾ s,

(7) (w, M) ⊧ CP_{=s}(α, β) if either μ(w)({u ∈ W (w) : (u, M) ⊧ β}) = 0 and

s = 1 or μ(w)({u ∈ W (w) : (u, M) ⊧ β}) > 0 and
\frac{μ(w)(\{u∈W (w):(u,M)⊧α∧β\})}{μ(w)(\{u∈W (w):(u,M)⊧β\})} = s,

(8) (w, M) ⊧ CP_{≈r}(α, β) if either μ(w)({u ∈ W (w) : (u, M) ⊧ β}) = 0 and r = 1 or μ(w)({u ∈ W (w) : (u, M) ⊧ β}) > 0 and for every positive integer n, \frac{μ(w)(\{u∈W (w):(u,M)⊧α∧β\})}{μ(w)(\{u∈W (w):(u,M)⊧β\})} ∈ [max\{0, r − 1/n\}, min\{1, r + 1/n\}].

In the sequel, we will omit M from (w, M) ⊧ α and write w ⊧ α if M is clear from the context.

Note that the condition 5 is equivalent to saying that the probability of α equals r−ϵ_{0} (or r+ϵ_{0}) for some infinitesimal ϵ_{0} ∈ S. The similar holds for the condition 8.

In an LICP^{S}-model M = ⟨W, Prob, v⟩ the set {u ∈ W (w) : u ⊧ α}, is denoted by [α]_{w}. In the sequel we consider only so-called measurable models. An LICP^{S}-model M = ⟨W, Prob, v⟩ is said to be measurable if for every w ∈ W, H(w) = {[α]_{w} : α ∈ For_{S}}, i.e., if every set of the form [α]_{w} is measurable and every H(w) contains only sets definable by formulas. It is not hard to see that H(w)’s are algebras. Let us denote this class of models by LICP_{Meas}^{S}.

A set of formulas T is LICP_{Meas}^{S}-satisfiable if there is a world w in an LICP_{Meas}^{S}- model M such that for every formula α ∈ T, w ⊧ α. A formula α is LICP_{Meas}^{S}- satisfiable if the set {α} is LICP_{Meas}^{S}-satisfiable. A formula α is LICP_{Meas}^{S}-valid (denoted by ⊧ α) if it is satisfied in each world in each model.

4. Axiomatization

The set of all valid formulas can be characterized by the following set of axiom schemata:

(1) all the axioms of the classical propositional logic

(2) P_{⩾0}α

(3) P_{⩽s}α → P_{<t}α, t > s

(4) P_{<s}α → P_{⩽s}α

(5) P_{⩾1}(α ↔ β) → (P_{=s}α → P_{=s}β)

(6) (P_{=s}α ∧ P_{=t}β ∧ P_{⩾1}¬(α ∧ β)) → P_{=min(1,s+t)}(α ∨ β)

(7) P_{≈r}α → P_{⩾r_{1}}α, for every rational r_{1} ∈ [0, r)

(8) P_{≈r}α → P_{⩽r_{1}}α, for every rational r_{1} ∈ (r, 1]

(9) CP_{=s}(α, β) → ¬CP_{=t}(α, β), s ≠ t

(10) P_{=0}β → CP_{=1}(α, β)

(11) (P_{=t}β ∧ P_{=s}(α ∧ β)) → CP_{=s/t}(α, β), t ≠ 0, s ⩽ t

(12) CP_{=s}(α, β) → ¬CP_{⩾t}(α, β), s < t

(13) CP_{=s}(α, β) → CP_{⩾t}(α, β), s ⩾ t

(14) CP_{=s}(α, β) → (P_{=ts}(α ∧ β) ↔ P_{=t}β), t ≠ 0

(15) CP_{≈r}(α, β) → CP_{⩾r_{1}}(α, β), for every rational r_{1} ∈ [0, r)

(16) CP_{≈r}(α, β) → CP_{⩽r_{1}}(α, β), for every rational r_{1} ∈ (r, 1]

(17) CP_{=r}(α, β) → CP_{≈r}(α, β) and inference rules:

(1) From α and α → β infer β.

(2) From α infer P_{⩾1}α.

(3) From β → P_{≠s}α, for every s ∈ S, infer β → ⊥.

(4) From γ → (P_{=ts}(α ∧ β) ↔ P_{=s}β), for every s ∈ S ∖ {0}, infer γ → CP_{=t}(α, β).

(5) For every r ∈ Q[0, 1], from γ → P_{⩾r−1/n}α, for every integer n ⩾ 1/r, and γ → P_{⩽r+1/n}α, for every integer n ⩾ 1/(1 − r), infer γ → P_{≈r}α.

(6) For every r ∈ Q[0, 1], from γ → CP_{⩾r−1/n}(α, β), for every integer n ⩾ 1/r, and γ → CP_{⩽r+1/n}(α, β), for every integer n ⩾ 1/(1 − r), infer γ → CP_{≈r}(α, β).

We denote this axiomatic system by Ax_{LICP^{S}}.

The axioms 2– 6 and Rule 2 concern the “crisp” probabilities. They are given in [18, 19]. For example, Axiom 2 says that every formula is satisfied in a set of worlds of the probability at least 0. By substituting ¬α for α in Axiom 2, the formula P_{⩽1}α (= P_{⩾0}¬α) is obtained. This formula means that every formula is satisfied in a set of worlds of the probability at most 1. Let us denote it by 2’. Axiom 5 means that the equivalent formulas must have the same probability. Axiom 6 corresponds to the property of the finite additivity of probability. Rule 2 may be considered as the analogue of the rule of necessitation in modal logic. From Axiom 2’ and Rule 2 we obtain another inference rule 2’: from α infer P_{=1}α. Rule 3 guarantees that the probability of a formula belongs to the set S, enabling us thus to syntactically specify the range of the probability functions that will appear in the semantics.

The axioms 9–14 and Rule 4 concern properties of the “crisp” conditional probabilities and the relationship between the probability and conditional probability.

The axioms 7–8 and 15–17, and the rules 5 and 6 syntactically determine imprecise probabilities. For example, Rule 5 says that if the probability of α belongs to the interval [r−1/n, r+1/k] for all integers integers n and k such that r−1/n ⩾ 0, r + 1/k ⩽ 1, then the probability of α is infinitesimally close to r.

Note that the rules 3–6 are infinitary.

A formula α is deducible from a set T of formulas (denoted T ⊢_{Ax_{LICP^{S}}} α) 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 to the theorems only. A formula α is a theorem (⊢ α) if it is deducible from the empty set. T ⊬_{Ax_{LICP^{S}}} α means that T ⊢_{Ax_{LICP^{S}}} α does not hold. A set T of formulas is consistent if there is at least one formula α such that T ⊬_{Ax_{LICP^{S}}} α. 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.

The limitation of application of Rule 2 in deductions allows us to obtain Deduction theorem (Theorem 5.1) which is one of the main steps in our approach to proving completness of Ax_{LICP^{S}}. Also, note that, in the presence of Deduction theorem, unrestricted applications of Rule 2 would produce undesirable consequences. For example, consider the following deduction:

α ⊢ α
α ⊢ P_{⩾1}α, by Rule 2
⊢ α → P_{⩾1}α by Deduction theorem,

but the last formula α → P_{⩾1}α certainly is not a valid formula of our logic.

5. Soundness and completeness

Soundness of the system follows from the soundness of the classical propositional logic, as well as from the properties of probabilistic measures, so the proof is straightforward and we omit it here. For the detailed arguments see the proof of Theorem 13 in [15].

In order to prove the completeness theorem for our logic, we show that every consistent set of sentences is satisfiable. We begin with the deduction theorem and some auxiliary statements. Then, we describe how a consistent set T of formulas can be extended to a maximal consistent set, and how a canonical model can be constructed out of maximal consistent sets. Finally, we prove that for every world w from the canonical model and every formula α, w ⊧ α if and only if α ∈ w, and as a consequence we obtain that the set T is satisfiable.

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

Proof. We use the transfinite induction on the length of the inference. Let us first consider the case where β = P_{⩾1}γ is obtained from T ∪ {α} by an application of Rule 2. In that case γ and β must be theorems. Then, from ⊢ β → (α → β), we obtain T ⊢ α → β. Next, suppose that β = γ → CP_{=t}(φ, ψ) is obtained from T ∪ {α} by an application of Rule 4. Then:

T, α ⊢ γ → (P_{=ts}(φ ∧ ψ) ↔ P_{=s}ψ), for every s ∈ S ∖ {0}

T ⊢ α → (γ → (P_{=ts}(φ ∧ ψ) ↔ P_{=s}ψ)), for every s ∈ S ∖ {0}, by the induction hypothesis T ⊢ (α ∧ γ) → (P_{=ts}(φ ∧ ψ) ↔ P_{=s}ψ)), for every s ∈ S ∖ {0} T ⊢ (α ∧ γ) → CP_{=t}(φ, ψ), by Rule 4 T ⊢ α → β.

The other cases follow similarly. □

Theorem 5.2. For every formula α, the following hold:

(1) ⊢ P_{⩾t}α → P_{⩾s}α, t > s

(2) ⊢ P_{⩽t}α → P_{⩽s}α, t < s

(3) ⊢ P_{=t}α → ¬P_{=s}α, t ≠ s

(4) ⊢ P_{=t}α → ¬P_{⩾s}α, t < s

(5) ⊢ P_{=t}α → ¬P_{⩽s}α, t > s

(6) ⊢ P_{=r}α → P_{≈r}α, r ∈ Q[0, 1].

Proof. (1–2) Let us call the property expressed by these two formulas the monotonicity of the probability. The formulas follow from the axioms 3 and 4.

(3) Note that P_{=t}α denotes P_{⩾t}α ∧ P_{⩽t}α, while ¬P_{⩾s}α = P_{<s}α. From Axiom 3, we have ⊢ P_{⩽t}α → ¬P_{⩾s}α for every s > t. Similarly, by the contraposition, from Axiom 3, we obtain ⊢ P_{⩾t}α → ¬P_{⩽s}α, for every s < t. It follows that ⊢ (P_{⩽t}α ∧ P_{⩾t}α) → (¬P_{⩽s}α ∨ ¬P_{⩾s}α), and that ⊢ P_{=t}α → ¬P_{=s}α for every s ≠ t.

(4–5) Similarly as the above item (3) of this Theorem.

(6) This statement give us an example of an application of an infinitary inference rule. Namely, by the above items (4–5) of this Theorem, we have ⊢ P_{=r}α → P_{⩾r−1/n}α for every n ⩾ 1/r, and ⊢ P_{=r}α → P_{⩽r+1/n}α for every n ⩾ 1/(1 − r). Then, by Rule 5, it follows ⊢ P_{=r}α → P_{≈r}α. □

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

Proof. Let T be a consistent set, and α_{0}, α_{1}, … an enumeration of all formulas. We define a sequence of sets T_{i}, i = 0, 1, 2, … such that:

(1) T_{0} = T

(2) for every i ⩾ 0, (a) if T_{2i} ∪ {α_{i}} is consistent, then T_{2i+1} = T_{2i} ∪ {α_{i}};

(b) otherwise, if α_{i} is of the form γ → CP_{=t}(α, β), then T_{2i+1} = T_{2i} ∪ {¬α_{i}, γ → ¬(P_{=ts}(α ∧ β) ↔ P_{=s}β)}, for some s > 0 so that T_{2i+1} is consistent;

(c) otherwise, if α_{i} is of the form γ → P_{≈r}α, then T_{2i+1} = T_{2i} ∪ {¬α_{i}, γ → ¬P_{⩾r−1/n}α}, or T_{2i+1} = T_{2i} ∪ {¬α_{i}, γ → ¬P_{⩽r+1/n}α}, for some integer n so that T_{2i+1} is consistent;

(d) otherwise, if α_{i} is of the form γ → CP_{≈r}(α, β), then T_{2i+1} = T_{2i} ∪ {¬α_{i}, γ → ¬CP_{⩾r−1/n}(α, β)}, or T_{2i+1} = T_{2i} ∪ {¬α_{i}, γ → ¬CP_{⩽r+1/n}(α, β)}, for some integer n so that T_{2i+1} is consistent;

(e) otherwise, T_{2i+1} = T_{2i} ∪ {¬α_{i}},

(3) for every i ⩾ 0, T_{2i+2} = T_{2i+1} ∪ {P_{=s}α_{i}}, for some s ∈ S, so that T_{2i+2} is consistent,

The sets obtained by the steps 1 and 2a are obviously consistent. The step 2e produces consistent sets, too. For if T_{2i}, α_{i} ⊢ ⊥, by Deduction theorem we have T_{2i} ⊢ ¬α_{i}, and since T_{2i} is consistent, so it is T_{2i} ∪ {¬α_{i}}. The same holds for the steps 2b– 2d. Let us first consider the step 2b. Suppose that α_{i} is of the form γ → CP_{=t}(α, β), and that neither T_{2i} ∪ {γ → CP_{=t}(α, β)} nor T_{2i} ∪ {¬(γ → CP_{=t}(α, β)), γ → ¬(P_{=ts}(α ∧ β) ↔ P_{=s}β)}, for every s > 0, are consistent. It means that:

(1) T_{2i}, ¬(γ → CP_{=t}(α, β)), γ → ¬(P_{=ts}(α ∧ β) ↔ P_{=s}β) ⊢ ⊥, for every s > 0,

(2) T_{2i}, ¬(γ → CP_{=t}(α, β)) ⊢ (γ → ¬(P_{=ts}(α ∧ β) ↔ P_{=s}β)) → ⊥, for every s > 0, by Deduction theorem,

(3) T_{2i}, ¬(γ → CP_{=t}(α, β)) ⊢ ¬(γ → ¬(P_{=ts}(α ∧ β) ↔ P_{=s}β)), for every s > 0,

(4) T_{2i}, ¬(γ → CP_{=t}(α, β)) ⊢ γ → (P_{=ts}(α ∧ β) ↔ P_{=s}β)), for every s > 0, by the classical tautology ¬(α → β) → (α → ¬β),

(5) T_{2i}, ¬(γ → CP_{=t}(α, β)) ⊢ γ → CP_{=t}(α, β), by Rule 4,

(6) T_{2i} ⊢ ¬(γ → CP_{=t}(α, β)) → (γ → CP_{=t}(α, β)), by Deduction theorem,

(7) T_{2i} ⊢ γ → CP_{=t}(α, β), by classical reasoning

which contradicts consistency of T_{2i} since T_{2i} ∪{γ → CP_{=t}(α, β)} is not consistent. Next, consider the step 2c, suppose that α_{i} is of the form γ → P_{≈r}α, and that T_{2i} ∪ {γ → P_{≈r}α} is not consistent. Also, let all the sets T_{2i} ∪ {¬(γ → P_{≈r}α), γ → ¬P_{⩾r−1/n}α}, for every integer n : r − 1/n ⩾ 0, and T_{2i} ∪ {¬(γ → P_{≈r}α), γ → ¬P_{⩽r+1/n}α} for every integer n : r + 1/n ⩽ 1 be inconsistent Then, we have:

(1) T_{2i}, ¬(γ → P_{≈r}α), γ → ¬P_{⩾r−1/n}α ⊢ ⊥, for every integer n,
(2) T_{2i}, ¬(γ → P_{≈r}α), γ → ¬P_{⩽r+1/n}α ⊢ ⊥, for every integer n,
(3) T_{2i}, ¬(γ → P_{≈r}α) ⊢ γ → P_{⩾r−1/n}α, for every integer n,
(4) T_{2i}, ¬(γ → P_{≈r}α) ⊢ γ → P_{⩽r+1/n}α, for every integer n,
(5) T_{2i}, ¬(γ → P_{≈r}α) ⊢ γ → P_{≈r}α, by Rule 5

which, similarly as above, contradicts consistency of T_{2i}. The step 2d and the case when α_{i} = γ → CP_{≈r}(α, β) follows in the same way using Rule 6.

Finally, consider the step 3 of the construction, and suppose that for every s ∈ S, T_{2i+1} ∪ {P_{=s}α_{i}} is not consistent. Let T_{2i+1} = T_{0} ∪ T_{2i+1}^{+}, where T_{2i+1}^{+} denotes the set of all formulas β that are added to T_{0} in the previous steps of the construction. Then:

(1) T_{0}, T_{2i+1}^{+}, P_{=s}α_{i} ⊢ ⊥, for every s ∈ S, by the hypothesis
(2) T_{0}, T_{2i+1}^{+} ⊢ ¬P_{=s}α_{i}, for every s ∈ S, by Deduction theorem
(3) T_{0} ⊢ (⋀_{β∈T_{2i+1}^{+}} β) → ¬P_{=s}α_{i}, for every s ∈ S, by Deduction theorem
(4) T_{0} ⊢ (⋀_{β∈T_{2i+1}^{+}} β) → ⊥, by Rule 3
(5) T_{2i+1} ⊢ ⊥

which contradicts consistency of T_{2i+1}.

Let T^{∗} = ∪_{i}T_{i}. We have to prove that T^{∗} is a maximal consistent set.

First, we can show that if P_{=s}α ∈ T^{∗}, then for every formula β, β → P_{=s}α ∈ T^{∗}. Suppose that it is not the case. Then, according to the above construction, for some β, and some j, P_{=s}α and ¬(β → P_{=s}α) (i.e., β ∧ ¬P_{=s}α) belong to T_{j}. It means that T_{j} ⊢ P_{=s}α ∧ ¬P_{=s}α, a contradiction.

The steps 2a–2e 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 α, ¬α ∈ T^{∗}. To prove that, suppose that α = α_{i} and ¬α = α_{j} for some i and j. If α, ¬α ∈ T^{∗}, then also α, ¬α ∈ T_{max(2i,2j)+1}, a contradiction with the consistency of T_{max(2i,2j)+1}.

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

First, note that if for some i, T_{i} ⊢ α, it must be α ∈ T^{∗}. Otherwise, if ¬α ∈ T^{∗}, there must be some k such that T_{k} ⊢ α and T_{k} ⊢ ¬α which contradicts the consistency of T_{k}.

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

So, let us consider the infinitary rules.

Let γ_{i} = β → ⊥ be obtained from the set of premises {γ_{i}^{k} = β → ¬P_{=s_{k}}φ : s_{k} ∈ S} by Rule 3. Suppose that γ_{i} ∉ T^{∗}. By the induction hypothesis, γ_{i}^{k} ∈ T^{∗} for every k. The step 3 of the construction guaranties that there are some l and s_{l} ∈ S such that P_{=s_{l}}φ ∈ T_{l}. Reasoning as above, we conclude that β → P_{=s_{l}}γ ∈ T^{∗}. Thus, there must be some j such that both β → ¬P_{=s_{l}}γ, and β → P_{=s_{l}}γ belongs to T_{j}. It follows that T_{j} ⊢ β → ¬P_{=s_{l}}γ, T_{j} ⊢ β → P_{=s_{l}}γ, and T_{j} ⊢ β → ⊥, which means that β → ⊥ ∈ T^{∗}, i.e., γ_{i} ∈ T^{∗}, a contradiction.

Let γ_{i} = β → CP_{=t}(φ, ψ) be obtained from the set of premises {γ_{i}^{k} = β → (P_{=ts}(φ ∧ ψ) ↔ P_{=s}ψ) : s ∈ S ∖ {0}} by rule Rule 4. Suppose that γ_{i} ∉ T^{∗}. By the step 2b of the construction, there are some s′ > 0 and l such that β → ¬(P_{=ts′}(φ ∧ ψ) ↔ P_{=s′}ψ) ∈ T_{l}. It follows that there must be some j such that both β → ¬(P_{=ts′}(φ ∧ ψ) ↔ P_{=s′}ψ) and β → (P_{=ts′}(φ ∧ ψ) ↔ P_{=s′}ψ) belongs to T_{j}. Then, T_{j} ⊢ β → ⊥ and T_{j} ⊢ β → CP_{=t}(φ, ψ). Thus, β → CP_{=t}(φ, ψ) ∈ T^{∗}, a contradiction.

Let γ_{i} = β → P_{≈r}φ be obtained by Rule 5 from the set of premises of the form β → P_{⩾r−1/n}φ, for every integer n : r − 1/n ⩾ 0 and β → P_{⩽r+1/n}φ, for every integer n : r + 1/n ⩽ 1. Suppose that γ_{i} ∉ T^{∗}. By the step 2c of the construction, there are some n and j such that β → ¬P_{⩾r−1/n}φ or β → ¬P_{⩽r+1/n}φ belongs to T_{j}. Let us suppose the former case, while the latter one will follow similarly. It means that there is some l such that β → P_{⩾r−1/n}φ, β → ¬P_{⩾r−1/n}φ ∈ T_{l}. Then, T_{l} ⊢ β → ⊥, and T_{l} ⊢ β → P_{≈r}φ. It follows that γ_{i} ∈ T^{∗}, a contradiction.

Finally, the case concerning the formulas of the form γ_{i} = β → CP_{≈r}(φ, ψ) and Rule 6 can be proved in the same way.

Hence, from T^{∗} ⊢ α, we have α ∈ T^{∗}. It follows that T^{∗} is a maximal consistent set. □

Being a maximal consistent set, T^{∗} has all the expected properties summarized in the next statement.

Theorem 5.4. Let T^{∗} be defined as above. Then, the following hold:

(1) T^{∗} contains all theorems.

(2) If α ∈ T^{∗}, then ¬α ∉ T^{∗}.

(3) α ∧ β ∈ T^{∗} iff α ∈ T^{∗} and β ∈ T^{∗}.

(4) If α, α → β ∈ T^{∗}, then β ∈ T^{∗}.

(5) There is exactly one s ∈ S such that P_{=s}α ∈ T^{∗}.

(6) If P_{⩾s}α ∈ T^{∗}, there is some t ∈ S such that t ⩾ s and P_{=t}α ∈ T^{∗}.

(7) If P_{⩽s}α ∈ T^{∗}, there is some t ∈ S such that t ⩽ s and P_{=t}α ∈ T^{∗}.

(8) There is exactly one s ∈ S such that CP_{=s}(α, β) ∈ T^{∗}.

(9) If CP_{⩾s}(α, β)∈T^{∗}, there is some t∈S such that t⩾s and CP_{=t}(α, β)∈T^{∗}.

(10) If CP_{≈r_{1}}(α, β) ∈ T^{∗} and r_{2} ∈ Q[0, 1] ∖ {r_{1}}, then CP_{≈r_{2}}(α, β) ∉ T^{∗}

Proof. (1– 4) The proof is standard and left to the reader.

(5) First, note that, according to Theorem 5.2. 3, if P_{=s}α ∈ T^{∗}, then for every t ≠ s, P_{=t}α ∉ T^{∗}. On the other hand, suppose that for every s ∈ S, ¬P_{=s}α ∈ T^{∗}. It follows that T^{∗} ⊢ ¬P_{=s}α for every s ∈ S, and by Rule 3, T^{∗} ⊢ ⊥ which contradicts consistency of T^{∗}. Thus, for every α, there is exactly one s ∈ S such that P_{=s}α ∈ T^{∗}.

(6) Since P_{⩾s}α ∈ T^{∗}, we have that ¬P_{<s}α ∈ T^{∗}. By the above item (5) of this Theorem, for every α there is some t ∈ S such that P_{=t}α ∈ T^{∗}. It means that P_{⩾t}α ∈ T^{∗}, and P_{⩽t}α ∈ T^{∗}. If t < s, then by Axiom 3 from P_{⩽t}α ∈ T^{∗} it follows that P_{<s}α ∈ T^{∗} (i.e., ¬P_{⩾s}α ∈ T^{∗}), a contradiction. Thus, it must be t ⩾ s.

(7) Similarly as the above item (6) of this Theorem.

(8) According to Axiom 9 there cannot be two different t, s ∈ S such that CP_{=t}(α, β) ∈ T^{∗} and CP_{=s}(α, β) ∈ T^{∗}. From the above item (6) of this Theorem, we have that for exactly one t′ and exactly one t′′, P_{=t′}β ∈ T^{∗} and P_{=t′′}(α∧β) ∈ T^{∗}. If t′ = 0, then CP_{=1}(α, β) ∈ T^{∗}, by Axiom 10. Let t′ ≠ 0, and s = \frac{t′′}{t′}. Using Axiom 11 we have that CP_{=s}(α, β) ∈ T^{∗}. Thus, for all α and β, there is exactly one s ∈ S such that CP_{=s}(α, β) ∈ T^{∗}.

(9) Let CP_{⩾s}α ∈ T^{∗}. From the above item (8) of this Theorem, there is exactly one t ∈ S such that CP_{=t}(α, β) ∈ T^{∗}. It follows from Axiom 12 that t cannot be less than s. Thus, it must be t ⩾ s.

(10) Let CP_{≈r_{1}}(α, β) ∈ T^{∗} and r_{2} ∈ Q[0, 1] ∖ {r_{1}}. Suppose that r_{2} < r_{1}. If CP_{≈r_{2}}(α, β) ∈ T^{∗}, from the axioms 15 and 16, for every r_{3} ∈ (r_{2}, r_{1}) ∩ Q[0, 1] it must be CP_{⩾r_{3}}(α, β) ∈ T^{∗} and CP_{⩽r_{3}}(α, β) ∈ T^{∗}, which implies CP_{=r_{3}}(α, β) ∈ T^{∗}, a contradiction to the above item (9) of this Theorem. The same conclusion follows from the assumption that r_{2} > r_{1}. □

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

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

• [α] = {w ∈ W : α ∈ 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} and – μ(w)([α]) = s iff P_{=s}α ∈ w and

• for every propositional letter p ∈ Var, v(w)(p) = true iff p ∈ w. The next theorem states that M is an LICP_{Meas}^{S}-model.

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

(1) μ(w) is a well-defined function.

(2) {[α]} is an algebra of subsets of W (w).

(3) μ(w) : {[α]} → S is a finitely additive probability measure.

Proof. (1) It follows from Theorem 5.4. 5 that for every α there is exactly one s ∈ S such that P_{=s}α ∈ w, i.e., that μ(w)([α]) = s. On the other hand, let [α] = [β] for some α and β. It means that for every w ∈ W, α ↔ β ∈ w, that ¬(α ↔ β) is inconsistent, and that ⊢ α ↔ β and ⊢ P_{=1}(α ↔ β). Axiom 5 guarantees that P_{=s}α ∈ w iff P_{=s}β ∈ w. Thus, [α] = [β] implies that μ(w)([α]) = μ(w)([β]).

(2) For an arbitrary β, W = [β ∨ ¬β], and W ∈ H(w). If [β] ∈ H(w), then the complement of [β] is [¬β], and it belongs to H(w) as well. If [β_{1}],…, [β_{k}] ∈ H(w), then also the union [β_{1}] ∪ … ∪ [β_{k}] ∈ H(w) because [β_{1}] ∪ … ∪ [β_{k}] = [β_{1} ∨ … ∨ β_{k}].

(3) It follows from the step 3 of the construction in Theorem 5.3 that μ(w) : H(w) → S. Since for an arbitrary formula α, W = [α ∨ ¬α], ⊢ α ∨ ¬α and by the Rule 2’ we have ⊢ P_{=1}(α ∨ ¬α), it follows that P_{=1}(α ∨ ¬α) ∈ w. It means that μ(w)(W) = 1. Let [α] ∩ [β] = ∅, μ(w)([α]) = s and μ(w)([β]) = t. Since, [α] ∩ [β] = ∅, we have that [¬(α ∧ β)] = W, and μ(w)([¬(α ∧ β)]) = 1. From the assumptions we have that P_{=s}α, P_{=t}β, P_{⩾1}¬(α ∧ β) ∈ w. Using Axiom 6 it follows that P_{=s+t}(α ∨ β) ∈ w, i.e., μ(w)([α ∨ β]) = s + t. □

Now we can prove the extended completeness theorem for the class LICP_{Meas}^{S}:

Theorem 5.6 (Extended completeness theorem). A set T of formulas is consistent if and only if T has an LICP_{Meas}^{S}-model.

Proof. The (⇐)-direction follows from the soundness of the axiomatic system Ax_{LICP^{S}}. In order to prove the (⇒)-direction we construct the canonical LICP_{Meas}^{S}-model M = ⟨W, Prob, v⟩ as above, and show that for all α and w ∈ W, w ⊧ α iff α ∈ w.

Let α be a propositional letter from Var. By the definition of the valuation v(w), w ⊧ α iff α ∈ w. The classical cases α = ¬β and α = β ∧ γ follow by the standard arguments.

Let α = P_{⩾s}β. If P_{⩾s}β ∈ w, then, by Theorem 5.4. 6, there is some t ⩾ s such that P_{=t}β ∈ w, i.e., such that μ(w)([β]) = t ⩾ s. Thus, w ⊧ P_{⩾s}β. On the other hand suppose that w ⊧ P_{⩾s}β, i.e., that μ(w)([β]) = t ⩾ s, and P_{=t}β ∈ w. It means that P_{⩾t}β ∈ w, and by Theorem 5.2. 1 it follows that P_{⩾s}β ∈ w.

Let α = P_{≈r}β. If P_{≈r}β ∈ w, by the axioms 7 and 8, for every rational r′ < r, P_{⩾r′}β ∈ w, and for every rational r′ > r, P_{⩽r′}β ∈ w. Suppose that w |̸= P_{≈r}β. It means that there is some t ∈ S such that t ≠ r and μ(w)([β]) = t, i.e., P_{=t}β ∈ w. Also, there must be an interval [r_{1}, r_{2}] containing r such that r_{1} and r_{2} are rational and t ∉ [r_{1}, r_{2}], otherwise w ⊧ P_{≈r}β. Now, if t < r, then according to Theorem 5.2. 4 ¬P_{⩾r_{1}}β ∈ w, a contradiction. The similar conclusion follows from the assumption that t > r. Thus, it must be w ⊧ P_{≈r}β. For the other direction, suppose that w ⊧ P_{≈r}β. It follows that w ⊧ P_{⩾r′}β for every rational r′ < r and w ⊧ P_{⩽r′′}β for every rational r′′ > r. However, if P_{≈r}β ∉ w, by the step 2c of the construction in Theorem 5.3, there must be some rational r_{1} < r (or some rational r_{2} > r) such that ¬P_{⩾r_{1}}β ∈ w (or ¬P_{⩽r_{2}}β ∈ w) which contradicts consistency of w. Thus, P_{≈r}β ∈ w.

Let α = CP_{=s}(β, γ). Suppose that CP_{=s}(β, γ) ∈ w. If P_{=0}γ ∈ w, from Axiom 10 and Theorem 5.4. 8 it must be CP_{=1}(β, γ) ∈ w, and s = 1. Since μ(w)([γ]) = 0, we have w ⊧ CP_{=1}(β, γ). Otherwise, let P_{=t}γ ∈ w, t ≠ 0. It follows from Axiom 14 that P_{=st}(β ∧ γ) ∈ w. Since μ(w)([γ]) = t ≠ 0 and μ(w)([β ∧ γ]) = st, we have w ⊧ CP_{=s}(β, γ). For the other direction, suppose that w ⊧ CP_{=s}(β, γ). If w ⊧ P_{=0}γ, then s = 1 and P_{=0}γ ∈ w. From Axiom 10 we have that CP_{=1}(β, γ) ∈ w. Otherwise, let w ⊧ P_{=t}γ, t ≠ 0, and CP_{=s}(β, γ) ∉ w. Then, by the step 2b of the construction in Theorem 5.3, there is some u > 0 such that ¬(P_{=su}(β ∧ γ) ↔ P_{=u}γ) ∈ w. It means that (P_{=su}(β∧γ)∧¬P_{=u}γ) ∈ w or (¬P_{=su}(β∧γ)∧P_{=u}γ) ∈ w, i.e., P_{=su}(β ∧ γ) ∈ w and ¬P_{=u}γ ∈ w or ¬P_{=su}(β ∧ γ) ∈ w and P_{=u}γ ∈ w. In the former case μ(w)([β ∧ γ]) = su and μ(w)([γ]) = t, t ∉ {0, u}. It follows that \frac{μ(w)([β∧γ])}{μ(w)([γ])} ≠ s, a contradiction since w ⊧ CP_{=s}(β, γ). In the latter case, we have that u = t, μ(w)([β ∧ γ]) ≠ st and μ(w)([β]) = t, t ≠ 0, which implies a contradiction in the same way as above. Thus, CP_{=s}(β, γ) ∈ w.

Let α = CP_{⩾s}(β, γ). Suppose that CP_{⩾s}(β, γ) ∈ w. From Theorem 5.4. 8 and Theorem 5.4. 9, there is exactly one t ⩾ s such that CP_{=t}(β, γ) ∈ w, and w ⊧ CP_{=t}(β, γ). It follows that w ⊧ CP_{⩾s}(β, γ). For the other direction, suppose that w ⊧ CP_{⩾s}(β, γ). If μ(w)([γ]) = 0, we have that M ⊧ CP_{=1}(β, γ), and since P_{=0}γ ∈ w, by Axiom 10 it follows that CP_{=1}(β, γ) ∈ w. Then, by Axiom 13 we have that CP_{⩾s}(β, γ) ∈ w. Otherwise, let μ(w)([γ]) ≠ 0. From Theorem 5.4. 5 there is exactly one u′ such that P_{=u′}(β ∧ γ) ∈ w, and exactly one u′′ ≠ 0 such that P_{=u′′}γ ∈ w. It means that μ(w)([β ∧ γ]) = u′ and μ(w)([γ]) = u′′, w ⊧ CP_{=u′/u′′}(β, γ), and CP_{=u′/u′′}(β, γ) ∈ w. Since w ⊧ CP_{⩾s}(β, γ), Axiom 12 guarantees that it must be s ⩽ \frac{u′}{u′′}. It follows from Axiom 13 that CP_{⩾s}(β, γ) ∈ w.

Finally, let α = CP_{≈r}(β, γ). Suppose that CP_{≈r}(β, γ) ∈ w. If μ(w)([γ]) = 0, it follows that w ⊧ CP_{≈1}(β, γ), and by the axioms 10 and 17 that CP_{≈1}(β, γ) ∈ w. By Theorem 5.4. 10 we have that r = 1 and w ⊧ CP_{≈r}(β, γ). Next, suppose that μ(w)([γ]) ≠ 0. From the axioms 15 and 16 we have that for every rational r_{1} ∈ [0, r), CP_{⩾r_{1}}(β, γ) ∈ w, and for every rational r_{2} ∈ (r, 1], CP_{⩽r_{2}}(β, γ) ∈ w. Suppose that w |̸= CP_{≈r}(β, γ). It means that there is some t ∈ S such that t ≠ r and μ(w)([γ]) > 0, \frac{μ(w)([β∧γ])}{μ(w)([γ])} = t and CP_{=t}(β, γ) ∈ w. Furthermore, there must be an interval [r_{1}, r_{2}] containing r such that r_{1} and r_{2} are rational and t ∉ [r_{1}, r_{2}]. If it is not the case, w ⊧ CP_{≈r}(β, γ). Suppose that t < r. According to Axiom 12, ¬CP_{⩾r_{1}}(β, γ) ∈ w, a contradiction. The similar conclusion follows from the assumption that t > r. It follows w ⊧ CP_{≈r}(β, γ). For the other direction, suppose that w ⊧ CP_{≈r}(β, γ). Then, w ⊧ CP_{⩾r′}(β, γ) for every rational r′ < r and w ⊧ CP_{⩽r′′}(β, γ) for every rational r′′ > r. However, if CP_{≈r}(β, γ) ∉ w, by the step 2d of the construction in Theorem 5.3, there must be some rational r_{1} < r (or r_{2} > r) such that ¬CP_{⩾r_{1}}(β, γ) ∈ w (or ¬CP_{⩽r_{2}}(β, γ) ∈ w) which contradicts consistency of w. Thus, CP_{≈r}(β, γ) ∈ w. □

6. Conclusion

In this paper we consider a language, a class of probabilistic models and a sound and complete axiomatic system for reasoning about conditional probabilities.

We are aware of only one paper [6] in which conditional probability is defined syntactically. The approach taken there includes among the axioms the complicated machinery of real closed fields. It is needed to obtain the sound and complete axiomatization. In our approach, since the parts of field theory are moved to the meta theory, the axioms are rather simple. Also, we are able to prove the extended completeness theorem (‘every consistent set of formulas has a model’) which is impossible for the system in [6], although at a price of introducing infinitary deduction rules.

Note that in the canonical LICP_{Meas}^{S}-model M = ⟨W, Prob, v⟩ constructed above, for all w, w′ ∈ W, the following conditions hold:

• W (w) = W (w′) and

• H(w) = H(w′).

Thus, the same proof can be used to show that Ax_{LICP^{S}} is complete with respect to the subclass of LICP_{Meas}^{S} containing only models that satisfy those conditions.

As we mentioned in the introduction, a fragment of the presented logic (denoted LP P^{S}) is used in [21, 22] to model defaults. Besides the mentioned syntactical restrictions in LP P^{S}, we use there an additional semantical requirement called “neatness”. The requirement means that only the empty set has the zero probability and it is important in modelling default reasoning. In this paper we do not consider the “neatness”-condition, but, following the ideas from [22], we can easily handle it. The only change in the completeness proof concerns an additional step in building a maximal consistent extension of a set of formulas, where we have to add the following step: if the current extension of the considered consistent set is enlarged by P_{=0}α, then ¬α must be added as well. In allowing the nesting of probabilistic operators our logic resembles conditional logic [3], i.e., it treats the conditional probability operator as a standard binary logical operator (except that it has a denumerable list of such operators). However, our logic is much more expressive since it also includes the (absolute) probability operators (P_{⩾s}) which behave like a sort of modal operators. This enables us to combine defeasible and probabilistic knowledge in the same context.

There are many possible directions for further investigations. For example, the question of decidability of our logic naturally arises. In [6] decidability of a similar logic was proven. For the present approach the problem is still open since we do not consider real-valued probabilities, but the range of probability is the unit interval of a recursive nonarchimedean field.

References

[1] N. Alechina, Logic with probabilistic operators, in: A. Nieuwendijk (Ed.), Proc. of the AC-COLADE ’94, 1995, 121–138.

[2] F. Bacchus, L_{p}, A logic for representing and reasoning with statistical knowledge, Comput. Artif. Intell. 6 (1990), 209–231.

[3] J. Burgess, Quick completeness proofs for some logics of conditionals, Notre Dame J. Formal Logic 22(1) (1981), 76–84.

[4] R. -Dor - dević, M. Rašković, and Z. Ognjanović, Completeness theorem for propositional probabilistic models whose measures have only finite ranges, Arch. Math. Logic 43 (2004), 557–563.

[5] R. Fagin, and J. Halpern, Reasoning about knowledge and probability, J. ACM 41(2) (1994), 340–367.

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

[7] T. Flaminio, F. Montagna, A logical and algebraic treatment of conditional probability, in: L. A. Zadeh (Ed.), Proceedings of IPMU ’04, Perugia, Italy, 2004, 493–500.

[8] N. Friedman and J. Halpern, Plausibility measures and default reasoning, J. ACM 48(6) (2001), 648–685.

[9] A. Frish and P. Haddawy, Anytime deduction for probabilistic logic, Artif. Intell. 69 (1994), 93–122.

[10] W. van der Hoeck, Some consideration on the logics P_{F} D, J. Non-Classical Log. 7(3) (1997), 287–307.

[11] J. Keisler, Elementary Calculus. An Infinitesimal Approach, 2nd ed. Prindle, Weber and Schmidt, Boston, Massachusetts, 1986.

[12] D. Lehmann and M. Magidor, What does a conditional knowledge base entail?, Artif. Intell. 55 (1992), 1–60.

[13] T. Lukasiewicz, Probabilistic default reasoning with conditional constraints, Ann. Math. Artif. Intell. 34(1–3) (2002), 35–88.

[14] E. Marchioni, L. Godo, A Logic for Reasoning about Coherent Conditional Probability: A Modal Fuzzy Logic Approach, in: J. J. Alfares and J. Leite (Eds.), Proc. of the 9th European Conference Logics in Artificial Intelligence, Lecture Notes Comp. Sci. 3229 (2004), 213–225.

[15] Z. Marković, Z. Ognjanović, and M. Rašković, A probabilistic extension of intuitionistic logic, Math. Log. Q. 49 (2003), 415–424.

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

[17] N. Nilsson, Probabilistic logic revisited, Artif. Intell. 59 (1993), 29–42.

[18] Z. Ognjanović, and M. Rašković, Some probability logics with new types of probability operators, J. Log. Comput. 9(2) (1999), 181–195.

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

[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ć, and Z. Marković, A Probabilistic Approach to Default Reasoning; in: J. Delgrande, T. Schaub (Eds.), Proc. of the NMR ’04, 2004, 335–341

[22] M. Rašković, Z. Ognjanović, and Z. Marković, A Logic with Conditional Probabilities; in: J. J. Alfares and J. Leite (Eds.), Proc. of the 9th European Conference Logics in Artificial Intelligence, Lecture Notes Comp. Sci. 3229 (2004), 226–238.

[23] A. Robinson, Non-Standard Analysis, North-Holland, Amsterdam 1966.

Matematički institut SANU (Received 08 11 2004) Kneza Mihaila 35 (Revised 29 12 2005) 11001 Beograd, p.p. 367 Serbia and Montenegro

      zorano@mi.sanu.ac.yu
      zoranm@mi.sanu.ac.yu
    miodragm@mi.sanu.ac.yu