PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 90(104) (2011), 13–22 DOI: 10.2298/PIM1104013D

A LOGIC WITH BIG-STEPPED PROBABILITIES THAT CAN MODEL NONMONOTONIC REASONING OF SYSTEM P

Dragan Doder

Communicated by Žarko Mijajlović

Abstract. We develop a sound and strongly complete axiomatic system for probabilistic logic in which we can model nonmonotonic (or default) reasoning. We discuss the connection between previously developed logics and the two sublogics of the logic presented here.

1. Introduction

Since Kraus, Lehmann and Magidor introduced the set of rules called System P, which naturally determines properties of a nonmonotonic consequence relation (see [9]), several different semantics were proposed for it (see [2, 7, 9, 11]). Among others, two of them are probabilistic: a nonstandard, and a standard. The first one inspired the paper [18], where the probabilistic logic LP P^{S}, which is appropriate for modeling nonmonotonic reasoning, is presented. In the logic LP P^{S}, the range of probabilistic functions is chosen to be the unit interval of a recursive nonarchimedean field. This paper uses standard probabilistic semantics to develop the corresponding probabilistic logic with formulas that can model the consequence relation of System P.

From the technical point of view, we have modified the techniques presented in [4, 12, 13, 14, 15, 17], where a Henkin-like construction was used.

The rest of the paper is organized as follows. In Section 2 we motivate our approach, discuss the related papers and define some basic notions. The set of formulas of our logic and the corresponding class of probabilistic models are presented in Section 3. In Section 4 we present the axiomatic system and we prove the Completeness theorem. The relationship with logics LP P_{2} and LP P_{2,⪯} , developed in [13] and [17], respectively, is discussed in Section 5.

2010 Mathematics Subject Classification: Primary: 03B48.

Partially supported by Ministarstvo prosvete i nauke Republike Srbije, through Matematički Institut, project ON174026.

2. Preliminaries and related work

Defaults are rules with exceptions, which allow inferring defeasible conclusions from available, but incomplete information. They are often represented by the corresponding binary consequence relation |∼, where the intended meaning of α |∼ β is “if α, then generally β". Here, α and β are assumed to be the propositional formulas from For_{P}, the set of formulas obtained from a set of propositional letters P. The relation |∼ is nonmonotonic in the sense that α |∼ β does not imply α∧γ |∼ β. Kraus, Lehmann and Magidor [9] proposed a set of properties, named System P (for preferential), that any nonmonotonic consequence relation should satisfy. The rules of System P are the following:^{1} ^{2}

REF : \overline{α |∼ α} ;  LLE : \frac{⊢ α ↔ β, α |∼ γ}{β |∼ γ} ;
RW : \frac{⊢ α → β, γ |∼ α}{γ |∼ β} ; AND : \frac{α |∼ β, α |∼ γ}{α |∼ β ∧ γ} ;
OR : \frac{α |∼ γ, β |∼ γ}{α ∨ β |∼ γ} ;  CM : \frac{α |∼ β, α |∼ γ}{α ∧ β |∼ γ} .

In [11] a nonstandard probabilistic semantics for System P has been developed: α |∼ β iff the conditional probability of β given α equals 1 − ε, where ε is a positive infinitesimal. It is easy to show that replacing ε with a positive standard number would lead to the failure of the inference rules of System P (for the approximations of default rules if we replace ε with \frac{1}{n}, we refer the reader to [5]). The paper [2] used a special subclass of probability measures to provide a standard semantics for System P, assuming that the set of propositional letters P is finite. By (standard) probability measure on For_{P} we assume a function μ : For_{P} −→ [0, 1] which satisfies

(1) μ(α) = 1, whenever α is a tautology,

(2) μ(α ∨ β) = μ(α) + μ(β), whenever α ∧ β is a contradiction. Conditional probabilities are defined in the usual way: if μ(α) ≠ 0, then μ(β | α) = \frac{μ(α∧β)}{μ(α)} . A probability measure μ is neat if μ(α) = 0 implies that α is a contradiction. It is shown in [2] that the standard probabilistic semantics for System P is given by so called big-stepped probabilities, i.e., the neat probability measures that satisfy the conditions

(3) ∑ _{at′∈At_{P} ,μ(at′)<μ(at)} μ(at′) < μ(at), for all at ∈ At_{P}, and

(4) μ(at) = μ(at′) iff ⊢ at ↔ at′, for all at, at′ ∈ At_{P},

where P = {p_{1}, p_{2}, …, p_{n}} and At_{P} = {±p_{1} ± p_{2} ± ⋯± p_{n}| + p_{i} = p_{i}, −p_{i} = ¬p_{i}} is the set of atoms of F or_{P}. Restricting ourselves to the class of big-stepped probabilities, we can interpret a default rule of the form α |∼ β as

(2.1)  μ(β|α) > μ(¬β|α),

1REF –reflexivity, LLE–left logical equivalence, RW –right weakening, CM–cautious monotonicity.

2For some other rules proposed for nonmonotonic reasoning we refer the reader to [3, 6, 10 ].

A LOGIC WITH BIG-STEPPED PROBABILITIES THAT CAN MODEL NONMONOTONIC…15

or, equivalently,

(2.2)  μ(β|α) > \frac{1}{2}.

It is well known that conditions (1) and (2) are expressible in a logic that enriches the classical propositional calculus with probabilistic operators of the form P_{⩾r} (r ∈ ℚ ∩ [0, 1]), which are applied to propositional formulas (see, for example, [13, 15]). On the other hand, condition (3) is naturally expressible in the logic presented in [8], in which the sum of probabilities is allowed in the syntax. Conditions (2.1) and (2.2) are expressible in the logic from [4], where [8] is generalized by introducing a conditional probability operator.

Our aim is to develop a simpler logic, with probabilistic operators of the form P_{⩾r} (P_{⩾r}α has the intended meaning “the probability of α is at least r") and a simple set of axioms, in which default rules are still expressible. It will turn out (see Section 4) that it is enough to enrich the syntax with the qualitative probability formulas of the form α ⪯ β (the meaning is “β is at least probable as α"), as in [17]. Also, although the condition (2.2) is naturally expressible in logics with conditional probability operators (see [16, 18]), we can express (2.1) using P_{⩾r}, since 2.1 is equivalent to

(2.3)  μ(β ∧ α) > μ(¬β ∧ α),

whenever α is not a contradiction. Consequently, System P can be modeled in the logic LP P_{2,⪯} from [17], an extension of propositional calculus (it contains both classical and probabilistic formulas), with a special kind of Kripke models as semantics. In the rest of the paper, we will present a purely probabilistic logic, with more intuitive semantics, that can model defaults.

3. Syntax and semantics of LBSP

Let P = {p_{1}, p_{2}, …, p_{n}} be the set of propositional letters, let For_{P} the corresponding set of formulas and At_{P} the set of atoms of For_{P}. We will denote the elements of For_{P} by α, β and γ, primed or indexed if necessary. The set of formulas For of the logic LBSP is the smallest set which satisfies the following conditions:

– {P_{⩾r}α, α ⪯ β | α, β ∈ For_{P}, r ∈ ℚ ∩ [0, 1]} ⊆ For,

– if ϕ, ψ ∈ For, then ϕ ∧ ψ, ¬ϕ ∈ For.

The other Boolean connectives (∨, → and ↔) are introduced as in the propositional case. The formulas of LBSP will be denoted by ϕ, ψ and θ (primed or indexed if necessary). To simplify notation, we introduce the following abbreviations:

– P_{<r} α is ¬P_{⩾r}α,

– α ≺ β is α ⪯ β ∧ ¬β ⪯ α,

– P_{⩽r}α, P_{>r} α, P_{=r} α, α ⪰ β and α ≻ β are defined in a similar way. The semantics for the logic LBSP consists of the class of big-stepped proba-

bilities on For_{P}, denoted by Meas_{BS}^{P} . For μ ∈ Meas_{BS}^{P} , we define the satisfiability relation ⊧ recursively as follows:

• μ ⊧ P_{⩾r}α if μ(α) ⩾ r,

• μ ⊧ α ⪯ β if μ(α) ⩽ μ(β),

• M ⊧ ¬ϕ if M |̸= ϕ,
• M ⊧ ϕ ∧ ψ if M ⊧ ϕ and M ⊧ ψ.

We say that a formula ϕ is satisfiable, if there is a measure μ ∈ Meas_{BS}^{P} such that μ ⊧ ϕ. A set T of formulas is satisfiable if there is μ ∈ Meas_{BS}^{P} such that μ ⊧ ϕ for all ϕ ∈ T. The formula ϕ is valid if μ ⊧ ϕ for all μ ∈ Meas_{BS}^{P} .

Remark 3.1. Note that, by (2.3), the formula

(α ∧ ¬β ≺ α ∧ β) ∨ P_{=0} α

models α |∼ β, where |∼ is the consequence relation of System P.

4. A complete axiomatization

In this section we will introduce the axiomatization for the logic LBSP, and we will prove that the axiomatization is sound and strongly complete with respect to the class of models Meas_{BS}^{P} . We denote the axiomatic system below by Ax_{LBSP} .

Axiom Schemes.

A1 all instances of propositional theorems

A2 P_{⩾0}α

A3 P_{=1} α, whenever α is a tautology

A4 P_{>0} α, whenever α is not a contradiction

A5 P_{⩽r}α → P_{<s} α, whenever r < s

A6 P_{<r} α → P_{⩽r}α

A7 P_{=1} (α → β) → (P_{⩾r}α → P_{⩾r}β)

A8 (P_{⩾r}α ∧ P_{⩾s}β ∧ P_{⩾1}(¬α ∨ ¬β)) → P_{⩾min {1,r+s}} (α ∨ β) A9 (P_{⩽r}α ∧ P_{<s} β) → P_{<r+s} (α ∨ β), whenever r + s ⩽ 1 A10 (α ⪯ β ∧ P_{⩾r}α) → P_{⩾r}β A11 (⋀ _{at′∈S} at ≻ at′) → at ≻ ⋁ _{at′∈S} at′, for all S ⊆ At_{P} A12 ⋀ _{at,at′∈At_{P} ,at≠at′} ¬(at ⪯ at′∧ at′ ⪯ at)

Inference rules.

R1 from α and α → β infer β

R2 from φ → P_{⩾r− \frac{1}{k}} α for every k ⩾ \frac{1}{r} infer φ → P_{⩾r}α

R3 from φ → (P_{⩾r}α → P_{⩾r}β) for every r ∈ ℚ ∩ [0, 1] infer φ → α ⪯ β

The inference rule R1 is Modus Ponens. The axioms A2, A3 and A5–A9, together with the rule R2, characterize probability measures. The relationship with the logic LP P_{2} from [13] is discussed in Section 5. The axiom A10 and the inference rule R3 are taken from [17] and characterize a qualitative probability operator. Finally, axioms A4, A11 and A12 ensure that a probability measure is a big-stepped probability.

A formula ϕ is deducible from a set T of sentences (T ⊢_{LBSP} ϕ) 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 (we will write ⊢ instead of ⊢_{LBSP} , if the index is obvious from the context). A formula ϕ is a theorem (⊢ ϕ) if it is deducible from the empty set.

A set of sentences T is inconsistent if there is a formula ϕ such that T ⊢ ϕ ∧ ¬ϕ, otherwise it is consistent. A consistent set T of sentences is maximally consistent if for every ϕ ∈ For, either ϕ ∈ T or ¬ϕ ∈ T.

In the following, we will use some obvious properties of probability measures, such as μ(¬ϕ) = 1 − μ(ϕ) and μ(ϕ ∨ ψ) = μ(ϕ) + μ(ψ) − μ(ϕ ∧ ψ).

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

Proof. The theorem can be proved using the transfinite induction on the length of the inference. The form of the infinitary inference rules R2 and R3 is adopted in order to enable the step of induction in the proof of Deduction theorem: if ψ → θ is obtained (from T ∪ {ϕ}) by an infinitary rule from ψ → θ_{i}, i = 1, 2, …, then, by the induction hypothesis, T ⊢ ϕ → (ψ → θ_{i}), or, equivalently, T ⊢ (ϕ ∧ ψ) → θ_{i}, for i = 1, 2, … Applying the same inference rule, we obtain T ⊢ (ϕ ∧ ψ) → θ, so T ⊢ ϕ → (ψ → θ). □

Lemma 4.1. The above axiomatization is sound with respect to the class of models Meas_{BS}^{P} .

Proof. Using a straightforward induction on the length of the inference. For example, consider the axiom A7.

Suppose that μ ∈ Meas_{BS}^{P} is a big-stepped probability such that μ ⊧ P_{=1} (α → β) and μ ⊧ P_{⩾r}α. By the definition of ⊧, μ(α → β) = 1 and μ(α) ⩾ r. Consequently, μ(¬α)+μ(β) ⩾ 1, so μ(β) ⩾ 1−μ(¬α) = μ(α) ⩾ r. Finally, μ ⊧ P_{⩾r}β. □

In the rest of this section, we will prove the strong version of Completeness Theorem: every consistent set of formulas is satisfiable. Let T be a consistent set of formulas and let ϕ_{0}, ϕ_{1}, … be an enumeration of all formulas in For. We define a completion T^{∗} of T inductively as follows:

(1) T_{0} = T.

(2) If T_{i} is consistent with ϕ_{i}, then T_{i+1} = T_{i} ∪ {ϕ_{i}}.

(3) If T_{i} is inconsistent with ϕ_{i}, then:

(a) if ϕ_{i} is of the form ψ → P_{⩾r}α, then T_{i+1} = T_{i} ∪ \{ψ → ¬P_{⩾r− \frac{1}{n}} α\}, where n is a positive integer such that T_{i+1} is consistent,

(b) if φ_{i} is of the form ψ → α ⪯ β, then T_{i+1} = T_{i} ∪ {ψ → ¬(P_{⩾r}α → P_{⩾r}β)}, where r ∈ ℚ∩[0, 1] is a number such that T_{i+1} is consistent,

(c) otherwise, T_{i+1} = T_{i}.
(4) T^{∗} = ⋃ _{n=0}^{∞} T_{n}.

The existence of the numbers n and r from (a) and (b) is a direct consequence of Deduction Theorem. For example, if we suppose that T_{i} ∪ \{ψ → ¬P_{⩾r− \frac{1}{n}} α\} is inconsistent for all n, we can conclude that

T_{i} ⊢ ψ → P_{⩾r− \frac{1}{n}} α

for all n. By R2, T_{i} ⊢ ψ → P_{⩾r}α, so T would be inconsistent.

The maximality of the set T^{∗} (i.e., for each ϕ ∈ For, either ϕ ∈ T^{∗} or ¬ϕ ∈ T^{∗}) follows directly from the fact that each T_{i} is consistent.

The consistency of T^{∗} follows from the fact that T^{∗} is deductively closed (indeed, T^{∗} ⊢ ⊥ would imply ⊥ ∈ T_{i}, for some i), where that claim follows from the following facts:

(1) any axiom is consistent with each T_{i},

(2) T^{∗} is closed under the inference rules (the proof for R1 is standard, while the proofs for R2 and R3 can be found in [13, 15] and [17] (respectively), where similar completions are constructed, and the proofs of the closeness under the inference rules are essentially the same).

So, the set T^{∗} is maximally consistent.

Theorem 4.2. The above axiomatization is sound and strongly complete with respect to the class of models Meas_{BS}^{P} .

Proof. Soundness follows from Lemma 4.1. In order to construct a model for a consistent set T, we will extend it to a maximally consistent set T^{∗}, as above. We define μ : For_{P} −→ [0, 1] as follows:

μ(α) = sup{r ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{⩾r}α}.

Let us show that μ ∈ Meas_{BS}^{P} . Since μ(⊤) = 1 and the neatness follow from the axioms A3 and A4, it is sufficient to prove

(1) μ(α ∨ β) = μ(α) + μ(β), whenever α ∧ β is a contradiction,

(2) ∑ _{at′∈At_{P} ,μ(at′)<μ(at)} μ(at′) < μ(at), for all at ∈ At_{P},

(3) if μ(at) = μ(at′) then ⊢ at ↔ at′, for all at, at′ ∈ At_{P}.

(1): Let μ(α) = a, μ(β) = b and α ∧ β be a contradiction. Then α → ¬β is a tautology, so, by the axiom A3, ⊢ P_{=1} (α → ¬β). Consequently, T^{∗} ⊢ P_{=1} (α → ¬β) . By A7 and R1 we obtain T^{∗} ⊢ P_{⩾r}α → P_{⩾r}¬β. Since P_{⩾r}¬β is equivalent to ¬P_{⩾1−r} β, we have T^{∗} ⊢ P_{⩾r}α → ¬P_{⩾1−r} β, so sup{r ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{⩾r}α} ⩽ 1 − sup{r ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{⩾r}β}. By the definition of μ we obtain a + b ⩽ 1.

Let r be any rational number such that T^{∗} ⊢ P_{⩾r}α and let s be any rational number such that T^{∗} ⊢ P_{⩾s}β. Since r + s ⩽ a + b ⩽ 1, by A8 we conclude T^{∗} ⊢ P_{⩾r+s} (α ∨ β), so μ(α ∨ β) = sup{r ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{⩾r}(α ∨ β)} ⩾ a + b. Consequently, if a + b = 1, then μ(α ∨ β) = 1.

Let a + b < 1. Suppose that μ(α ∨ β) > a + b. Then there exist numbers r, s ∈ [0, 1] ∩ ℚ such that r > a, s > t and r + s < μ(α ∨ β). By the maximality of T^{∗}, we obtain T^{∗} ⊢ P_{⩽r}α and T^{∗} ⊢ P_{<s} β. By the axiom A9, T^{∗} ⊢ P_{<r+s} (α ∨ β). Finally, μ(α ∨ β) ⩽ r + s; a contradiction.

(2): Let at ∈ At_{P} and let S denote the set {at′ ∈ At_{P} | μ(at′) < μ(at)}. If at′ ∈ S, then {r ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{⩾r}at′} ⊆ {r ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{⩾r}at}. Consequently, T^{∗} ⊢ P_{⩾r}at′ → P_{⩾r}at, for every r ∈ [0, 1] ∩ ℚ. By the inference rule R3 (setting ϕ = ⊤) we obtain

(4.1)  T^{∗} ⊢ at′ ⪯ at.

If T^{∗} ⊢ at ⪯ at′, by A10 we have T^{∗} ⊢ P_{⩾r}at → P_{⩾r}at′ (for all r), and, consequently, μ(at) ⩽ μ(at′); a contradiction. So, by the maximality of T^{∗}, we obtain

(4.2)  T^{∗} ⊢ ¬(at ⪯ at′).

Since (4.1) and (4.2) imply T^{∗} ⊢ at ≻ at′, by the axiom A11 we conclude

(4.3)  T^{∗} ⊢ at ≻ ⋁_{at′∈S} at′.

Specially, T^{∗} ⊢ at ⪰ ⋁ _{at′∈S} at′, and, by A10, T^{∗} ⊢ P_{⩾r} ⋁ _{at′∈S} at′ → P_{⩾r}at. Consequently, μ(⋁ _{at′∈S} at′) ⩽ μ(at). On the other hand, if μ(at) ⩽ μ(⋁ _{at′∈S} at′), by the definition of μ we obtain T^{∗} ⊢ P_{⩾r}at → P_{⩾r} ⋁ _{at′∈S} at′, for all r, so, by R3, T^{∗} ⊢ at ⪯ ⋁ _{at′∈S} at′; which is in contradiction with (4.3). Now (2) follows from the equality μ(⋁ _{at′∈S} at′) = ∑ _{at′∈At_{P} ,μ(at′)<μ(at)} μ(at′).

(3): Suppose that there exist at, at′ ∈ At_{P} so that at ≠ at′ and μ(at) = μ(at′). Then T^{∗} ⊢ P_{⩾r}at → P_{⩾r}at′ holds for every r ∈ ℚ ∩ [0, 1]. By R3, we obtain T^{∗} ⊢ at ⪯ at′. Similarly, from T^{∗} ⊢ P_{⩾r}at′ → P_{⩾r}at (for every r ∈ ℚ ∩ [0, 1]) we obtain T^{∗} ⊢ at′ ⪯ at, which contradicts the consistency of T^{∗} (by the axiom A12).

Thus, μ is a big-stepped probability, and it is sufficient to prove that T^{∗} ⊢ ϕ iff μ ⊧ ϕ. The proof is by the induction on complexity of formulas; the case when ϕ is of the form P_{⩾r}α follows from the definition of μ, while the cases when it is a conjunction or a negation are standard.

Let T^{∗} ⊢ α ⪯ β. If T^{∗} ⊢ P_{⩾r}α, then, by the axiom A10, T^{∗} ⊢ P_{⩾r}β, so μ(α) ⩽ μ(β), or, equivalently, μ ⊧ α ⪯ β.

Conversely, let μ(α) ⩽ μ(β). By the definition of μ we obtain

{r ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{⩾r}α} ⊆ {r ∈ [0, 1] ∩ ℚ | T^{∗} ⊢ P_{⩾r}β},

so T^{∗} ⊢ P_{⩾r}α → P_{⩾r}β, for r ∈ [0, 1] ∩ ℚ. Finally, by R3, T^{∗} ⊢ α ⪯ β. □

5. On the relationship with the logics LPP_{2} and LPP_{2,⪯}

In this section we will compare the logic LBSP with the logics LPP_{2} and LPP_{2,⪯} (see [13, 17]). In the rest of the paper we assume that |P| ⩽ ℵ_{0}. Also, for a logic L, we will denote the corresponding inference relation by ⊢_{L}.

The set of formulas of LPP_{2} is For_{P} ∪ For_{1}, where For_{1} is the set of all formulas from For in which the symbol ⪯ does not occur. Obviously, neither mixing of pure propositional formulas and probability formulas, nor nested probability operators are allowed. The logic LPP_{2} contains the axioms A1, A2, A5, A6, A8 and A9, the inference rules R1 and R2, as well as the rule:

R4 From α infer P_{⩾1}α.

Let us denote by LP_{2} the sublogic of LBSP with the set of formulas For_{1} and with the axiomatic system consisting of the axioms A1–A3, A5–A9 and the inference rules R1 and R2. The following theorem shows that, if we identify knowledge represented by the formula α ∈ For_{P} with probabilistic knowledge represented by the formula P_{⩾1}α ∈ For_{1}, the strength of LP_{2} is equal to the strength of LPP_{2}.

Theorem 5.1. Let T ⊆ For_{P} ∪ For_{1}, and let T_{1} = {P_{⩾1}α | α ∈ T ∩ For_{P}} ∪

(T ∩ For_{1}). Then:

(1) if T ⊢_{LPP _{2}} α, then T_{1} ⊢_{LP _{2}} P_{⩾1}α, α ∈ For_{P},
(2) T ⊢_{LPP _{2}} ϕ iff T_{1} ⊢_{LP _{2}} ϕ, ϕ ∈ For_{1}.

Proof. (1): Suppose that T ⊢_{LPP _{2}} α. Then T ∩ For_{P} ⊢_{LPP _{2}} α and any proof of α is finite. Let α_{0}, α_{1}, α_{2}, …, α_{n} = α be a proof of α. Note that every α_{i} is an instance of A1 or a formula from the set T ∩ For_{P}, or it is derived from the preceding formulas by the inference rule R1. Suppose that the inference rule R1 is used in the proof m times. Let α_{k} be the first formula in the proof obtained by R1. Then there exist i, j < k and β such that α_{i} = β and α_{j} = β → α_{k}. From P_{=1} (β → α_{k}) and A7_{1} = P_{=1} (β → α_{k}) → (P_{=1} β → P_{=1} α_{k}) (the instance of A7) we conclude (by R1) (P_{=1} β → P_{=1} α_{k}). From the previous formula and P_{=1} β we have P_{=1} α_{k}. Thus, A7_{1}, P_{=1} α_{i}, P_{=1} α_{j} , P_{=1} α_{k} is the proof of P_{=1} α_{k} in LP_{2}. For i ⩽ m, let us denote by A7_{i} the instance of A7 obtained, analogously as for the above A_{1}, from the i-th application of modus ponens in the proof. Continuing, we obtain that A7_{1}, A7_{2}, …, A7_{m}, P_{=1} α_{0}, P_{=1} α_{1}, P_{=1} α_{2}, …, P_{=1} α_{n} = P_{=1} α is the proof of P_{=1} α, thus {P_{⩾1}α | α ∈ T ∩ For_{P}} ⊢_{LP _{2}} P_{⩾1}α.

(2): Let T ⊢_{LPP _{2}} ϕ and let Θ_{0}, Θ_{1}, Θ_{2}, …, Θ_{λ} = ϕ be a proof of ϕ (Θ_{i} ∈ For_{P} ∪ For_{1}). We modify the proof, as in (1), replacing any formula Θ_{j} ∈ For_{P} with P_{⩾1}Θ_{j}, and adding an instance of A7 for every application of R1.

For the other direction, note that the axioms A3 and A7 are theorems of the logic LPP_{2}. □

The logic LPP_{2,⪯} has the set of formulas For_{P} ∪ For, and it contains the axioms A1, A2, A5, A6, A8, A9, A10 and the axiom

A13 (P_{⩽r}α ∧ P_{⩾r}β) → α ⪯ β. The inference rules of LPP_{2,⪯} are R1–R4.

Remark 5.1. The axiom A13 is redundant in LPP_{2,⪯} and it is a theorem of LBSP. Indeed, from P_{⩽r_{1}} α ∧ P_{⩾r_{1}} β we obtain P_{⩽r_{1}} α, P_{⩾r_{1}} β and P_{⩾r_{1}} α → P_{⩾r_{1}} β.

– Let r ∈ (r_{1}, 1] ∩ ℚ. From P_{⩽r_{1}} α, by A5 we obtain P_{<r} α, or, equivalently,

¬P_{⩾r}α. Consequently, P_{⩾r}α → P_{⩾r}β.

– Let r ∈ [0, r_{1}) ∩ ℚ. From P_{⩾r_{1}} β we obtain P_{⩽1−r_{1}} ¬β. By A5 we conclude P_{<1−r} ¬β. Consequently, P_{⩽1−r} ¬β, or, equivalently, P_{⩾r}β. Finally,

P_{⩾r}α → P_{⩾r}β.
We proved that ⊢ (P_{⩽r_{1}} α ∧ P_{⩾r_{1}} β) → P_{⩾r}α → P_{⩾r}β holds for every r ∈

[0, 1] ∩ ℚ. By R3 we obtain ⊢ (P_{⩽r_{1}} α ∧ P_{⩾r_{1}} β) → α ⪯ β. □

Let LP_{2,⪯} be the sublogic of LBSP with the axioms A1–A3, A5–A10 and the inference rules R1–R3. Note that the axiomatization LP_{2,⪯} is obtained by adding the axiom A10 and the inference rule R3 to the axiomatic system of LP_{2}. By Remark 5.1, we may also obtain that adding A10 and R3 to LPP_{2} results with logic LPP_{2,⪯} . Using Theorem 5.1, we conclude:

Corollary 5.1. Let T ⊆ For_{P} ∪ For, and let T_{1} = {P_{⩾1}α | α ∈ T ∩ For_{P}} ∪

(T ∩ For). Then:

(1) if T ⊢_{LPP _{2,⪯}} α, then T_{1} ⊢_{LP_{2,⪯}} P_{⩾1}α, α ∈ For_{P},

(2) T ⊢_{LPP _{2,⪯}} ϕ iff T_{1} ⊢_{LP_{2,⪯}} ϕ, ϕ ∈ For.

6. Conclusion

One of the most prominent applications of probability logics is the mathematical representation of uncertainty. As it was shown by Lehmann and Magidor [11], hyperreal-valued probabilities provide natural semantics for default reasoning. According to the results of Benferhat, Dubois and Prade [2], big-stepped probabilities can be used for the alternative, real-valued representation of defaults.

This paper deals with the problem of developing an axiomatic system with the class of big-stepped probability distributions as semantics. Strong completeness of the system, named LBSP, is proved using a Henkin-like construction, along the line of research presented in [4, 12, 13, 14, 15, 17]. By [2], the consequence relation of System P can be modelled in the logic LBSP.

Our axiomatic system is infinitary, since it is the only nontrivial way to obtain real-valued strongly complete probabilistic logic. Namely, one of the main axiomatization issues for real valued probability logics is the noncompactness phenomena. For example, the set of formulas T = \{P_{>0} α\} ∪ \{P_{⩽ \frac{1}{n}} α | n ∈ ω\} is finitely satisfiable but it is not satisfiable. Consequently, any finitary axiomatic system would be incomplete. Thus, infinitary axiomatizations are the only way to establish strong completeness.

Acknowledgments

The author would like to thank the anonymous referee for the comments that have helped clarify a number of points, eliminate mistakes and improve the text.

References

1. C. Beierle and Gabriele Kern-Isberner, The Relationship of the Logic of Big-Stepped Probabilities to Standard Probabilistic Logics, Lect. Notes Comput. Sci. 5956 (2010), 191–210.

2. S. Benferhat, D. Dubois and H. Prade, Possibilistic and standard probabilistic semantics of conditional knowledge bases, J. Log. Comput. 9(6) (1999), 873–895.

3. Hassan Bezzazi, David Makinson and Ramón Pino Pérez, Beyond Rational Monotony: Some Strong Non-Horn Rules for Nonmonotonic Inference Relations, J. Log. Comput. 7(5) (1997), 605–631.

4. D. Doder, B. Marinković, P. Maksimović and A. Perović, A logic with conditional probability operators, Publ. Inst. Math., Nouv. Sér. 87(101) (2010), 85–96.

5. D. Doder, M. Rašković, Z. Marković and Z. Ognjanović, Measures of inconsistency and defaults, Internat. J. Approx. Reasoning 51 (2010), 832–845.

6. D. Doder, A. Perović and Z. Ognjanović, Probabilistic Approach to Nonmonotonic Consequence Relations, ECSQARU, Lect. Notes Artif. Intell. 6717 (2011), 459–471.

7. D. Dubois and H. Prade, Conditional objects, possibility theory and default rules; in: G. Crocco et al. (eds.), Conditionals: From Philosophy to Computer Science, Oxford University Press, 1995, 311–346.

8. R. Fagin, J. Y. Halpern and N. Megiddo, A logic for reasoning about probabilities, Inform. Comput. 87(1-2) (1990), 78–128.

9. S. Kraus, D. Lehmann and M. Magidor, Nonmonotonic reasoning, preferential models and cumulative logics, Artif. Intell. 44 (1990), 167–207.

10. H. E. Kyburg Jr., C. M. Teng and G. R. Wheeler, Conditionals and consequences, J. Appl. Log. 5(4), (2007), 638–650.

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

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

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

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

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

16. 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.

17. Z. Ognjanović, A. Perović and M. Rašković, Logics with the Qualitative Probability Operator, Log. J. IGPL 16(2) (2008), 105–120.

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

Faculty of Mechanical Engineering (Received 22 12 2010) University of Belgrade (Revised 11 08 2010) 11120 Belgrade Serbia

    ddoder@mas.bg.ac.rs