PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 95 (109) (2014), 73–86 DOI: 10.2298/PIM1409073I

COMPLEX VALUED PROBABILITY LOGICS

Angelina Ilić Stepić and Zoran Ognjanović

Communicated by Miloš Kurilić

Abstract. We present two complex valued probabilistic logics, LCOMP_{B} and LCOMP_{S} , which extend classical propositional logic. In LCOMP_{B} one can express formulas of the form B_{z,ρ} α meaning that the probability of α is in the complex ball with the center z and the radius ρ, while in LCOMP_{S} one can make statements of the form S_{z,ρ} α with the intended meaning – the probability of propositional formula α is in the complex square with the center z and the side 2ρ. The corresponding strongly complete axiom systems are provided. Decidability of the logics are proved by reducing the satisfiability problem for LCOMP_{B} (LCOMP_{S} ) to the problem of solving systems of quadratic (linear) inequalities.

1. Introduction

In measure theory, complex measures generalize the concept of measures by letting them have complex values. It is well known that complex measures are used for characterization of linear functionals on the space of all continuous complex-valued functions that vanish at infinity (Riesz Theorem) [9]. By adding the assumption that the measure of the entire space is equal to 1, we obtain complex valued probabilities [1, 3]. Complex valued probabilities have proven to be useful in applications. For example, in [12] the author considers relativistic quantum mechanics based on complex probability theory. In this approach, a wave function Ψ is not treated as “the state of the system". Ψ represents the best estimate of the complex probability of finding particle at some point in a measure space. Actually, it says what is known about the system. Thus, the collapse of the wave function represents learning a new fact about the system and therefore leads to calculation of new complex probabilities. In this way realistic quantum theory gives simple explanations of several paradoxical problems in quantum mechanics. In [13] complex probabilities are applied to the concepts of degradation of systems and estimation of remaining useful life of faulty components in the field of prognostic based on reliability. Complex probabilities also appear in Markov Stochastic Processes, where in [14] the authors consider the transition probability matrix P of a discrete Markov chain and give a motivating example for calculating P^{r} where n < r < n + 1, for some n ∈ Z. It turns out that, in general, P^{r} is a complex matrix, i.e., it belongs to the class of generalized stochastic matrices.

2010 Mathematics Subject Classification: 03B48, 68T37.

In this paper, we develop two logics for reasoning about complex valued probabilities. Since the field of complex numbers is not ordered, we can not use the standard probabilistic operators of the form P_{⩾r}α, with the intended meaning “The probability of α is greater or equal to r" [4, 5, 6, 7, 8]. We had a similar situation formalizing p-adic valued probabilities [10], where we introduced probabilistic operators of the form K_{r,ρ} α that have the intuitive meaning “The probability of α belongs to the p-adic ball with the center r and the radius ρ". Similarly, in this paper we use complex balls (in the first logic) and squares (in the second logic) to estimate probabilities of events. The main differences between axiomatizations for the logics from [10] and those presented in this paper, as well as in the proofs of the corresponding statements, follow from the fact that the strong triangle inequality holds for p-adic fields, but not for complex numbers.

We consider two logics:

• LCOMP_{B}, with the probabilistic operators B_{z,ρ} α meaning “The probability of α is in the ball with the center z and the radius ρ",

• LCOMP_{S}, with the probabilistic operators S_{z,ρ} α meaning “The probability of α is in the square with the center z and the side 2 · ρ"

For these logics, the corresponding axiom systems with infinitary rules of inference are given and proved to be sound and strongly complete.

Decidability for the logic LCOMP_{B} is proved by reducing the satisfiability problem to the problem of solving systems of quadratic inequalities, which is known to be in PSPACE [1]. For the logic LCOMP_{S} the same reduction can be done to the linear systems solving problem, which implies NP-completeness of the logic.

The rest of the paper is organized as follows: In Sections 2 and 3 we present the logics LCOMP_{B} and LCOMP_{S}, respectively. Section 2 is divided into 4 subsections, within which we present Syntax and Semantics, and then axioms and inference rules, prove the corresponding soundness and completeness and discuss decidability. Finally, the concluding remarks are given in Section 4.

2. The logic LCOMP_{B}

In this section, we present the probability logic LCOMP_{B} in which we use probabilistic operators of the form B_{z,ρ} α. The intended meaning of these operators is: “The probability of α belongs to the ball B[z, ρ]".

Let | · | denote the standard real absolute value, (|x| = x if x ⩾ 0, |x| = −x if x < 0). If C is a field of complex numbers and z = x + iy ∈ C, then we use ∥ · ∥ for the complex norm, ∥x + iy∥ = \sqrt{x^{2} + y^{2}} . Let B[z, ρ] = \{z_{1} ∈ C : ∥z − z_{1}∥ ⩽ ρ\} be a complex ball with the center z and the radius ρ, CQ = {a + ib | a, b ∈ Q} the set of complex numbers with rational coordinates, and Q^{+} the set of all non-negative rationals.

2.1. Syntax and semantics. Suppose that Var is a countable set of propositional letters. By For_{Cl} we will denote the set of all propositional formulas over Var. Propositional formulas will be denoted by α, β and γ. The set For_{CP} of all probabilistic formulas is defined as the least set satisfying the following conditions:

• If α ∈ For_{Cl}, z ∈ CQ, ρ ∈ Q^{+} , then B_{z,ρ} α is a probabilistic formula;

• If φ, ϕ are probabilistic formulas, then (¬φ), (φ ∧ ϕ) are probabilistic formulas. Probabilistic formulas will be denoted by φ, ϕ and θ. The set For of all LCOMP_{B}- formulas is a union of For_{Cl} and For_{CP}. Formulas will be denoted by A, B and C, indexed if necessary. The other classical connectives (∨, ⇒, ⇔) can be defined as usual. We denote both α ∧ ¬α and φ ∧ ¬φ by ⊥, letting the context to determine the meaning. Also, we use ⊤ for α ∨ ¬α and φ ∨ ¬φ.

Definition 2.1. An LCOMP_{B}-model is a structure M = ⟨W, H, μ, v⟩ where:

• W is a nonempty set of elements called worlds;

• H is an algebra of subsets of W;

• μ : H −→ C is a measure (additive function) such that μ(W) = 1;

• v : W × Var → {true, false} is a valuation which associated with every world w ∈ W a truth assignment v(w, ·) on propositional letters; the valuation v(w, ·) is extended to classical propositional formulas as usual.

If M is an LCOMP_{B}-model, we will denote by [α] the set of all worlds w such that v(w, α) = true. An LCOMP_{B}-model M = ⟨W, H, μ, v⟩ is measurable if [α] ∈ H for every formula α ∈ For_{Cl}. In this paper we focus on the class of all measurable LCOMP_{B}-models. Thus, when we write “LCOMP_{B}-model" we mean “measurable LCOMP_{B}-model".

Definition 2.2. Let M = ⟨W, H, μ, v⟩ be an LCOMP_{B}-model. The satisfiability relation ⊧ is inductively defined as follows:

• If α ∈ For_{Cl}„ then M ⊧ α iff v(w, α) = true for every w ∈ W.

• If α ∈ For_{Cl}, z ∈ CQ, ρ ∈ Q^{+} , then M ⊧ B_{z,ρ} α iff ∥μ([α]) − z∥ ⩽ ρ.

• If φ ∈ For_{CP}„ then M ⊧ ¬φ iff it is not M ⊧ φ.

• If φ, ψ ∈ For_{CP}, then M ⊧ φ ∧ ψ iff M ⊧ φ i M ⊧ ψ. □

Note that for all ρ ∈ Q^{+} , z ∈ CQ, M ⊧ B_{z,ρ} α means that μ([α]) belongs to the complex ball with the center z and the radius ρ. If ρ = 0„ then we obtain that the probability of α is equal to z.

2.2. Axiomatization. The axiom system AX_{LCOMP _{B}} of the logic LCOMP_{B} contains the following axioms and inference rules: Axioms A1. Substitutional instances of tautologies; A2. B_{z,ρ} α ⇒ B_{z,ρ′} α, whenever ρ′ ⩾ ρ; A3. B_{z_{1} ,ρ_{1}} α ∧ B_{z_{2} ,ρ_{2}} β ∧ B_{0,0}(α ∧ β) ⇒ B_{z_{1} +z_{2} ,ρ_{1} +ρ_{2}} (α ∨ β); A4. B_{z_{1} ,ρ_{1}} α ⇒ ¬B_{z_{2} ,ρ_{2}} α, if ∥z_{1} − z_{2}∥ > ρ_{1} + ρ_{2}; A5. B_{z_{1} ,ρ_{1}} α ⇒ B_{z_{2} ,ρ_{1} +ρ_{2}} α, if ∥z_{1} − z_{2}∥ ⩽ ρ_{2}; Inference rules R1. From A and A ⇒ B infer B. Here A and B are either both propositional, or

both probabilistic formulas; R2. From α infer B_{1,0}α; R3. If n ∈ N, from φ ⇒ ¬B_{z, \frac{1}{n}} α for every z ∈ CQ, infer φ ⇒⊥; R4. From α ⇒⊥, infer B_{0,0}α; R5. If z ∈ CQ, from φ ⇒ B_{z,ρ+ \frac{1}{n}} α for every n ∈ N, infer φ ⇒ B_{z,ρ} α; R6. From (α ⇔ β), infer (B_{z,ρ} α ⇒ B_{z,ρ} β);

We will briefly discuss the meaning and the scope of the axioms and inference rules. Axiom A1 provides validity of all classical tautologies. Axiom A2 corresponds to the obvious property of balls: a ball of smaller radius is contained in a ball of larger radius. Axiom A3 corresponds to the additivity of measures. Axiom A4 provides that the measure of a formula cannot belong to two disjoint balls. Axiom A5 allows that the following holds: if the measure of α belongs to the ball B, it belongs to some larger ball B′, such that B ⊆ B′.

Rule R2 can be considered as the rule of necessitation in modal logic, but it can be applied only to theorems. Rule R3 provides that for every classical formula α and every n ∈ N, there must be some z ∈ CQ such that the measure of α belongs to the ball B[z, \frac{1}{n}]. Rule R4 guarantees that contradiction has the measure 0. Rule R5 expresses the next property: if the measure of α is arbitrarily close to some number z ∈ CQ„ then the measure of α is equal to z. Finally, rule R6 says that equivalent classical formulas have the same measure. Note that the rules R3 and R5 are infinitary.

Definition 2.3. A formula A is deducible from the set T of formulas (denoted T ⊢ A) if there is a sequence (called a proof) of formulas A_{0}, A_{1}… A_{n}, where A_{n} = A such that every A_{i} is either an instance of some axiom, or it is a formula from the set T, or it can be derived from the preceding formulas by some inference rule. The length of a proof is a successor ordinal. As it is usual, T ⊬ α means that T ⊢ α does not hold. A formula A is a theorem (⊢ A) iff it is deducible from the empty set. A set of formulas T is consistent if there are α ∈ For_{Cl} and φ ∈ For_{CP} such that T ⊬ α and T ⊬ φ. A consistent set T of formulas is said to be maximal consistent if it has the following properties:

• For every α ∈ For_{Cl}, if T ⊢ α„ then both α and B_{1,0}α are in T;

• For every φ ∈ For_{CP}, either φ ∈ T or ¬φ ∈ T. A set of formulas T is deductively closed if for every A ∈ For, if T ⊢ A, then A ∈ T.

2.3. Soundness and completeness.

Theorem 2.1 (Deduction theorem). Let T be a set of formulas and A and B both classical or both propositional formulas. Then, T, A ⊢ B implies T ⊢ A ⇒ B.

Proof. We use transfinite induction on the length of the proof of B from T ∪ {A}. For example, we consider the case where B = (φ ⇒ ⊥) obtained from T ∪ {A} by an application of rule R3 and A ∈ For_{P}. Then for some n ∈ N, α ∈ For_{Cl}:

T, A ⊢ φ ⇒ ¬(B_{z, \frac{1}{n}} α) for every z ∈ CQ T ⊢ A ⇒ (φ ⇒ ¬(B_{z, \frac{1}{n}} α)) for every r ∈ CQ, by induction hypothesis T ⊢ A ∧ φ ⇒ ¬(B_{z, \frac{1}{n}} α) for every r ∈ CQ, by classical reasoning T ⊢ A ∧ φ ⇒ ⊥, by rule R3 T ⊢ A ⇒ (φ ⇒ ⊥). The other cases follow similarly. □

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

Proof. Let T be a consistent theory, \overline{T} the set of all classical formulas that are consequences of T, α_{0}, α_{1},… an enumeration of all formulas from For_{Cl}, and φ_{0}, φ_{1},… an enumeration of all formulas from For_{CP}. Let f : N → N^{2} be any bijection (i.e., f is of the form f(i) = (π_{1}(i), π_{2}(i))^{1}). We define a sequence of theories T_{i} in the following way:

(1) T_{0} = T ∪ \overline{T} ∪ \{B_{1,0}α|α ∈ \overline{T}\};

(2) For every i ⩾ 0, (a) If T_{2i} ∪ {φ_{i}} is consistent, then T_{2i+1} = T_{2i} ∪ {φ_{i}};

(b) Otherwise, if T_{2i} ∪ {φ_{i}} is inconsistent, then:

(i) If φ_{i} = (ψ ⇒ B_{z,ρ} α), then T_{2i+1} = T_{2i} ∪ {¬φ_{i}, ψ ⇒ ¬B_{z,ρ+p^{−n}} α} for some n ∈ N such that T_{2i+1} is consistent,

(ii) Otherwise T_{2i+1} = T_{2i} ∪ {¬φ_{i}};

(3) For every i ⩾ 0, T_{2i+2} = T_{2i+1} ∪ \{B_{z, \frac{1}{π_{1} (i)}} α_{π_{2} (i)} \} for some z ∈ CQ such that T_{2i+2} is consistent.

We show that for every i, T_{i} is consistent.

The set T_{0} is consistent since it contains consequences of a consistent set. The sets obtained by the steps 2a are obviously consistent. The step 2b (ii) produces consistent sets too. For if T_{2i}, φ_{i} ⊢⊥, by Deduction Theorem we have T_{2i} ⊢ ¬φ_{i}, and since T_{2i} is consistent so is T_{2i} ∪ {¬φ_{i}}. Let us consider the step 2b(i). Suppose that φ_{i} = (ψ ⇒ B_{z,0} α), T_{2i} ∪ {φ_{i}} is inconsistent and that for every n ∈ N, T_{2i} ∪ {¬(ψ ⇒ B_{z,0} α), ψ ⇒ ¬B_{z,p^{−n}} α} is inconsistent. Then:

T_{2i}, ¬(ψ ⇒ B_{z,ρ} α), ψ ⇒ ¬B_{z,ρ+ \frac{1}{n}} α ⊢⊥, for every n ∈ N T_{2i}, ¬(ψ ⇒ B_{z,ρ} α) ⊢ ¬(ψ ⇒ ¬B_{z,ρ+ \frac{1}{n}} α), for every n ∈ N, by Deduction

theorem

T_{2i}, ¬(ψ ⇒ B_{z,ρ} α) ⊢ ψ ⇒ B_{z,ρ+ \frac{1}{n}} α, for every n ∈ N, by classical tautology ¬(α ⇒ ¬β) ⇒ (α ⇒ β)

T_{2i}, ¬(ψ ⇒ B_{z,ρ} α) ⊢ ψ ⇒ B_{z,ρ} α, by rule R5 T_{2i} ⊢ ¬(ψ ⇒ B_{z,ρ} α) ⇒ (ψ ⇒ B_{z,ρ} α), by Deduction theorem T_{2i} ⊢ ψ ⇒ B_{z,ρ} α.

x ˙− y = \{ \begin{matrix}x − y & if x ⩾ y \\ 0 & otherwise . \end{matrix}

1For instance, we can consider the function f(x) = (π_{1}(x), π_{2}(x)), where π_{1}(x) = (x + 1)_{1}, π_{2}(x) = [ \frac{1}{2}([ \frac{x+1}{2^{(x+1)1}} ] ˙− 1)]. Here, (x)_{i} is the degree of the i-th prime number in the factorization of x and Note that f is the inverse function of the function F : N^{2} → N, F (m, n) = 2^{m} (2n + 1) − 1.

Since T_{2i} ∪ {ψ ⇒ B_{z,ρ} α} is not consistent, from T_{2i} ⊢ ψ ⇒ B_{z,ρ} α it follows that T_{2i} is not consistent, a contradiction.

Next, consider the step 3. Suppose that for every z ∈ CQ the set T_{2i+1} ∪ \{B_{z, \frac{1}{π_{1} (i)}} α_{\frac{1}{π_{2} (i)}} \} is inconsistent. Let T_{2i+1} = T_{0} ∪ T_{2i+1}^{+} , where T_{2i+1}^{+} is set of all formulas from For_{P} which were added to T_{0} in previous steps of the construction. Then:

T_{0}, T_{2i+1}^{+} , B_{z, \frac{1}{π_{1} (i)}} α_{π_{2} (i)} ⊢⊥, for every z ∈ CQ

T_{0}, T_{2i+1}^{+} ⊢ ¬B_{z, \frac{1}{π_{1} (i)}} α_{π_{2} (i)} for every z ∈ CQ, by Deduction theorem

T_{0} ⊢ (⋀ _{φ∈T_{2i+1}^{+}} φ) ⇒ ¬B_{z, \frac{1}{π_{1} (i)}} α_{π_{2} (i)} , for every z ∈ CQ, by Deduction theorem T_{0} ⊢ (⋀ _{φ∈T_{2i+1}^{+}} φ) ⇒⊥, by rule R3. Therefore T_{2i+1} ⊢⊥, a contradiction. Let T^{∗} = ⋃ _{i<ω} T_{i}. It remains to show that T^{∗} is maximal and consistent. The

steps 1 and 2 of the above construction guarantee that T^{∗} is maximal. We continue by showing that T^{∗} is a deductively closed set which does not contain all formulas, and, as a consequence, that T^{∗} is consistent.

First we show that T^{∗} does not contain all formulas. Let α ∈ For_{Cl}. According to the construction of T_{0}, α and ¬α cannot be simultaneously in T_{0}. Suppose that φ ∈ For_{CP}. Then for some i, j, φ = φ_{i} and ¬φ = φ_{j}. Since T_{max (2i,2j)+1} is consistent, T^{∗} cannot contain both φ and ¬φ.

Next we show that T^{∗} is deductively closed. If α ∈ For_{Cl} and T^{∗} ⊢ α, then by the construction of T_{0}, α ∈ T^{∗} and B_{1,0}α ∈ T^{∗}. Let φ ∈ For_{CP}. Notice that if φ = φ_{j} and T_{i} ⊢ φ_{j}, it must be φ ∈ T^{∗} because T_{max (i,2j)+1} is consistent. Suppose that the sequence φ_{1}, φ_{2}, …φ forms the proof of φ from T^{∗}. If the sequence is finite, there must be a set T_{i} such that T_{i} ⊢ φ. Then, similarly as above, φ ∈ 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 premises belong to T^{∗}, then there must be φ_{i} ∈ T^{∗}. If the rule is a finitary one, then there must be a set T_{j} which contains all premises and T_{j} ⊢ φ_{i}. Reasoning as above, we conclude that φ_{i} ∈ T^{∗}. So, let us now consider the infinitary rules.

Suppose that φ_{i} = (ψ ⇒ ⊥) is obtained from the set \{φ_{z} = (ψ ⇒ ¬B_{z, \frac{1}{n}} α) | z ∈ CQ} of premises, by rule R3 and for some α ∈ For_{Cl}, n ∈ N. By the induction hypothesis φ_{z} ∈ T^{∗} for every z ∈ CQ. By the step 3 of the construction there must be some z′ and some l such that ψ ⇒ B_{z′, \frac{1}{n}} α belongs to T_{l}. Since all premises belongs to T^{∗}, for some k, ψ ⇒ ¬B_{z′, \frac{1}{n}} α ∈ T_{k}. If m = max(l, k), then ψ ⇒ ¬B_{z′, \frac{1}{n}} α, ψ ⇒ B_{z′, \frac{1}{n}} α ∈ T_{m}. Thus T_{m} ⊢ ψ ⇒ B_{z′, \frac{1}{n}} α and T_{m} ⊢ ψ ⇒ ¬B_{z′, \frac{1}{n}} α so T_{m} ⊢ ψ ⇒⊥ Then, in the same way as above, we have ψ ⇒⊥∈ T^{∗}. Finally, the case φ_{i} = (ψ ⇒ B_{z,ρ} α) follows similarly. □

Let T^{∗} be a maximal consistent set obtained from a consistent set T by the construction from Theorem 2.2. According to the step (3), T^{∗} has the following property: For every formula α ∈ For_{Cl} and every n ∈ N there is at least one z ∈ CQ such that B_{z, \frac{1}{n}} α ∈ T^{∗}. Since T^{∗} is deductively closed, using axiom A5, we can obtain countably many numbers z ∈ CQ such that B_{z, \frac{1}{n}} α ∈ T^{∗}. Now, for each formula α ∈ For_{Cl} we make a sequence z_{n} in the following way:

• For every n ∈ N we arbitrarily chose any number z such that B_{z, \frac{1}{n}} α ∈ T^{∗} and

this z will be the n-th number of the sequence, i.e., z_{n} = z. In this way we obtain the sequence z(α)=z_{0}, z_{1}, z_{2} … where B_{z_{n} , \frac{1}{n}} α ∈ T^{∗}.

Notice that it is possible that z_{m} = z_{k}, for some m ≠ k.

Lemma 2.1. Let z(α) be defined as above. Then, z(α) is a Cauchy sequence (with respect to the norm ∥ · ∥).

Proof. Let ε be arbitrary. Choose n_{0} such that \frac{2}{n_{0}} ⩽ ε. If n, m ⩾ n_{0}, then according to the definition of z(α), B_{z_{n} , \frac{1}{n}} α, B_{z_{m} , \frac{1}{m}} α ∈ T^{∗}. We claim that ∥z_{n} − z_{m}∥ ⩽ \frac{1}{n} + \frac{1}{m}. To prove this, suppose that ∥z_{n} − z_{m}∥ > \frac{1}{n} + \frac{1}{m}. Then:

T^{∗} ⊢ B_{z_{n} , \frac{1}{n}} α

T^{∗} ⊢ B_{z_{m} , \frac{1}{m}} α
T^{∗} ⊢ B_{z_{n} , \frac{1}{n}} α ⇒ ¬B_{z_{m} , \frac{1}{m}} α by axiom A4
T^{∗} ⊢ ¬B_{z_{m} , \frac{1}{m}} α by rule R1, which contradicts the consistency of T^{∗}.

Thus, ∥z_{n} − z_{m}∥ ⩽ \frac{1}{n} + \frac{1}{m} ⩽ \frac{2}{n_{0}} ⩽ ε. □

In the following lemma we will show that this limes does not depend on the choice of z_{k}’s.

Lemma 2.2. Let α ∈ T^{∗}, α ∈ For_{Cl}. Suppose that (z_{n})_{n∈N} , and (z′_{n})_{n∈N} are two different sequences obtained by the above given construction (i.e., for at least one m, z_{m} ≠ z′_{m}). Then lim_{n→∞} z_{n} = lim_{n→∞} z′_{n}.

Proof. According to axiom A4, as in the previous lemma we conclude that for every n, ∥z_{n} −z′_{n}∥ ⩽ \frac{2}{n}. Suppose that lim_{n→∞} z_{n} = a. Let ε be arbitrary. Then there is n′_{0} such that for n ⩾ n′_{0} ∥z_{n} − a∥ ⩽ \frac{ε}{2}. Choose n′′_{0}such that n′′_{0}> \frac{4}{ε} and let n_{0} ⩾ max{n′_{0}, n′′_{0}}. Then for n ⩾ n_{0}:

∥z′_{n} − a∥ = ∥(z′_{n} − z_{n}) + (z_{n} − a)∥ ⩽ ∥z′_{n} − z_{n}∥ + ∥z_{n} − a∥ ⩽ \frac{2}{n} + \frac{ε}{2} ⩽ \frac{ε}{2} + \frac{ε}{2} = ε.

Therefore lim_{n→∞} z′_{n} = a. □

Next we define a canonical model. Let M_{T^{∗}} = ⟨W, H, μ, v⟩, where:

• W = \{w | w ⊧ \overline{T}\} contains all classical propositional interpretations that satisfy the set \overline{T} of all classical consequences of the set T,

• H = {[α] : α ∈ For_{Cl}}

• μ : H → C: Let z(α) = (z_{n})_{n∈N} . Then

μ([α]) = \{ \begin{matrix}z & if B_{z,0} α ∈ T^{∗} \\ lim_{n→∞} z_{n} & otherwise \end{matrix}

• for every world w and every propositional letter p ∈ Var, v(w, p) = true iff w ⊧ p. The axioms guarantee that everything is well defined. For example, by the

classical reasoning we can show that {[α] : α ∈ For_{Cl}} is an algebra of subsets of W. The rule R6 implies that if [α] = [β], then μ([α]) = μ([β]). From the axioms A2, A3 and rule R4 it follows that μ is finitely additive probability measure.

Theorem 2.3 (Strong completeness). A set of formulas T is consistent iff it has an LCOMP_{B}-model.

Proof. (⇐) This direction follows from the soundness of the above axiomatic system.

(⇒) In order to prove this direction we construct M_{T^{∗}} = (W, H, μ, v) as above, and show, by induction on complexity of formulas, that for every formula A, M_{T^{∗}} ⊧ A iff A ∈ T^{∗}. For instance, we will consider the case where A = B_{z,ρ} α for some z ∈ CQ, ρ ∈ Q and α ∈ For_{Cl}.

Suppose that B_{z,ρ} α ∈ T^{∗}. First we assume that ρ > 0. Let z(α) = (z_{n})_{n∈N} and μ([α]) = lim_{n→∞}^{p} z_{n}. Thus (∀ε)(∃n_{0})(∀n)(n ⩾ n_{0} → ∥μ([α]) − z_{n}∥ ⩽ ε).

We distinguish the following cases:

• There is ρ_{1} < ρ such that B_{z,ρ_{1}} α ∈ T^{∗}. Then ρ − ρ_{1} > 0 > \frac{1}{m}, for some m ∈ N. Let ε = ρ − ρ_{1} − \frac{1}{m} > 0. Let n_{0} be such that for every n ⩾ n_{0}, ∥μ([α]) − z_{n}∥ ⩽ ρ − ρ_{1} − \frac{1}{m}. If n ⩾ max\{n_{0}, m\}, then from T^{∗} ⊢ B_{z,ρ_{1}} and T^{∗} ⊢ B_{z_{n} , \frac{1}{n} α} , using axiom A4 we obtain ∥z−z_{n}∥ ⩽ ρ_{1}+ \frac{1}{n}. Thus ∥z−μ([α])∥ = ∥z − z_{n} + z_{n} − μ([α])∥ ⩽ ∥z − z_{n}∥ + ∥z_{n} − μ([α])∥ ⩽ ρ_{1} + \frac{1}{n} + ρ − ρ_{1} − \frac{1}{m} ⩽ ρ. Therefore M_{T^{∗}} ⊧ B_{z,ρ} α.

• There is no ρ_{1} < ρ such that B_{z,ρ_{1}} α ∈ T^{∗}. But from T^{∗} ⊢ B_{z,ρ} α and axiom A2, we obtain T^{∗} ⊢ B_{z,ρ+ \frac{1}{n}} α, for every n ∈ N. Therefore, according to the previous considerations, we obtain ∥z − μ([α])∥ ⩽ ρ + \frac{1}{n}, for every n ∈ N, and thus ∥z − μ([α])∥ ⩽ ρ.

Finally, let ρ = 0, i.e., T^{∗} ⊢ B_{z,0} α. Then, according to the definition of measure μ in the canonical model, μ([α]) = z, i.e., ∥μ([α]) − z∥ = 0. Thus, M_{T^{∗}} ⊧ B_{z,0} α.

For the other direction, suppose that M_{T^{∗}} ⊧ B_{z,ρ} α. Let ρ > 0. As in the previous direction, we consider the following cases.

• ∥μ([α]) − z∥ < ρ, that is, there is ρ_{1} < ρ such that M_{T^{∗}} ⊧ B_{z,ρ_{1}} α. Choose k ∈ N such that ρ − ρ_{1} > \frac{1}{k}. Let μ([α]) = lim_{n→∞}^{p} z_{n}. Then, there is n_{0} such that (∀n)(n ⩾ n_{0} → ∥μ([α]) − z_{n}∥ ⩽ \frac{1}{k}). Let n ⩾ n_{0} and \frac{1}{n} + \frac{1}{k} + ρ_{1} ⩽ ρ. Then from ∥z_{n} − μ([α])∥ ⩽ \frac{1}{k} and ∥z − μ([α])∥ ⩽ ρ_{1}, we obtain ∥z − z_{n}∥ ⩽ ρ_{1} + \frac{1}{k}. Therefore, T^{∗} ⊢ B_{z_{n} , \frac{1}{n}} α

T^{∗} ⊢ B_{z_{n} , \frac{1}{n}} α ⇒ B_{z, \frac{1}{n} +ρ_{1} + \frac{1}{k}} α, by A5 T^{∗} ⊢ B_{z, \frac{1}{n} +ρ_{1} + \frac{1}{k}} α T^{∗} ⊢ B_{z,ρ} α, using A2

• There is no ρ_{1} < ρ such that ∥μ([α]) − z∥ < ρ_{1}. Since ∥μ([α]) − z∥ < ρ, we have ∥μ([α]) − z∥ < ρ + \frac{1}{n}, for every n ∈ N. Therefore, using the previous considerations we obtain T^{∗} ⊢ B_{z,ρ+ \frac{1}{n}} α for every n ∈ N, and according to rule R5, T^{∗} ⊢ B_{z,ρ} α. If ρ = 0, then ∥μ([α]) − z∥ = 0, so ∥μ([α]) − z∥ < \frac{1}{n} for every n ∈ N. Thus

T^{∗} ⊢ B_{z,0+ \frac{1}{n}} α for every n ∈ N, and by rule R5, Thus T^{∗} ⊢ B_{z,0} α. □

2.4. Decidability. In this section, we analyze decidability of the satisfiability problem for LCOMP_{B}-formulas. Since there is a procedure for deciding satisfiability of classical propositional formulas, we will consider only For_{CP}-formulas.

Let φ ∈ For_{CP}. If p_{1}, …, p_{n} are all propositional letters appearing in φ, then an atom of a formula φ is a formula of the form ±p_{1} ∧ … ∧ ±p_{n}, where ±p_{i} is either p_{i} or ¬p_{i}. It can be shown, using classical propositional reasoning, that φ is equivalent to a formula

DNF(φ) = ⋁_{i=1,m} ( ⋀_{j=1,k_{i}} ±B_{z_{i,j} , \frac{1}{n_{i,j}}} α_{i,j} )

where ±B_{z_{i,j} , \frac{1}{n_{i,j}}} α_{i,j} denotes either B_{z_{i,j} , \frac{1}{n_{i,j}}} α_{i,j} or ¬B_{z_{i,j} , \frac{1}{n_{i,j}}} α_{i,j}

φ is satisfiable iff at least one disjunct from DNF(φ) is satisfiable.

Fix some i and consider disjunct D_{i} = ⋀ _{j=1,k_{i}} ±B_{z_{i,j} , \frac{1}{n_{i,j}}} α_{i,j} from DNF(φ). Let p_{1}, …, p_{n} be all propositional letters appearing in D_{i}. Every propositional formula α is equivalent to the complete disjunctive normal form, denoted FDNF(α).

If ⊧ (α ⇔ β), then according to the rule R6, for every model M and every z ∈ CQ, ρ ∈ Q^{+} , M ⊧ B_{z,ρ} α iff M ⊧ B_{z,ρ} β. Thus, disjunct D_{i} is satisfiable iff the formula ⋀ _{j=1,k_{i}} ±B_{z_{i,j} , \frac{1}{n_{i,j}}} FDNF(α_{i,j} ) is satisfiable. Since for two different atoms

a_{i} and a_{j}, [a_{i}] ∩ [a_{j}] = ∅, for every model M, μ[a_{i} ∨ a_{j}] = μ[a_{i}] + μ[a_{j}]. Hence, disjunct D_{i} is satisfiable iff the following system is satisfiable

∑_{t=1}^{2^{n}} z_{t} = 1

J_{1} = \{ \begin{matrix}( ∑_{a_{t}∈α_{i,1}} x_{t} − a_{1})^{2} + ( ∑_{a_{t}∈α_{i,1}} y_{t} − b_{1})^{2} ⩽ ρ_{1}^{2} & if ± B_{z_{1} ,ρ_{1}} α_{i,1} = B_{z_{1} ,ρ_{1}} α_{i,1} \\ ( ∑_{a_{t}∈α_{i,1}} x_{t} − a_{1})^{2} + ( ∑_{a_{t}∈α_{i,1}} y_{t} − b_{1})^{2} > ρ_{1}^{2} & if ± B_{z_{1} ,ρ_{1}} α_{i,1} = ¬B_{z_{1} ,ρ_{1}} α_{i,1} \end{matrix}

⋮

J_{k_{i}} = \{ \begin{matrix}( ∑_{a_{t}∈α_{i,k_{i}}} x_{t}−a_{k_{i}} )^{2}+( ∑_{a_{t}∈α_{i,k_{i}}} y_{t}−b_{k_{i}} )^{2}⩽ρ_{k_{i}}^{2} & if ±B_{z_{k_{i}} ,ρ_{k_{i}}} α_{i,k_{i}} = B_{z_{k_{i}} ,ρ_{k_{i}}} α_{i,k_{i}} \\ ( ∑_{a_{t}∈α_{i,k_{i}}} x_{t}−a_{k_{i}} )^{2}+( ∑_{a_{t}∈α_{i,k_{i}}} y_{t}−b_{k_{i}} )^{2}>ρ_{k_{i}}^{2} & if ±B_{z_{k_{i}} ,ρ_{k_{i}}} α_{i,k_{i}} = ¬B_{z_{k_{i}} ,ρ_{k_{i}}} α_{i,k_{i}} \end{matrix}

where a_{t} ∈ α_{i,j} denote that the atom a_{t} appears in FDNF(α_{i,j} ), z_{t} = μ([a_{t}]) = x_{t} + iy_{t} and z_{j} = a_{j} + ib_{j}, 1 ⩽ j ⩽ k_{i}.

As we can see, our formulas can be coded in the existential fragment of the RCF. It is well known that the SAT problem for this fragment is PSPACE complete [1], so PSAT for LCOMP_{B} is in PSPACE.

Therefore, we have the following result.

Theorem 2.4. The satisfiability problem for LCOMP_{B}-formulas is decidable.

3. The logic LCOMP_{S}

In this section we present the probability logic LCOMP_{S} in which we use probabilistic operators S_{z,ρ} α meaning “The probability of α belongs to the square parallel to the x axis, with the center z and the side 2ρ". Let [a, b] = {x ∈ R | a ⩽ x ⩽ b} denote interval on real line. The most of the notions defined in Section 2 are also used for the logic LCOMP_{S}. The main, but important differences are:

• In the definition of all probabilistic formulas For_{CP}^{S}, basic probabilistic formulas are of the form S_{z,ρ} α where α ∈ For_{Cl}, z ∈ CQ and ρ ∈ Q^{+} .

• If M = ⟨W, H, μ, v⟩ is an LCOMP_{S} model, then for α, For_{Cl}, z ∈ CQ, ρ ∈ Q^{+} and z = a + ib, M ⊧ S_{z,ρ} α iff Re(μ([α])) ∈ [a − ρ, a + ρ] and Im(μ([α])) ∈ [b − ρ, b + ρ].

Note that, for arbitrary ρ ∈ Q^{+} , z ∈ CQ, M ⊧ S_{z,ρ} α means that μ([α]), belongs to the complex square parallel to the x axis, with the center z and the side 2ρ. If ρ = 0, then we obtain that the probability is equal to z.

The axiom system AX_{LCOMP _{S}} of the logic LCOMP_{S} contains the following axioms and inference rules: Axioms

A1. Substitutional instances of tautologies; A2. S_{z,ρ} α ⇒ S_{z,ρ′} α, whenever ρ′ ⩾ ρ; A3. S_{z_{1} ,ρ_{1}} α ∧ S_{z_{2} ,ρ_{2}} β ∧ S_{0,0}(α ∧ β) ⇒ S_{z_{1} +z_{2} ,ρ_{1} +ρ_{2}} (α ∨ β); A4. S_{z_{1} ,ρ_{1}} α ⇒ ¬S_{z_{2} ,ρ_{2}} α, if [a_{1} − ρ_{1}, a_{1} + ρ_{1}] ∩ [a_{2} − ρ_{2}, a_{2} + ρ_{2}] = ∅ or [b_{1} − ρ_{1}, b_{1} +

ρ_{1}] ∩ [b_{2} − ρ_{2}, b_{2} + ρ_{2}] = ∅, where z_{1} = a_{1} + ib_{1} and z_{2} = a_{2} + ib_{2}; A5. S_{z_{1} ,ρ_{1}} α ⇒ S_{z_{2} ,ρ_{2}} α, if [a_{1}−ρ_{1}, a_{1}+ρ_{1}] ⊆ [a_{2}−ρ_{2}, a_{2}+ρ_{2}] and [b_{1}−ρ_{1}, b_{1}+ρ_{1}] ⊆

[b_{2} − ρ_{2}, b_{2} + ρ_{2}]

Inference rules

R1. From A and A ⇒ B infer B. Here A and B are either both propositional, or

both probabilistic formulas; R2. From α infer S_{1,0}α; R3. If n ∈ N, from φ ⇒ ¬S_{z, \frac{1}{n}} α for every z ∈ CQ, infer φ ⇒⊥; R4. From α ⇒⊥, infer S_{0,0}α; R5. If z ∈ CQ, from φ ⇒ S_{z,ρ+ \frac{1}{n}} α for every n ∈ N, infer φ ⇒ S_{z,ρ} α; R6. From (α ⇔ β), infer (S_{z,ρ} α ⇒ S_{z,ρ} β);

Axiom A2 corresponds to the obvious property of squares: a square with smaller side is contained in a square with larger side and the same center. Axiom A3 corresponds to the additivity of measures. Axiom A4 provides that the measure of formula cannot belong to two disjoint squares. Axiom A5 allows that the following holds: if the measure of the formula α belongs to the square S, it belongs to a larger square S′, such that S ⊆ S′. Rule R3 provides that for every classical formula α and every n ∈ N, there must be some z ∈ CQ such that the measure of α belongs to the square S[z, \frac{1}{n}]. Rule R5 expresses the following property: if the measure of α is arbitrary close to some number z ∈ CQ, then the measure of α is equal to z.

Construction of maximal consistent extensions of consistent sets of formulas can be done similarly as above. If T^{∗} is maximal consistent set of formulas, then for each formula α ∈ For_{Cl} we make a sequence z(α) = z_{0}, z_{1},…, where S_{z_{j} , \frac{1}{j}} α ∈ T^{∗}.

Lemma 3.1. For every α ∈ For_{Cl}, z(α) is a Cauchy sequence (with respect to the norm ∥ · ∥).

Proof. Let ε be arbitrary. Choose n_{0} such that \frac{4}{n_{0}} ⩽ ε. If n, m ⩾ n_{0}, then S_{z_{n} , \frac{1}{n}} α, S_{z_{m} , \frac{1}{m}} α ∈ T^{∗}. Let z_{n/m} = x_{n/m} + iy_{n/m} . Then, there exist x and y such that x ∈ [x_{n} − \frac{1}{n} , x_{n} + \frac{1}{n}] ∩ [x_{m} − \frac{1}{m} , x_{m} + \frac{1}{m}] and y ∈ [y_{n} − \frac{1}{n} , y_{n} + \frac{1}{n}] ∩ [y_{m} − \frac{1}{m} , y_{m} + \frac{1}{m}]. To prove that, suppose that [x_{n} − \frac{1}{n} , x_{n} + \frac{1}{n}] ∩ [x_{m} − \frac{1}{m} , x_{m} + \frac{1}{m}] = ∅ or [y_{n} − \frac{1}{n} , y_{n} + \frac{1}{n}] ∩ [y_{m} − \frac{1}{m} , y_{m} + \frac{1}{m}] = ∅. Then:

T^{∗} ⊢ S_{z_{n} , \frac{1}{n}} α T^{∗} ⊢ S_{z_{m} , \frac{1}{m}} α T^{∗} ⊢ S_{z_{n} , \frac{1}{n}} α ⇒ ¬S_{z_{m} , \frac{1}{m}} α by Axiom A4 T^{∗} ⊢ ¬S_{z_{m} , \frac{1}{m}} α by rule R1, which contradicts the consistency of T^{∗}. Thus, we have

x_{n} ∈ [x − \frac{1}{n} , x + \frac{1}{n}], x_{m} ∈ [x − \frac{1}{m} , x + \frac{1}{m}],
y_{n} ∈ [y − \frac{1}{n} , y + \frac{1}{n}], y_{m} ∈ [y − \frac{1}{m} , y + \frac{1}{m}].

Therefore |x_{n} − x_{m}| ⩽ \frac{1}{n} + \frac{1}{m} and |y_{n} − y_{m}| ⩽ \frac{1}{n} + \frac{1}{m} and hence

∥z_{n} − z_{m}∥ = \sqrt{(x_{n} − x_{m})^{2} + (y_{n} − y_{m})^{2}} ⩽ 2(\frac{1}{n} + \frac{1}{m}) ⩽ \frac{4}{n_{0}} ⩽ ε.  □

Lemma 3.2. Let α ∈ T^{∗}, α ∈ For_{Cl}. Suppose that (z_{n})_{n∈N} , and (z′_{n})_{n∈N} are two different sequences obtained by the above given construction (i.e., for at least one m, z_{m} ≠ z′_{m}). Then lim_{n→∞} z_{n} = lim_{n→∞} z′_{n}.

Proof. Suppose that lim_{n→∞} z_{n} = a. Let ε be arbitrary. Then there is n′_{0} such that for n ⩾ n′_{0} ∥z_{n} − a∥ ⩽ \frac{ε}{2}. Choose n′′_{0} such that n′′_{0} > \frac{8}{ε} and let n_{0} ⩾ max{n′_{0}, n′′_{0}}. Then for n ⩾ n_{0} as in the previous Lemma we conclude that ∥z_{n} − z′_{n}∥ ⩽ \frac{4}{n_{0}} ⩽ \frac{ε}{2}. Thus

∥z′_{n} − a∥ = ∥(z′_{n} − z_{n}) + (z_{n} − a)∥ ⩽ ∥z′_{n} − z_{n}∥ + ∥z_{n} − a∥ ⩽ \frac{ε}{2} + \frac{ε}{2} = ε.

Therefore lim_{n→∞} z′_{n} = a. □

Theorem 3.1 (Strong completeness). A set of formulas T is consistent iff it has an LCOMP_{S}-model.

Proof. We analyze formulas of the form A = S_{z,ρ} α for some z ∈ CQ, ρ ∈ Q and α ∈ For_{Cl}.

Suppose that S_{z,ρ} α ∈ T^{∗} where z = x + iy. Let z(α) = (z_{n})_{n∈N} and μ([α]) = lim_{n→∞}^{p} r_{n} = a + ib.

First assume that ρ > 0. We distinguish the following cases:

• There is ρ_{1} < ρ such that S_{z,ρ_{1}} α ∈ T^{∗}. Then ρ − ρ_{1} > 0 > \frac{1}{m}, for some m ∈ N. Let ε = ρ − ρ_{1} − \frac{1}{m} > 0. Then, there is n_{0} such that for every n ⩾ n_{0}, ∥μ([α]) − z_{n}∥ ⩽ ρ − ρ_{1} − \frac{1}{m}. Let n ⩾ max\{n_{0}, m\} and z_{n} = x_{n} + iy_{n}. Then from \sqrt{(x_{n} − a)^{2} + (y_{n} − b)^{2}} ⩽ ε we obtain |x_{n} − a|, |y_{n} − b| ⩽ ε. Since T^{∗} ⊢ S_{z,ρ_{1}} α and T^{∗} ⊢ S_{z_{n} , \frac{1}{n} α} , using axiom A4, we conclude that there is T ∈ [x − ρ_{1}, x + ρ_{1}] ∩ [x_{n} − \frac{1}{n} , x_{n} − \frac{1}{n}]. Thus x − ρ_{1} ⩽ T ⩽ x + ρ_{1}, x_{n} − \frac{1}{n} ⩽ T ⩽ x_{n} − \frac{1}{n} and therefore |x − x_{n}| ⩽ ρ_{1} + \frac{1}{n}. In the same way, we obtain that |y − y_{n}| ⩽ ρ_{1} + \frac{1}{n}. Then |a − x| = |(a − x_{n}) + (x_{n} − x)| ⩽ |a − x_{n}| + |x_{n} − x| ⩽ ε + ρ_{1} + \frac{1}{n} = ρ − ρ_{1} − \frac{1}{m} + ρ_{1} + \frac{1}{n} ⩽ ρ. Thus, a ∈ [x − ρ, x + ρ]. Similarly, b ∈ [y − ρ, y + ρ]. Hence, M_{T^{∗}} ⊧ S_{z,ρ} α.

• There is no ρ_{1} < ρ such that S_{z,ρ_{1}} α ∈ T^{∗}. But from T^{∗} ⊢ S_{z,ρ} α and axiom A2, we obtain T^{∗} ⊢ S_{z,ρ+ \frac{1}{n}} α, for every n ∈ N. Therefore, we obtain M_{T^{∗}} ⊧ S_{z,ρ+ \frac{1}{n}} α for every n ∈ N. Thus a ∈ [x − ρ + \frac{1}{n} , x + ρ + \frac{1}{n}] and b ∈ [y − ρ + \frac{1}{n} , y + ρ + \frac{1}{n}] for every n ∈ N, and hence a ∈ [x − ρ, x + ρ], b ∈ [y − ρ, y + ρ], that is M_{T^{∗}} ⊧ S_{z,ρ} α.

Finally, let ρ = 0, i.e., T^{∗} ⊢ S_{z,0} α. Then, according to the definition of measure μ in the canonical model, μ([α]) = z, i.e., a ∈ [z − 0, z + 0], b ∈ [z − 0, z + 0]. Thus, M_{T^{∗}} ⊧ S_{z,0} α.

For the other direction, suppose that M_{T^{∗}} ⊧ S_{z,ρ} α, z = x + iy and μ([α]) = a + ib. Let ρ > 0. As in the previous direction, we consider the following cases.

• There is ρ_{1} < ρ such that M_{T^{∗}} ⊧ S_{z,ρ_{1}} α. Choose m ∈ N such that ρ − ρ_{1} > \frac{1}{m} . Let μ([α]) = lim_{n→∞} z_{n}, where z_{n} = x_{n} + iy_{n}. Then, there is n_{0} such that (∀n)(n ⩾ n_{0} → ∥μ([α])−z_{n}∥ ⩽ ρ−ρ_{1} − \frac{1}{m}, and therefore |x_{n} −a| ⩽ ρ−ρ_{1} − \frac{1}{m}, |y_{n}−b| ⩽ ρ−ρ_{1}− \frac{1}{m}. Since M_{T^{∗}} ⊧ S_{z,ρ_{1}} α it follows that |x−a| ⩽ ρ_{1}, |y−b| ⩽ ρ_{1}. Thus |x − x_{n}| = |(x − a) + (a − x_{n})| ⩽ |x − a| + |x_{n} − a| ⩽ ρ − ρ_{1} − \frac{1}{m} + ρ_{1} = ρ − \frac{1}{m} ⩽ ρ − \frac{1}{n}. In the same way we obtain |y − y_{n}| ⩽ ρ − \frac{1}{n} Therefore [x_{n} − \frac{1}{n} , x_{n} + \frac{1}{n}] ⊆ [x − ρ, x + ρ], [y_{n} − \frac{1}{n} , y_{n} + \frac{1}{n}] ⊆ [y − ρ, y + ρ] and hence form T^{∗} ⊢ S_{z_{n} , \frac{1}{n}} α, using axiom A5 we obtain

T^{∗} ⊢ S_{z_{n} , \frac{1}{n}} α ⇒ S_{z,ρ} α, by A5 and by rule R1, T^{∗} ⊢ S_{z,ρ} α.

• There is no ρ_{1} < ρ such that M_{T^{∗}} ⊧ S_{z,ρ_{1}} α. Then, from M_{T^{∗}} ⊧ S_{z,ρ} α we obtain M_{T^{∗}} ⊧ S_{z,ρ+ \frac{1}{n}} α for every n ∈ N. Therefore, we obtain T^{∗} ⊢ S_{z,ρ+ \frac{1}{n}} α for every n ∈ N, and according to rule R5, T^{∗} ⊢ S_{z,ρ} α. If ρ = 0, then from M_{T^{∗}} ⊧ S_{z,0} α follows M_{T^{∗}} ⊧ S_{z, \frac{1}{n}} α for every n ∈ N. Thus

T^{∗} ⊢ S_{z, \frac{1}{n}} α for every n ∈ N, and by rule R5, T^{∗} ⊢ S_{z,0} α. □

Theorem 3.2. The satisfiability problem for LCOMP_{S}-formulas is NP-complete.

Proof. Let φ be a probabilistic LCOMP_{S}-formula. Similarly as in Section2.4, we consider one disjunct D from the DNF(φ) and we conclude that φ is satisfiable iff the system of the following form is satisfiable:

∑_{t=1}^{2^{n}} z_{t} = 1

J_{1} = \{ \begin{matrix}a_{1} − ρ_{1} ⩽ ∑_{a_{t}∈α_{1}} x_{t} ⩽ a_{1} + ρ_{1} and \\ b_{1} − ρ_{1} ⩽ ∑_{a_{t}∈α_{1}} y_{t} ⩽ b_{1} + ρ_{1} & if ± S_{z_{1} ,ρ_{1}} α_{1} = S_{z_{1} ,ρ_{1}} α_{1} \\ ∑_{a_{t}∈α_{1}} x_{t} ⩽ a_{1} − ρ_{1} or ∑_{a_{t}∈α_{1}} x_{t} ⩾ a_{1} + ρ_{1} or \\ ∑_{a_{t}∈α_{1}} y_{t} ⩾ b_{1} + ρ_{1} or ∑_{a_{t}∈α_{1}} y_{t} ⩽ b_{1} − ρ_{1} & if ± S_{z_{1} ,ρ_{1}} α_{1} = ¬S_{z_{1} ,ρ_{1}} α_{1} \end{matrix}

⋮

J_{k} = \{ \begin{matrix}a_{k} − ρ_{k} ⩽ ∑_{a_{t}∈α_{k}} x_{t} ⩽ a_{k} + ρ_{k} and \\ b_{k} − ρ_{k} ⩽ ∑_{a_{t}∈α_{k}} y_{t} ⩽ b_{k} + ρ_{k} & if ± S_{z_{k} ,ρ_{k}} α_{k} = S_{z_{k} ,ρ_{k}} α_{k} \\ ∑_{a_{t}∈α_{k}} x_{t} ⩽ a_{k} − ρ_{k} or ∑_{a_{t}∈α_{k}} x_{t} ⩾ a_{k} + ρ_{k} or \\ ∑_{a_{t}∈α_{k}} y_{t} ⩾ b_{k} + ρ_{k} or ∑_{a_{t}∈α_{k}} y_{t} ⩽ b_{k} − ρ_{k} & if ± S_{z_{k} ,ρ_{k}} α_{k} = ¬S_{z_{k} ,ρ_{k}} α_{k} \end{matrix}

where a_{t} ∈ α_{j} denotes that the atom a_{t} appears in FDNF(α_{j}), z_{t} = μ([a_{t}]) = x_{t}+iy_{t} and z_{j} = a_{j} + ib_{j},1 ⩽ j ⩽ k.

Thus, the statement is proved since PSAT for LCOMP_{S}-satisfiability is reduced to the linear systems solving problem, similarly as in [3]. □

4. Conclusion

We have presented two similar logics that formalize reasoning about complex valued probabilities. The following example, however, shows that it is not possible simply to replace operators of the forms B_{z,ρ} and S_{z,ρ} and keep the meaning of formulas. Namely, since [2, 4] ⊂ [1, 17] and [3, 5] ⊂ [2, 18], S_{3+4i,1} α ⇒ S_{9+10i,8} α is LCOMP_{S}-valid, but its counterpart B_{3+4i,1} α ⇒ B_{9+10i,8} α, is not LCOMP_{B}-valid, because it is obvious that \frac{5}{2} + \frac{7}{2}i ∈ B[3 + 4i, 1] but \frac{5}{2} + \frac{7}{2}i ∉ B[9 + 10i, 8]. Similarly, since B[4 + 4i, 2] ∩ B[9 + 6i, 3] = ∅, B_{4+4i,2} α ⇒ ¬B_{9+6i,3} α is LCOMP_{B}-valid, while S_{4+4i,2} α ⇒ ¬S_{9+6i,3} α is not LCOMP_{S}-valid, because the corresponding squares have a common side.

Acknowledgements. The authors are partially supported by Serbian ministry of education and science through grants III044006 and ON174026.

References

1. J. Canny, Some algebraic and geometric computations in PSPACE; in: Proc. XX ACM Symposium on Theory of Computing, 1978, 460–467.

2. D. R. Cox, A use of complex probabilities in the theory of stochastic processes, Math. Proc. Cambridge Phil. Soc. 51 (1955), 313–319.

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

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

5. , Some first order probability logics, Theor. Comput. Sci. 247 (2000), 191–212.

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

7. Z. Ognjanović, M. Rašković, Z. Marković, Probability logics; in: Zoran Ognjanović (ed.) Logic in Computer Science, Zb. Rad. 12(20), Matematički institut SANU, Beograd, 2009, 35–111.

8. Z. Ognjanović, Z. Marković, M. Rašković, D. Doder, A. Perović, A probabilistic temporal logic that can model reasoning about evidence, Ann. Math. Artif. Intell. 65 (2012),

9. W. Rudin, Real and Complex Analysis, McGraw-Hill, 1970.

10. A. Ilić Stepić, Z. Ognjanović, N. Ikodinović, A. Perović, A p-adic probability logic, Math. Log. Q. 58 (2012), 263–280.

11. D. Weingarten, Complex probabilities on R^{N} as real probabilities on C^{N} and an application to path integrals, Phys. Rev. Lett. 89 (2002).

12. S. Youssef, Quantum mehanics as comlex probability theory, Mod. Phys. Lett. A 9 (1994), 2571–2586.

13. A. A. Jaoude, The theory of complex probability and the first order reliability method, J. Math. Stat. 9 (2013), 329–343.

14. B. Bidabad, B. Bidabad, Complex probability and Markov stochastic processes, in: Proc. First Iranian Statistics Conference, Isfahan University of Technology, 1992.

Mathematical Institute (Received 08 02 2013) of Serbian Academy of Sciences and Arts (Revised 11 11 2013) Kneza Mihaila 36 Belgrade Serbia

angelina@mi.sanu.ac.rs
zorano@mi.sanu.ac.rs