SMV-algebras and Probabilistic Kripke Models
by
Tommaso Flaminio
Dipartimento di Matematica e Informatica, Università degli Studi di Siena. Italy
Coauthors: Franco Montagna

States on MV-algebras have been introduced by Mundici in [Mu] as averaging processes for formulas in \Lukasiewicz logic.

In order to treat states in a logical framework, Flaminio and Godo introduce in [FG07] the logics FP(\L_n, \L) and FP(\L, \L). The latter is obtained by adding a unary modality Pr to the language of \Lukasiewicz logic (cf [H98]) and modal axioms suggested by the following semantic interpretation: the probability of an event A is interpreted as the truth value of the modal formula Pr(A).

Well-founded formulas of FP(\L, \L) are constituted of all the formulas of \Lukasiewicz logic (those are the non-modal formulas), and the class of modal formulas so defined: for each non-modal formula A, Pr(A) is a modal formula, the truth constant [`0] is modal, finally these formulas are combined by means of the \Lukasiewicz connectives. This means that, for instance, neither Pr(A→Pr(B)) nor B⊕Pr(A) (A and B being Pr-free) are well-founded formulas. Using those modal fuzzy logics one can treat probability over many-valued events.

A probabilistic Kripke model for the logic FP(\L, \L) is a pair K=(W, m) where W is a set of valuations of \Lukasiewicz formulas in [0, 1] and m:W→[0, 1] satisfies the condition: ∑_{w ∈ W}m(w)=1. Elements of W are also called nodes or possible worlds.

Given a Kripke model K=(W, m) and a formula A of FP(\L, \L), the truth value ∥A∥_{K, w} of A in K at the node w is inductively defined as follows:

• If A does not contain any occurrence of the modality Pr, then ∥A∥_{K, w}=w(A),

• If A is in the form Pr(B), then ∥A∥_{K, w}=∑_{w ∈ W}w(y)·m(w).

• \Lukasiewicz connectives are treated truth-functionally as usual.

As they are, the FP(\L_n, \L) and FP(\L, \L) logics are not algebraizable in the sense of Blok-Pigozzi. Recall in fact that Pr(A) is a well-founded formula only if A is a non-modal formula (and hence A does not contain any occurrence of Pr), and a formula of the form B⊕C is well-founded whenever B is modal iff C is modal. Therefore the algebraic counterpart of the operator Pr is a partial operation but not an operation.

As to provide an algebraic approach to states, in [FM07] we introduced the variety of SMV-algebras. An SMV-algebra is a system A=(A, ⊕, ¬, s, 0, 1), where the reduct (A, ⊕, ¬, 0, 1) is an MV-algebra, and s:A→ A satisfies the following equations for each x, y ∈ A:

• s(0)=0

• s(¬x)=¬s(x)

• s(s(x)⊕s(y))=s(x)⊕s(y)

• s(x⊕y)=s(x)⊕s(y\ominus (x\odot y))

In [FM07, FM08] we show how, starting from an SMV-algebra A one can define a state s (in the sense of Mundici) on the MV-reduct of A. Furthermore, we use SMV-algebras to equationally characterize the coherence of a finite and rational-valued assessment over \Lukasiewicz events:

Theorem 1 Let a: P(A_i)=n_i/m_i be a rational assessment over the \Lukasiewicz formulas A₁, ..., A_t. Then the following are equivalent:

(a) a is coherent.
(b) The equations e_i: (m_i-1)y_i=¬y_i, and d_i: s(A_i)=n_iy_i (for i=1, ..., t, and the y_i's being fresh variables) are satisfied in some non-trivial SMV-algebra.

Let now FP⁺(\L, \L) be the logic obtained by extending FP(\L, \L) by the following:

(a) the language is extended by the rules: (1) Pr(A) is a formula whenever A is a formula (without the restriction that A does not contain occurrence of Pr), and (2) if B and C are formulas (no matter if B and C are modal or not), then B⊕C is a formula (hence we also remove the restriction that B is modal iff so is C).
(b) the axioms of FP(L, L) (cf [FG07]) are extended to the formulas of the new language.
(c) the axiom schema Pr(A)↔ A is added, whenever A ranges over all formulas all of whose variables only occur under the scope of Pr (this axiom reflects the fact that such formulas represent real numbers which coincide with their probability).

An FP⁺(\L, \L)-formula A is said 1-satisfiable if there exists a probabilistic Kripke model K such that ∥A∥_K=1. Our main result now reads as follows:

Theorem 2 Let A be a term in the language of SMV-algebras. Then the following are equivalent:

(i) There is a Kripke-model K=(W, m) such that ∥A∥_K=1.
(ii) A is 1-satisfiable in an SMV-algebra (A, s).

Using this result we also show that the problem of deciding whether an equation A=1 holds in an SMV-algebra is PSPACE. The latter result, together with Theorem 1, provides a (new proof (cf [H07]) for the) PSPACE-containment for the problem of establishing the coherence of a rational assessment over \Lukasiewicz formulas.

PDF

Date received: February 21, 2008