PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 93 (107) (2013), 19–25 DOI: 10.2298/PIM1307019M

A FIRST-ORDER CONDITIONAL PROBABILITY LOGIC WITH ITERATIONS

Miloš Milošević and Zoran Ognjanović

Communicated by Žarko Mijajlović

Abstract. We investigate a first-order conditional probability logic with equality, which is, up to our knowledge, the first treatise of such logic. The logic, denoted LFPOIC^{=} , allows making statements such as: CP_{⩾s} (ϕ, θ), and CP_{⩽s} (ϕ, θ), with the intended meaning that the conditional probability of ϕ given θ is at least (at most) s. The corresponding syntax, semantic, and axiomatic system are introduced, and Extended completeness theorem is proven.

1. Syntax and semantics

The recent papers [1, 3, 6], discuss conditional probability extensions of classic propositional logic, while [2] introduces a first-order conditional probability logic in which iterations of conditional probability operators are not allowed. In this paper, we abandon that restriction and also extend logical language by adding equality, which causes changes in the corresponding syntax and semantics. Solving those issues is the main novelty presented in this paper.

Let [0, 1]_{ℚ} denote the set of all rational numbers from the interval [0, 1]. The language L of the LFOICP^{=} -logic consists of countable sets of variables V ar = {x_{1}, x_{2}, …}, relation symbols R_{i}^{m}, the relation symbol = which is, of course, interpreted rigidly as equality, and function symbols F_{j}^{n}, where m and n are arities of these symbols, logical connectives ∧ and ¬, the quantifier ∀, and binary conditional probability operators CP_{⩾s} and CP_{⩽t} for all s ∈ [0, 1]_{ℚ}, t ∈ [0, 1)_{ℚ}. Constants are function symbols whose arity is 0.

Terms and atomic formulas are defined as in the first-order classical logic with equality. The set of formulas For_{FOICP} ^{=} is the smallest set containing atomic formulas and closed under the following formation rules: if ϕ and θ are formulas, then ¬ϕ, CP_{⩾s}(ϕ, θ), CP_{⩽t}(ϕ, θ), ϕ∧θ and (∀x)ϕ are formulas. We use the standard abbreviations for other connectives, while P_{⩾s}(ϕ) denotes CP_{⩾s}(ϕ, ⊤). A formula ψ is a sentence if no variable is free in ψ. The subset of all sentences is denoted by Sent_{FOICP} ^{=} . We call a set T ⊂ For_{FOICP} ^{=} a theory if T contains only sentences.

2010 Mathematics Subject Classification: 03B48, 03B042, 03B45.

Partially supported by Ministarstvo prosvete i nauke Republike Srbije under grants III44006 and ON174026.

Semantics to the set of LFOICP^{=} -formulas is given in the possible-world style.

Definition 1.1. An LFOICP^{=} -model is a structure M = ⟨W, D, I, Prob⟩ where:

− W is a nonempty set of objects called worlds, − all worlds have a nonempty set D as a domain, − I associates an interpretation of function and relation symbols with every world w ∈ W such that the meanings of the terms are same in all worlds (we say that terms are rigid) and I(w)(R_{i}^{m}) is a subset of D^{m},

− 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 nonempty subset of W, − H(w) is an algebra of subsets of W (w), − μ(w) is a finitely additive probability measure on H(w).

The fact that ϕ ∈ For_{FOICP} ^{=} holds in a world w of some LFOICP^{=} -model M for a valuation v of variables is denoted as (M, w, v) ⊨ ϕ and the notation [ϕ]_{w}^{v} = {u ∈ W (w) | (M, u, v) ⊨ ϕ} is used throughout the paper.

Definition 1.2. Let M = ⟨W, D, I, Prob⟩ be an LFOICP^{=} -model and v be a valuation. The satisfiability of ϕ ∈ For_{FOICP} in w ∈ W for a given valuation v is defined as follows:

− if ϕ is a classical first-order atomic formula, then (M, w, v) ⊨ ϕ if and only if w ⊨ ϕ(\underline{a_{1}}, …, \underline{a_{n}}), where \underline{a_{i}}, i = 1, …, n, are the names for a_{i} = v(w)(x_{i}), and w is considered as a classical first-order model,

− if ϕ ≡ ¬ψ, then (M, w, v) ⊨ ¬ψ if and only if (M, w, v) ⊭ ψ,

− if ϕ ≡ ψ ∧ θ, then (M, w, v) ⊨ ψ ∧ θ if and only if (M, w, v) ⊨ ψ and

(M, w, v) ⊨ θ, − if ϕ ≡ (∀x)ψ(x), then (M, w, v) ⊨ (∀x)ψ(x) if and only if for every d ∈

D(w) (M, w, v) ⊨ ψ(\underline{d}), where \underline{d} is a name for d, − if ϕ ≡ CP_{⩾s}(ψ, θ), then (M, w, v) ⊨ CP_{⩾s}(ψ, θ) if and only if either

μ(w)([θ]_{w}^{v}) = 0, or μ(w)([θ]_{w}^{v}) > 0 and \frac{μ(w)([ψ ∧ θ]_{w}^{v})}{μ(w)([θ]_{w}^{v})} ⩾ s,

− if ϕ ≡ CP_{⩽s}(ψ, θ), then (M, w, v) ⊨ CP_{⩽s}(ψ, θ) if and only if either

μ(w)([θ]_{w}^{v}) = 0 and s = 1, or μ(w)([θ]_{w}^{v}) > 0 and \frac{μ(w)([ψ ∧ θ]_{w}^{v})}{μ(w)([θ]_{w}^{v})} ⩽ s.

We say that a formula ϕ holds in a world w of an LFOICP^{=} -model M and denote it by (M, w) ⊨ ϕ if for every valuation v, (M, w, v) ⊨ ϕ.

Since the satisfiability of a sentence ϕ in w does not depend on the given valuation v, and for all valuations sets [ϕ]_{w}^{v} coincide we denote the set of all worlds u ∈ W (w) of an LFOICP^{=} -model M where ϕ holds by [ϕ]_{w}. We may omit the subscript when the meaning of [ϕ] is clear from the context: if it is written μ(w)([ϕ]), then it is connoted [ϕ] = [ϕ]_{w}.

By the above definition the conditional probability of ϕ given ψ is 1 when μ(w)([ψ]_{w}^{v}) = 0 and we have expanded Kolmogorov’s definition of the conditional probability in a rather usual way following [6] and [7].

Definition 1.3. A formula ϕ ∈ For_{FOICP} ^{=} is satisfiable if there exist an LFOICP^{=} -model M, a world w in M, and a valuation v such that (M, w, v) ⊨ ϕ. A set T of formulas is satisfiable if there exist an LFOICP^{=} -model M, some world w in M, and a valuation v such that (M, w) ⊨ ϕ, for every ϕ ∈ T. A formula ϕ is valid if for every LFOICP^{=} -model M, and every world w from M, (M, w) ⊨ ϕ.

We focus on the class of models satisfying the requirement that for every ϕ ∈ Sent_{FOICP} ^{=} and every w from a model M, [ϕ]_{w} is a measurable set, i.e., [ϕ]_{w} ∈ H(w), and that class will be denoted by LFOICP_{Meas}^{=} . Also, we consider the class LFOICP_{All}^{=} of all LFOICP_{Meas}^{=} -models having property that for each w ∈ W every subset of W (w) is μ(w)− measurable.

Definition 1.4. A probabilistic k-nested implication Φ_{k}(τ, (θ_{i})_{i<ω} ) for the formula τ based on the sequence (θ_{i})_{i<ω} of formulas is defined by recursion:

Φ_{0}(τ, (θ_{i})_{i<ω} ) ≡ θ_{0} → τ, Φ_{k+1} (τ, (θ_{i})_{i<w} ) ≡ θ_{k+1} → P_{⩾1}(Φ_{k}(τ, (θ_{i})_{i<ω} )).

For example Φ_{3}(τ, (θ_{i})_{i<ω} ) ≡ θ_{3} → P_{⩾1}(θ_{2} → P_{⩾1}(θ_{1} → P_{⩾1}(θ_{0} → τ))).

2. Axioms

The axiomatic system Ax_{LFOICP} for LFOICP contains the following axiom schemata:

Axiom 1 all the axioms of the classical propositional logic, Axiom 2 ∀x(ϕ → ψ) → (ϕ → ∀xψ), where x is not a free variable in ϕ and ϕ, ψ ∈ For_{FOICP} , Axiom 3 ∀xϕ(x) → ϕ(t), where ϕ(t) is obtained by substitution of all free occurrences of x in the first-order formula ϕ(x) by the term t which is free for x in ϕ(x), Axiom 4 ∀x(x = x), Axiom 5 ∀x∀y(x = y → (ϕ(x, x) ↔ ϕ(x, y))), for ϕ ∈ For_{FOICP} . Axiom 6 CP_{⩾0}(ϕ, θ), Axiom 7 CP_{<s} (ϕ, θ) → CP_{⩽s}(ϕ, θ), Axiom 8 CP_{⩽s}(ϕ, θ) → CP_{<t} (ϕ, θ), t > s, Axiom 9 P_{>0} (θ) → (CP_{⩾s}(ϕ, θ) ↔ CP_{⩽1−s} (¬ϕ, θ)), Axiom 10 (P_{⩾s}(ϕ) ∧ P_{⩾t}(θ) ∧ P_{⩾1}(¬(ϕ ∧ θ))) → P_{⩾min {1,s+t}} (ϕ ∨ θ), Axiom 11 (P_{⩽s}(ϕ) ∧ P_{<t} (θ)) → P_{<s+t} (ϕ ∨ θ), s + t ⩽ 1, Axiom 12 P_{=0} (θ) → CP_{=1} (ϕ, θ), Axiom 13 (P_{⩾t}(θ) ∧ P_{⩽s}(ϕ ∧ θ)) → CP_{⩽min \{ \frac{s}{t} ,1\}} (ϕ, θ), t ≠ 0 Axiom 14 (P_{⩽t}(θ) ∧ P_{⩾s}(ϕ ∧ θ)) → CP_{⩾min \{ \frac{s}{t} ,1\}} (ϕ, θ), t ≠ 0

and inference rules:

Rule 1 modus ponens,

Rule 2 \frac{ϕ}{∀xϕ} , ϕ ∈ For_{FOICP} , Rule 3 \frac{ϕ}{P_{⩾1}(ϕ)}, ϕ ∈ For_{FOICP} ,

Rule 4 \frac{Φ_{k}(CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} ), for every integer n ⩾ \frac{1}{s}}{Φ_{k}(CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} )} ,

Rule 5 \frac{Φ_{k}(CP_{⩽s+ \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} ), for every integer n ⩾ \frac{1}{1−s}}{Φ_{k}(CP_{⩽s}(ψ, χ), (θ_{i})_{i<ω} )} .

Let us discuss the system Ax_{LFOICP} . The axioms 1–5 and the rules 1 and 2 correspond to the classical first-order reasoning, while the axioms 6–14 concern the probabilistic part of our system. Axiom 6 announces the nonnegativity and Axioms 7 and 8 the monotonicity of the conditional probability. Axiom 9 claims that CP_{⩾s}(ϕ, θ) and CP_{⩽1−s} (¬ϕ, θ) are equivalent if the condition has a positive probability. Axioms 10 and 11 correspond to the finite additivity of measures, while Axioms 12–14 describe the relationship between the conditional and absolute probability. Rule 3 is a form of modal necessitation. Rules 4 and 5 are the generalization of the infinitary rules which correspond to the Archimedean rule for real numbers, and do not occur in the previous papers.

Definition 2.1. ϕ ∈ For_{FOICP} is a theorem, which we denote by ⊢ ϕ, if there exists a denumerable sequence of formulas ϕ_{0}, ϕ_{1}, …, ϕ called the proof, such that each member of the sequence is an instance of some axiom schemata or is obtained from the previous formulas using an inference rule.

ϕ is deducible from a set of sentences T (T ⊢ ϕ) if there is an at most countable sequence of formulas ϕ_{0}, ϕ_{1}, …, ϕ called the proof, such that each member of the sequence is an instance of some axiom schemata, or is contained in T or is obtained from the previous formulas using an inference rule, with the exception that the inference rule 3 can be applied to the theorems only.

Definition 2.2. A theory T is consistent if there is at least one formula from For_{FOICP} which can not be deduced from T. A theory T is maximal consistent if it is consistent and for each ϕ ∈ Sent_{FOICP} , either ϕ ∈ T or ¬ϕ ∈ T.

The set of all formulas which are deducible from T is called the deductive closure of T and denoted by Cn(T). A theory T is deductively closed if T = Cn(T).

3. Soundness and completeness

Some of the following results can be proved in the way analogous to ones presented in [4, 6, 7], so we emphasize only the main differences and new ideas.

Theorem 3.1 (Soundness). The axiomatic system Ax_{LFOICP} ^{=} is sound with respect to the class of LFOICP_{Meas}^{=} -models.

Proof. Axioms 4 and 5 are obviously valid (for the validity of the latter axiom the assumption about constant domains and rigidness of terms is essential), and it remains to prove, using the induction on k, that rule R4 produces a valid formula from a set of valid premises. In fact we are going to show that if in a world w of some model M for a given valuation v holds Φ_{k}(CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} ), for every n ⩾ \frac{1}{s}, then (M, w, v) ⊨ Φ_{k}(CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} ). For the induction basis k = 0 we point out to the above mentioned literature, and assume that it is fulfilled for k = j. Suppose that there are an LFOICP_{Meas}^{=} -model M_{1}, a world w_{1}, and a valuation v_{1}, such that (M_{1}, w_{1}, v_{1}) ⊨ Φ_{j+1} (CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} ) for every n ⩾ \frac{1}{s}, and

(M_{1}, w_{1}, v_{1}) ⊭ θ_{j+1} → P_{⩾1}(Φ_{j} (CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} )).

We conclude (M_{1}, w_{1}, v_{1}) ⊨ θ_{j+1} ∧ ¬P_{⩾1}(Φ_{j} (CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} )), and for each n ⩾ \frac{1}{s}

(M_{1}, w_{1}, v_{1}) ⊨ P_{⩾1}(Φ_{j} (CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} )),

meaning that for each world u from some subset S ⊆ W (w_{1}) whose μ(w_{1}) measure is equal to 1 holds (M_{1}, u, v_{1}) ⊨ Φ_{j} (CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} ). By the induction hypothesis (M_{1}, u, v_{1}) ⊨ Φ_{j} (CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} ) for all worlds from S ⊆ W (w_{1}), μ(w_{1})(S) = 1, implying (M_{1}, w_{1}, v_{1}) ⊨ P_{⩾1}(Φ_{j} (CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} ), and the initial supposition leads to contradiction. □

Theorem 3.2 (Deduction theorem). If T is a theory and ϕ, ψ ∈ Sent_{FOICP} ^{=} , then T ∪ {ϕ} ⊢ ψ if and only if T ⊢ ϕ → ψ.

The proof of Deduction theorem for LFOICP^{=} differs from the proof of the corresponding theorem presented in [4, 6, 7] in the case when infinitary rules are applied. If σ = Φ_{k}(CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} ) is obtained from T ∪ {ϕ} using rule R4, then:

1. T ∪\{ϕ\} ⊢ θ_{k} → P_{⩾1}(Φ_{k−1} (CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} )), for each integer n ⩾ \frac{1}{s} 2. T ⊢ (ϕ ∧ θ_{k}) → P_{⩾1}(Φ_{k−1} (CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} )), for n ⩾ \frac{1}{s}, by the

induction hypothesis and using an instance of the classical propositional tautology (p → (q → r)) ↔ ((p ∧ q) → r) For i ≠ k the sequence (\overline{θ}_{i})_{i<ω} coincides with (θ_{i})_{i<ω} , and \overline{θ}_{k} ≡ ϕ ∧ θ_{k}. Introducing that notation we obtain

3. T ⊢ (ϕ∧θ_{k}) → P_{⩾1}(Φ_{k−1} (CP_{⩾s}(ψ, χ), (\overline{θ}_{i})_{i<ω} )), by the application of the rule R4 on 2

4. T ⊢ ϕ → (θ_{k} → P_{⩾1}(Φ_{k−1} (CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} ))) The next corollary follows from several applications of the previous theorem,

and makes more evident the necessity of imposing rigidness of terms.

Corollary 3.1. x = y → P_{⩾1}(x = y) is a theorem of LFOICP^{=} .

Proof. We deduce as follows:

1) ⊢ ∀x∀y(x = y → (P_{⩾1}(x = x) ↔ P_{⩾1}(x = y))) is an instance of A5,

2) ⊢ P_{⩾1}(x = x) → (x = y ↔ P_{⩾1}(x = y)), is obtained from 1) using A3 and Deduction theorem, and an instance of a propositional tautology (p → (q → r)) ↔ (q → (p → r)),

4) ⊢ P_{⩾1}(x = x), using A4, A3, Deduction theorem and R3,

5) ⊢ x = y → P_{⩾1}(x = y), from 4) and 3) using Modus ponens. □

Lemma 3.1. a) For all s, t ∈ [0, 1]_{ℚ} and ϕ, θ ∈ For_{FOICP} , if s ⩽ t, then ⊢ CP_{⩾t}(ϕ, θ) → CP_{⩾s}(ϕ, θ) . b) For all s, t ∈ [0, 1]_{ℚ}, t ≠ 0 and ϕ, θ ∈ For_{FOICP} , holds ⊢ (P_{=t} (θ) ∧ P_{=s} (ϕ ∧ θ)) → CP_{=min \{ \frac{s}{t} ,1\}} (ϕ, θ).

c) ⊢ P_{⩾1}(ϕ → θ) → (P_{⩾s}(ϕ) → P_{⩾s}(θ)) for all ϕ, θ ∈ For_{FOICP} .

d) P_{⩾1}(ϕ_{1}), P_{⩾1}(ϕ_{2}) ⊢ P_{⩾1}(ϕ_{1} ∨ ϕ_{2}) ∧ P_{⩾1}(ϕ_{1} ∧ ϕ_{2}).

Proof. As an illustration we prove d), while the other statements are left to the reader. We deduce as follows:

1) ⊢ P_{⩾1}(ϕ_{1} → (ϕ_{1} ∨ ϕ_{2})), applying Rule 3 to an instance of a propositional tautology ,

2) ⊢ P_{⩾1}(ϕ_{1} → (ϕ_{1} ∨ϕ_{2})) → (P_{⩾1}(ϕ_{1}) → P_{⩾1}(ϕ_{1} ∨ϕ_{2})), by c) of this lemma,

3) P_{⩾1}(ϕ_{1}) ⊢ P_{⩾1}(ϕ_{1} ∨ϕ_{2}), from 1) and 2) using R1 and Deduction theorem,

4) ⊢ P_{⩾1}(ϕ_{1}) ↔ P_{⩽0}(¬ϕ_{1}), an instance of A9,

5) ⊢ P_{<s} (¬ϕ_{1}) → P_{<s} (¬ϕ_{1} ∧ ϕ_{2}), using similar arguments as above and contraposition,

6) P_{⩽0}(¬ϕ_{1}) ⊢ P_{< \frac{1}{n}} (¬ϕ_{1}), for every n > 0, by A8,

7) P_{⩽0}(¬ϕ_{1}) ⊢ P_{⩽ \frac{1}{n}} (¬ϕ_{1} ∧ ϕ_{2}), for every n > 0, from 5) and 6), and by A7,

8) P_{⩽0}(¬ϕ_{1}) ⊢ P_{⩽0}(¬ϕ_{1} ∧ ϕ_{2}), from 7) using R5,

9) ⊢ P_{⩾1}((¬ϕ_{1} ∧ ϕ_{2}) ∨ (ϕ_{1} ∧ ϕ_{2})) → (P_{>0} (¬ϕ_{1} ∧ ϕ_{2}) ∨ P_{⩾1}(ϕ_{1} ∧ ϕ_{2})), by A11 and contraposition,

10) ⊢ P_{⩾1}(ϕ_{2}) → P_{⩾1}((¬ϕ_{1} ∧ ϕ_{2}) ∨ (ϕ_{1} ∧ ϕ_{2})), using the previous clause of this lemma

11) P_{⩾1}(ϕ_{2}) ⊢ P_{>0} (¬ϕ_{1} ∧ ϕ_{2}) ∨ P_{⩾1}(ϕ_{1} ∧ ϕ_{2}), from 9) and 10),

12) P_{⩾1}(ϕ_{1}) ⊢ P_{⩽0}(¬ϕ_{1} ∧ ϕ_{2}), from 4) and 8),

13) P_{⩾1}(ϕ_{1}), P_{⩾1}(ϕ_{2}) ⊢ P_{⩾1}(ϕ_{1} ∧ ϕ_{2}), from 11) and 12). □

Lemma 3.2. Let T be a consistent theory. Then:

a) for every formula ϕ ∈ For_{FOICP} , either T ∪ {ϕ} or T ∪ {¬ϕ} is consistent;

b) if ¬Φ_{k}(CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} ) ∈ T, then there exists an integer n > \frac{1}{s} such that T ∪ \{θ_{k} → ¬Φ_{k−1} (CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} )\} is consistent. Also, if ¬Φ_{k}(CP_{⩽s}(ψ, χ), (θ_{i})_{i<ω} ) ∈ T, then there exists an integer n > \frac{1}{1−s} such that T ∪ \{θ_{k} → ¬Φ_{k−1} (CP_{⩽s+ \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} )\} is a consistent theory.

Definition 3.1. A set T of formulas is saturated if for each formula of the form ¬(∀x)ϕ(x) which is contained in T there exists a term t such that ¬ϕ(t) ∈ T.

In order to prove the completeness theorem, the following theorem that states that every consistent theory T can be extended to a saturated maximal consistent theory T^{∗} in some broader language is needed.

Theorem 3.3. Let T be a consistent set of sentences in the first-order probability language L, and C a countably infinite set of new constant symbols. Then T can be extended to a saturated maximal consistent theory T^{∗} in the language L^{∗} = L ∪ C.

Proof. Let ϕ_{0}, ϕ_{1}, …, be an enumeration of all sentences in L^{∗}. We define a sequence of theories T_{i}, i ∈ ω as follows:

1) T_{0} = T, 2) if T_{i}∪{ϕ_{i}} is consistent, then T_{i+1} = T_{i}∪{ϕ_{i}}, otherwise T_{i+1} = T_{i}∪{¬ϕ_{i}},

3) if the set T_{i+1} is obtained by adding a formula of the form ¬(∀x)ψ(x) to the set T_{i}, then for some c ∈ C which does not occur in any of the formulas ϕ_{0}, …, ϕ_{i}, we add ¬ψ(c) to T_{i+1} such that T_{i+1} remains consistent,

4) if a formula of the form ¬Φ_{k}(CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} ) is added, then for some positive integer n, θ_{k} → ¬Φ_{k−1} (CP_{⩾s− \frac{1}{m}} (ψ, χ), (θ_{i})_{i<ω} ) is also added to T_{i+1} , so that T_{i+1} is consistent,

5) if a formula of the form ¬Φ_{k}(CP_{⩽s}(ψ, χ), (θ_{i})_{i<ω} ) is added, then for some positive integer m, θ_{k} → ¬Φ_{k−1} (CP_{⩽s+ \frac{1}{m}} (ψ, χ), (θ_{i})_{i<ω} ) is also added to T_{i+1} , so that T_{i+1} is consistent,

6) T^{∗} = ⋃ _{i<ω} T_{i}. T^{∗} has required properties. □

The next corollary summarizes some obvious properties of saturated maximal consistent theories.

Corollary 3.2. Let T be a saturated maximal consistent theory in L and ϕ, ψ ∈ Sent_{L}. Then:

a) if T ⊢ ϕ, then ϕ ∈ T, i.e. every saturated maximal consistent theory is deductively closed;

b) if t = sup{r | P_{⩾r}(ϕ) ∈ T } and t ∈ [0, 1]_{ℚ}, then P_{⩾t}(ϕ), P_{⩽t}(ϕ) ∈ T.

Definition 3.2. A cut theory P_{T}^{−} corresponding to a theory T in the language L is the set of sentences P_{T}^{−} = {ϕ ∈ Sent_{FOICP} ^{=} | P_{⩾1}(ϕ) ∈ T }.

Lemma 3.3. If P_{T}^{−} ⊢ ψ, then T ⊢ P_{⩾1}(ψ).

Proof. We use the transfinite induction on the length of the proof for ψ from P_{T}^{−} . If the proof is finite ψ_{1}, …, ψ_{l}, ψ and T ⊢ P_{⩾1}(ψ_{i}) for each i = 1, …, l, then:

1) ψ_{1} ∧ … ∧ ψ_{l} ⊢ ψ

2) ⊢ P_{⩾1}((ψ_{1} ∧ … ∧ ψ_{l}) → ψ), by Rule 3

3) ⊢ P_{⩾1}((ψ_{1} ∧ … ∧ ψ_{l}) → ψ) → (P_{⩾1}(ψ_{1} ∧ … ∧ ψ_{l}) → P_{⩾1}(ψ)), by Lemma 3.1c)

4) P_{⩾1}(ψ_{1} ∧ … ∧ ψ_{l}) ⊢ P_{⩾1}(ψ), from 2) and 3) using R1 and Deduction theorem

5) P_{⩾1}(ψ_{1}), …, P_{⩾1}(ψ_{l}) ⊢ P_{⩾1}(ψ_{1} ∧ … ∧ ψ_{l}), by Lemma 3.1d)

6) T ⊢ P_{⩾1}(ψ) We consider the case when the proof is infinite ψ_{1}, …, ψ. Suppose that some

ψ_{j} is of the form Φ_{k}(CP_{⩾s}(ψ, χ), (θ_{i})_{i<ω} ), and is obtained by an application of infinitary rule R4 to formulas Φ_{k}(CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} ), n ⩾ \frac{1}{s}, which occur in the proof sequence before ψ_{j}. Thus, by the induction hypothesis, we have that T ⊢ P_{⩾1}(Φ_{k}(CP_{⩾s− \frac{1}{n}} (ψ, χ), (θ_{i})_{i<ω} )) for every n ⩾ \frac{1}{s}, and since (⊤ → p) ↔ p is a tautology, using R4, we conclude T ⊢ P_{⩾1}(ψ). □

The canonical model M for a consistent theory T is defined as follows. From the set T of all maximal saturated extensions in the expanded language L^{∗} we pick one which is a extension of T, denote it by T_{1}, and set that the world w_{1} is T_{1}. Note that P_{T_{1}}^{−} is a consistent theory, since ⊤, P_{⩾1}(⊤), P_{⩾1}(⊤) ↔ P_{⩽0}(⊥) are contained in every maximal theory, T_{1} included, and P_{T_{1}}^{−} ⊢ ⊥ would imply T_{1} ⊢ P_{⩾1}(⊥) contradicting consistency of T_{1}. The corresponding probability space Prob(w_{1}) is determined with

W (w_{1})= {T^{∗} ∈ T | P_{T_{1}}^{−} ⊆ T^{∗}},  [ϕ]_{w_{1}} = {u ∈ W (w_{1}) | ϕ ∈ u},
H(w_{1}) = {[ϕ]_{w_{1}} | ϕ ∈ Sent_{L^{∗}} }, μ(w_{1})([ϕ]_{w_{1}} ) = {s | P_{⩾s}(ϕ) ∈ w_{1}}.

For each element from W (w_{1}) we proceed with this procedure and so on. Let C be the set of all constants from L^{∗}. The relation ∼ on C is defined by c_{i} ∼ c_{j} iff T_{1} ⊢ c_{i} = c_{j}, is an equivalence relation. Domain of the canonical model is D = C/ ∼ and its elements are classes of equivalence c^{∗}. For w ∈ W, I(w) is an interpretation such that:

− for every symbol of constant c_{j}, I(w)(c_{j}) = c^{∗} iff c_{j} = c ∈ w,

− for every function symbol F_{i}^{m}, I(w)(F_{i}^{m}) is a function from D^{m} to D

mapping (c_{1}^{∗}, …, c_{m}^{∗}) to c_{m+1}^{∗} iff F_{i}^{m}(c_{1}, …, c_{m}) = c_{m+1} ∈ w, − for every relation symbol R_{i}^{m}

I(w)(R_{i}^{m}) = {(c_{1}^{∗}, …, c_{m}^{∗}) ∈ D^{m} | R_{i}^{m}(c_{1}, …, c_{m}) ∈ w}.

Corollary 1 guarantees that terms are rigidly interpreted, cause t_{1} = t_{2} ∈ T_{1}, ⊢ t_{1} = t_{2} → P_{⩾1}(t_{1} = t_{2}) implies t_{1} = t_{2} ∈ P_{T_{1}}^{−}. It remains to be proved that M = ⟨W, D, I, Prob⟩ is really an LFOICP_{Meas}^{=} -model showing that H(w) is an algebra of subsets of W (w), μ(w) is a finitely additive measure, and (M, w) ⊨ ϕ iff ϕ ∈ w. Here we provide the proof for one fact, namely we prove that [ϕ]_{w} ⊆ [ψ]_{w} implies μ(w)([ϕ]_{w}) ⩽ μ(w)([ψ]_{w}). For every u ∈ W (w), if ϕ ∈ u then ψ ∈ u, and since u is a maximal theory, it means that ϕ → ψ ∈ u. Thus, P_{w}^{−} ∪ {¬(ϕ → ψ)} is not a consistent theory, and according to Deduction theorem P_{w}^{−} ⊢ ϕ → ψ. Using Lemma 3.3 we obtain w ⊢ P_{⩾1}(ϕ → ψ), and by Lemma 3.1c) and Deduction theorem w ⊢ P_{⩾s}(ϕ) → P_{⩾s}(ψ). We summarize these facts in two following lemmas:

Lemma 3.4. Let M = ⟨W, D, I, Prob⟩ be as above, w ∈ W and let ϕ, ψ be sentences from Sent_{FOICP}^{=} . Then, the following hold:

a) H(w) is an algebra of subsets of W (w),

b) if [ϕ] = [ψ], then μ(w)([ϕ]) = μ(w)([ψ]),

c) if [ϕ] = [ψ], then P_{⩾s}(ϕ) ∈ w iff P_{⩾s}(ψ) ∈ w, and P_{⩽s}(ϕ) ∈ w iff P_{⩽s}(ψ) ∈ w,

d) μ(w) is a finitely additive measure.

Lemma 3.5. M = ⟨W, D, I, Prob⟩, defined as above, is an LFOICP_{Meas}^{=} -model.

Theorem 3.4 (Extended completeness theorem for LFOICP_{Meas}^{=} ). A theory T is consistent if and only if it has an LFOICP_{Meas}^{=} -model.

Proof. The direction from right to left follows from the soundness theorem. The theory T can be extended to some saturated maximal consistent theory w in the expanded language L^{∗}, and for the canonical model M holds (M, w) ⊨ T. □

Theorem 3.5 (Extended completeness theorem for LFOICP_{All}^{=}). A theory T is consistent if and only if it has an LFOICP_{All}^{=}-model.

Proof. Applying the extension theorem for additive measures from [5] it is possible to obtain finitely additive measures on the power set of W whose restrictions are μ(w) from the weak canonical model M. □

References

1. N. Ikodinović, Z. Ognjanović, A logic with coherent conditional probabilities, Proceedings of the 8th European Conference Symbolic and Quantitative Approaches to Reasoning with Uncertainty ECSQARU 2005, Barcelona, Spain, July 6-8, 2005, Lluis Godo (ed.), Lect. Notes Comput. Sci. 3571 (2005), 726–736,

2. M. Milošević, Z. Ognjanović, A first-order probability logic, Log. J. IGPL, 20(1) (2012), 235– 253,

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

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

5. K. P. S. B. Rao, M. B. Rao, Theory of Charges, Academic Press, 1983

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

7. M. Rašković, Z. Ognjanović, Z. Marković, A logic with Conditional Probabilities, in: J. Leite and J. Alferes, (eds.), 9th European Conference Jelia’04 Logics in Artificial Intelligence, Lect. Notes Comput. Sci. 3229 (2004), 226–238,

Mathematical Institute (Received 22 03 2012) Serbian Academy of Sciences and Arts Beograd Serbia

  mionamil@eunet.rs
  zorano@mi.sanu.ac.rs