The Algebra of Worlds

www.bucephalus.org

September 6, 2002

Contents

1 Introduction 1

2 Worlds and their representation 2 2.1 Worlds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Special properties of worlds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Atom lists of worlds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.4 Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.5 Double tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

3 Operations on worlds and atoms lists 4 3.1 Atomic worlds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 The zero and unit world . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.3 Expansion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.4 Boolean junctions of worlds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.5 Infimum and supremum reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.6 Remark about the chosen notations . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 Relations between worlds 8

5 More operations 9 5.1 Negative and positive atoms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 5.2 Standard reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

1 Introduction

We are going to define the concept of a world algebra on a given set A. One such world is a function (A ⟶ B) ⟶ B, where A ⊆ A and B is the set of the two boolean or bit values. Such a world algebra is a standard model of a theory algebra. Another example of such a theory algebra is the set of (boolean or theory) formulas on A, equipped with the according operations and relations. There is a kind of isomorphism between the world and the formula algebra: each formula represents a unique world and every (finite) world can be represented by a formula. Worlds are — as the term suggests — very “meaningful” and intuitive. Formulas on the other hand have the advantage that they can display certain properties of the according world and that they are much more suitable as data structures for computer programs which implement theory algebras. So, there is a productive interplay between formulas and worlds.

2 Worlds and their representation

2.1 Worlds

A denotes a pre–defined set of atoms. In our case A is made of all non–empty strings of letters, digits and the understroke.

There is a strict linear order relation < defined on A.

Because A is linearly ordered by <, every finite atom set A of n atoms has a unique representation as an ordered atom list [ α_{1} α_{2} … α_{n}], with α_{1} < α_{2} < ⋯ < α_{n}. There is a unique bijection between the finite subsets of A and the set of all ordered atom lists on A. So the standard set relations ∈, ⊆ and operations ∩, ∪, \ on sets are well–defined on ordered atom lists as well, where the role of the empty set ∅ is taken by the empty list [ ].

B := {?,!} denotes the set of bitvalues. It has exactly two elements:

• ? the zero bit (also called false and written as 0 or f or ⊥)

• ! the unit bit (also called true and written as 1 or t or ⊤)

B is linearly ordered by defining for all β, β′ ∈ B

β < β′ :iff β = ? and β′ = !

If A is a finite set or ordered list of atoms, a (binary) valuation of A is a function ω : A ⟶ B. If A is the ordered list [ α_{1} … α_{n}], then ω is also written as

[ α_{1}/ω(α_{1}) … α_{n}/ω(α_{n}) ]

For example ω = [ a/? b/! c/! ] is a valuation of A = [ a b c].

We assume that there is a strict linear order < defined on the set of all the valuations of A. For example, for A = [ a b] we put

[ a/? b/? ] < [ a/! b/? ] < [ a/? b/! ] < [ a/! b/! ]

V al(A) denotes the set or ordered list of all the valuations of A.

For example, for A = [ a b]

V al(A) = [ [ a/? b/? ] [ a/! b/? ] [ a/? b/! ] [ a/! b/! ] ]

If A contains n different atoms, then V al(A) has 2^{n} different valuations of A.

Note that V al([ ]) = [ [ ] ], i.e. the empty list [ ] of atoms has exactly one valuation, also written [ ], which is the empty valuation.

A (finite binary) world τ (on A) is defined by

• A finite set or ordered list A of atoms.

• A function V al(A) ⟶ B.

In other words, τ is a function τ : (A ⟶ B) ⟶ B

A valuation ω in a world τ is also said to be a

• possible state in τ, if τ(ω) = !

• impossible state in τ, if τ(ω) = ?

2.2 Special properties of worlds

A world τ on A is said to be

• valid or a tautology if every valuation is a possible state, i.e. if τ(ω) = ! for all ω ∈ V al(A)

• satisfiable if at least one valuation is a possible state,

• contradictory or a contradiction if every valuation is an impossible state.

2.3 Atom lists of worlds

If τ is a world on an ordered atoms list A, then

@τ := A

is the (ordered) atom list of τ.

2.4 Tables

If τ is a world on A, the table of τ is uniquely defined by

\begin{matrix}A \\ ω_{0} & τ(ω_{0}) \\ ω_{1} & τ(ω_{1}) \\ ⋮ & ⋮ \\ ω_{2^{n}−1} & τ(ω_{2^{n}−1}) \end{matrix}  or  \begin{matrix}α_{1} & … & α_{n} \\ ω_{0}(α_{1}) & … & ω_{0}(α_{n}) & τ(ω_{0}) \\ ω_{1}(α_{1}) & … & ω_{1}(α_{n}) & τ(ω_{1}) \\ ⋮ & & ⋮ & ⋮ \\ ω_{2^{n}−1}(α_{1}) & … & ω_{2^{n}−1}(α_{n}) & τ(ω_{2^{n}−1}) \end{matrix}

where [ α_{1} … α_{n}] := A and [ ω_{0} ω_{1} … ω_{2^{n}−1} ] := V al(A).

For example, let A := [ hot rain snow] be an orderd list of three atoms. A world τ on A is represented by the table

hot rain snow
?  ?  ?  !
!  ?  ?  !
?  !  ?  ?
!  !  ?  !
?  ?  !  !
!  ?  !  ?
?  !  !  ?
!  !  !  ?

A possible state in w is given by, say [ hot/! rain/? snow/? ]. In other word, the state “it is hot, not raining, and not snowing” is a possible state in w, while for example “it is hot, it does not rain, and it snows” is an impossible state in w.

2.5 Double tables

Let ω_{1} : A_{1} ⟶ B and ω_{2} : A_{2} ⟶ B be two valuations on disjunct atom sets, i.e. A_{1} ∩ A_{2} is empty. Then

ω_{1} · ω_{2} : A_{1} ∪ A_{2} ⟶ B with ω_{1} · ω_{2}(α) := \begin{cases}ω_{1}(α) & if α ∈ A_{1} \\ ω_{2}(α) & if α ∈ A_{2} \end{cases}

For example

[ a/! c/! ] · [ b/? d/? ] = [ a/! b/? c/! d/? ]

Let τ be a world on an atom list A. We can split A in two atom lists: a left atom list A_{L} and an upper atom list A_{U}. We can then represent τ by its double table on A_{L} and A_{U}, which has the form

ω′′_{0}  …  ω′′_{2^{u}−1}  A_{U}
ω′_{0}  τ(ω′_{0} · ω′′_{0})  …  τ(ω′_{0} · ω′′_{2^{u}−1})
⋮  ⋮  ⋮
ω′_{2^{l}−1} τ(ω′_{2^{l}−1} · ω′′_{0}) … τ(ω′_{2^{l}−1} · ω′′_{2^{u}−1})
A_{L}

where [ ω′_{0} … ω′_{2^{l}−1} ] := V al(A_{L}) and [ ω′′_{0} … ω′′_{2^{u}−1} ] := V al(A_{U}).

For example let A = [ hot rain snow wet] and τ be a world on A as given by the table below. If we put A_{L} := [ hot snow] we get A_{U} = A\A_{L} = [ rain wet] and the double table of τ on A_{L} and A_{U} is well–defined:

\begin{matrix}hot & rain & snow & wet \\ ? & ? & ? & ? & ! \\ ! & ? & ? & ? & ! \\ ? & ! & ? & ? & ? \\ ! & ! & ? & ? & ? \\ ? & ? & ! & ? & ? \\ ! & ? & ! & ? & ? \\ ? & ! & ! & ? & ? \\ ! & ! & ! & ? & ? \\ ? & ? & ? & ! & ? \\ ! & ? & ? & ! & ? \\ ? & ! & ? & ! & ? \\ ! & ! & ? & ! & ! \\ ? & ? & ! & ! & ! \\ ! & ? & ! & ! & ? \\ ? & ! & ! & ! & ? \\ ! & ! & ! & ! & ? \end{matrix}  \begin{aligned}& & ? & ! & ? & ! & rain \\ & & ? & ? & ! & ! & wet \\ ? & ? & ! & ? & ? & ? \\ ! & ? & ! & ? & ? & ! \\ ? & ! & ? & ? & ! & ? \\ ! & ! & ? & ? & ? & ? \\ hot & snow \end{aligned}

So, given a theory or a table, there is a unique double table for each specified left (or upper) atom list. On the other hand, each double table represents a unique theory and table.

3 Operations on worlds and atoms lists

Tables and double tables are proper representations for worlds, but as the list of atoms increases, their size grows exponentially. Another way of representing worlds is by means of algebraic expressions (i.e. formulas): taking a subset of basic or atomic worlds, and defining a couple of operations, we can generate all possible worlds by recursively applying these operations on atomic worlds and results of previous operations.

So the most important constants and operations we are going to define are:

• the set of atomic worlds,

• the zero and unit world

• the expansion (∥) and two reductions (⇑,⇓) to in– and decrease the atom sets of worlds, and • the boolean junctions (¬, ∧, ∨, →, ↔).

The theory of the last example can then be written in a more compact form as say

[ ¬[ rain ∧ snow] ∧ [ wet ↔ [ rain ∨ snow] ] ∧ [ rain → hot] ∧ [ snow → h̸ot] ]

what can be read as

“It cannot rain and snow, it is wet if and only if it rains or snows, if it rains, it is hot, and if it snows, it is not hot.”

3.1 Atomic worlds

For every atom α there is a unique atomic world (of α), given by the table

\begin{matrix}α \\ ? & ? \\ ! & ! \end{matrix}

We don’t want to introduce a new notation for this atom world, so we simply write it as α as well. Note that there is a bijection between the set A of atoms and the set of all the atomic worlds generated from A and that should make this convention save against confusions.

3.2 The zero and unit world

If A is the empty set or list [ ] of atoms, there is exactly one valuation of A, namely the valuation ω = [ ]. So there are two well–defined worlds on A, namely

• the zero world, written ⊥, which is given by

⊥ : V al([ ]) ⟶ B with ⊥(ω) := ?

and its table

?

• the unit world, written ⊤, which is given by

⊤ : V al([ ]) ⟶ B with ⊤(ω) := !

and its table

!

3.3 Expansion

Let τ be a world on an atom list A and let B = [ α′_{1} … α′_{n}] a second atom list. The expansion of τ with B is written

[ τ ∥ B] or [ τ ∥ α′_{1} … α′_{n}]

and it is defined to be the theory on A ∪ B that is equivalent to the original theory τ. A proper definition of the equivalence relation is given below and it is introduced by means of the expansion operation. For now we only need to describe how to constuct the new world: let B′ := B\A, so B′ and A are disjunct and A ∪ B′ = A ∪ B, then

[ τ ∥ B] : (A ∪ B′) ⟶ B with [ τ ∥ B](ω · ω′) := τ(ω)

for every ω ∈ V al(A) and ω′ ∈ V al(B′).

This definition can be demonstrated with the use of double tables. Given A := [ a c] and B := [ a b d] and a world τ on A defined by the table

\begin{matrix}a & c \\ ? & ? & ! \\ ! & ? & ? \\ ? & ! & ! \\ ! & ! & ! \end{matrix}

In order to construct [ τ ∥ B] we first subtract A from B and get B′ := B\A = [ b d]. Then we build the double table on A and B′, in which each row has the same bit values than the original table, but multiplied over the whole row. Finally this double table can be transformed into its table form, and that’s the result [ τ ∥ B]. For our example that means

\begin{matrix}a & c \\ ? & ? & ! \\ ! & ? & ? \\ ? & ! & ! \\ ! & ! & ! \end{matrix} becomes \begin{aligned}& & ? & ! & ? & ! & b \\ & & ? & ? & ! & ! & d \\ ? & ? & ! & ! & ! & ! \\ ! & ? & ? & ? & ? & ? \\ ? & ! & ! & ! & ! & ! \\ ! & ! & ! & ! & ! & ! \\ a & c \end{aligned} which is \begin{matrix}a & b & c & d \\ ? & ? & ? & ? & ! \\ ! & ? & ? & ? & ? \\ ? & ! & ? & ? & ! \\ ! & ! & ? & ? & ? \\ ? & ? & ! & ? & ! \\ ! & ? & ! & ? & ! \\ ? & ! & ! & ? & ! \\ ! & ! & ! & ? & ! \\ ? & ? & ? & ! & ! \\ ! & ? & ? & ! & ? \\ ? & ! & ? & ! & ! \\ ! & ! & ? & ! & ? \\ ? & ? & ! & ! & ! \\ ! & ? & ! & ! & ! \\ ? & ! & ! & ! & ! \\ ! & ! & ! & ! & ! \end{matrix}

3.4 Boolean junctions of worlds

For every world τ on A the negation of τ is the world ¬τ on A, defined by

¬τ : V al(A) ⟶ B with ¬τ_{1}(ω) := \begin{cases}? & if τ(ω) = ! \\ ! & if τ(ω) = ? \end{cases}

Let τ_{1}, …, τ_{n} be worlds, n ≥ 0, all on the same atom list A. We define the following new worlds on A, as results of operations on the given ones:

[ τ_{1} ∧ ⋯ ∧ τ_{n}] : V al(A) ⟶ B with [ τ_{1} ∧ ⋯ ∧ τ_{n}](ω) := \begin{cases}? & if ? ∈ \{τ_{1}(ω), …, τ_{n}(ω)\} \\ ! & if ? ∉ \{τ_{1}(ω), …, τ_{n}(ω)\} \end{cases}
[ τ_{1} ∨ ⋯ ∨ τ_{n}] : V al(A) ⟶ B with [ τ_{1} ∨ ⋯ ∨ τ_{n}](ω) := \begin{cases}? & if ! ∉ \{τ_{1}(ω), …, τ_{n}(ω)\} \\ ! & if ! ∈ \{τ_{1}(ω), …, τ_{n}(ω)\} \end{cases}
[ τ_{1} → τ_{2} ] : V al(A) ⟶ B with [ τ_{1} → τ_{2} ](ω) := \begin{cases}? & if τ_{1}(ω) ≮ τ_{2}(ω) \\ ! & if τ_{1}(ω) < τ_{2}(ω) \end{cases}
[ τ_{1} ↔ τ_{2} ] : V al(A) ⟶ B with [ τ_{1} ↔ τ_{2} ](ω) := \begin{cases}? & if τ_{1}(ω) ≠ τ_{2}(ω) \\ ! & if τ_{1}(ω) = τ_{2}(ω) \end{cases}

More general, for every list of worlds τ_{1}, …, τ_{n} with n ≥ 0 we define

[ τ_{1} ∧ ⋯ ∧ τ_{n}] := [ [ τ_{1} ∥ A] ∧ ⋯ ∧ [ τ_{n} ∥ A] ] with A := ⋃_{i=1}^{n} @τ_{i}
[ τ_{1} ∨ ⋯ ∨ τ_{n}] := [ [ τ_{1} ∥ A] ∨ ⋯ ∨ [ τ_{n} ∥ A] ] with A := ⋃_{i=1}^{n} @τ_{i}
[ τ_{1} → τ_{2} ] := [ [ τ_{1} ∥ A] → [ τ_{2} ∥ A] ] with A := @τ_{1} ∪ @τ_{2}
[ τ_{1} ↔ τ_{2} ] := [ [ τ_{1} ∥ A] ↔ [ τ_{2} ∥ A] ] with A := @τ_{1} ∪ @τ_{2}

For example, let τ_{1} := [ a ∥ c] and τ_{2} := [ c ∥ b]. Their tables are

\begin{matrix}a & c & τ_{1} \\ ? & ? & ? \\ ! & ? & ! \\ ? & ! & ? \\ ! & ! & ! \end{matrix}  and  \begin{matrix}b & c & τ_{2} \\ ? & ? & ? \\ ! & ? & ? \\ ? & ! & ! \\ ! & ! & ! \end{matrix}

Their negations are

\begin{matrix}a & c & ¬τ_{1} \\ ? & ? & ! \\ ! & ? & ? \\ ? & ! & ! \\ ! & ! & ? \end{matrix}  and  \begin{matrix}b & c & ¬τ_{2} \\ ? & ? & ! \\ ! & ? & ! \\ ? & ! & ? \\ ! & ! & ? \end{matrix}

We put A := @τ_{1} ∪ @τ_{2} = [ a c] ∪ [ b c] = [ a b c] and generate [ τ_{1} ∥ A] and [ τ_{2} ∥ A]:

\begin{matrix}a & b & c & [ τ_{1} ∥ A] \\ ? & ? & ? & ? \\ ! & ? & ? & ! \\ ? & ! & ? & ? \\ ! & ! & ? & ! \\ ? & ? & ! & ? \\ ! & ? & ! & ! \\ ? & ! & ! & ? \\ ! & ! & ! & ! \end{matrix}  and  \begin{matrix}a & b & c & [ τ_{2} ∥ A] \\ ? & ? & ? & ? \\ ! & ? & ? & ? \\ ? & ! & ? & ? \\ ! & ! & ? & ? \\ ? & ? & ! & ! \\ ! & ? & ! & ! \\ ? & ! & ! & ! \\ ! & ! & ! & ! \end{matrix}

We then obtain the worlds [ τ_{1} ∧ τ_{2} ], [ τ_{1} ∨ τ_{2} ], [ τ_{1} → τ_{2} ], [ τ_{1} ↔ τ_{2} ]:

\begin{matrix}a & b & c & [ τ_{1} ∧ τ_{2} ] \\ ? & ? & ? & ? \\ ! & ? & ? & ? \\ ? & ! & ? & ? \\ ! & ! & ? & ? \\ ? & ? & ! & ? \\ ! & ? & ! & ! \\ ? & ! & ! & ? \\ ! & ! & ! & ! \end{matrix}  \begin{matrix}a & b & c & [ τ_{1} ∨ τ_{2} ] \\ ? & ? & ? & ? \\ ! & ? & ? & ! \\ ? & ! & ? & ? \\ ! & ! & ? & ! \\ ? & ? & ! & ! \\ ! & ? & ! & ! \\ ? & ! & ! & ! \\ ! & ! & ! & ! \end{matrix}

\begin{matrix}a & b & c & [ τ_{1} → τ_{2} ] \\ ? & ? & ? & ! \\ ! & ? & ? & ? \\ ? & ! & ? & ! \\ ! & ! & ? & ? \\ ? & ? & ! & ! \\ ! & ? & ! & ! \\ ? & ! & ! & ! \\ ! & ! & ! & ! \end{matrix}  \begin{matrix}a & b & c & [ τ_{1} ↔ τ_{2} ] \\ ? & ? & ? & ! \\ ! & ? & ? & ? \\ ? & ! & ? & ! \\ ! & ! & ? & ? \\ ? & ? & ! & ? \\ ! & ? & ! & ! \\ ? & ! & ! & ? \\ ! & ! & ! & ! \end{matrix}

Results of operations can be used for new operations, so in this way we can recursively generate the worlds and tables of more complex expressions like the earlier mentioned

[ ¬[ rain ∧ snow] ∧ [ wet ↔ [ rain ∨ snow] ] ∧ [ rain → hot] ∧ [ snow → h̸ot] ]

3.5 Infimum and supremum reduction

Let τ be a world on A and B a second atom list.

The expansion [ τ ∥ B] of τ with B was defined to be the world, uniquely defined by two properties: it must be equivalent to τ and its atom list should be A ∪ B.

Accordingly, we could define a reduction of τ with B by saying that the result must be equivalent to τ and have the atom list A ∩ B. But there is a problem: such a world doesn’t exist in general.

Comparing this phenomenon with integer arithmetic, the multiplication i · j is always well– defined, but the division i/j isn’t, as for example in 7/4, where the result 1.75 is not an integer anymore. But we could take the closest integers, here the lower 1 and upper 2 as results of two modified operations, called infimum division ↗ and supremum division ↙, e.g. 1 = 7 ↗ 4 ≤ 7/4 ≤ 7 ↙ 4 = 2 and 9 = 10 ↗ 3 ≤ 10/3 ≤ 10 ↙ 3 = 10.

Back to worlds (where the role of the integer order ≤ is taken by the order relation ⇒), we also define two reductions, the closest lower and upper reduction, called infimum reduction [ τ ⇑ B] of τ onto B and supremum reduction [ τ ⇓ B] of τ onto B. It turns out to be more convenient for later purposes, that the new atom list is not set to A ∩ B, but to B itself (although the results of both approaches are always equivalent). So an atomic “reduction” not necessarily “reduces” the atom list, but may also introduce new atoms.

The introduction of these operations can again be well demonstrated by using double tables: First, put A′ := A\B and construct the double table of [ τ ∥ B] with left atoms B and upper atoms A′. For the infimum reduction, the bit values of each row have to be replaced by their conjunction. For the supremum reduction, the bit values of each row have to be replaced by their disjunction. For example, let us reduce the last example theory τ onto B := [ hot rain]. The table on B and A′ = [ snow wet] is given by

? ! ? ! snow
? ? ! ! wet
?  ?  ! ? ? !
!  ?  ! ? ? ?
?  !  ? ? ? ?
!  !  ? ? ! ?
hot rain

The infimum reduction [ τ ⇑ B] is then given by

\begin{matrix}hot & rain & [ τ ⇑ B] \\ ? & ? & [ ! ∧? ∧? ∧! ] \\ ! & ? & [ ! ∧? ∧? ∧? ] \\ ? & ! & [ ? ∧? ∧? ∧? ] \\ ! & ! & [ ? ∧? ∧! ∧? ] \end{matrix}  which is  \begin{matrix}hot & rain & [ τ ⇑ B] \\ ? & ? & ? \\ ! & ? & ? \\ ? & ! & ? \\ ! & ! & ? \end{matrix}

and the infimum reduction [ τ ⇓ B] is then given by

\begin{matrix}hot & rain & [ τ ⇓ B] \\ ? & ? & [ ! ∨? ∨? ∨! ] \\ ! & ? & [ ! ∨? ∨? ∨? ] \\ ? & ! & [ ? ∨? ∨? ∨? ] \\ ! & ! & [ ? ∨? ∨! ∨? ] \end{matrix}  which is  \begin{matrix}hot & rain & [ τ ⇓ B] \\ ? & ? & ! \\ ! & ? & ! \\ ? & ! & ? \\ ! & ! & ! \end{matrix}

A formal definition for arbitrary worlds τ and atom lists B are given by: [ τ ⇑ B] : V al(B) ⟶ B with

[ τ ⇑ B](ω) := [ τ(ω · ω′_{1}) ∧ ⋯ ∧ τ(ω · ω′_{n}) ] for [ ω′_{1} … ω′_{n}] := V al(@τ\B)

[ τ ⇓ B] : V al(B) ⟶ B with

[ τ ⇓ B](ω) := [ τ(ω · ω′_{1}) ∨ ⋯ ∨ τ(ω · ω′_{n}) ] for [ ω′_{1} … ω′_{n}] := V al(@τ\B)

3.6 Remark about the chosen notations

The titles of these two new operations come from the fact that, of all theories on the new atom list B, [ τ ⇑ B] is the greatest lower bound (i.e. the infimum) and [ τ ⇓ B] is the least upper bound (i.e. the supremum), with respect to the subvalence relation ⇒ defined below. So, [ τ ⇑ B] ⇒ τ ⇒ [ τ ⇓ B] always holds.

In lattice theory infimum is synonymous to conjunction, and that stipulates the notation ⇑ as “∧ and ∥”. The same holds for supremum, disjunction and the ⇓ symbol.

The ∥ symbol itself is chosen due to its similarities with the symbolism f|B, which usually denotes the reduction of the domain A of a function f : A ⟶ C onto a subset B ⊆ A.

4 Relations between worlds

On the set of all worlds (on A) we define the following relations.

• The atomic order relations: For every pair τ_{1}, τ_{2} of worlds we put

τ_{1} ˆ⊆ τ_{2} :iff @τ_{1} ⊆ @τ_{2}

saying that τ_{1} is subatomic to τ_{2}, and

τ_{1} ˆ= τ_{2} :iff @τ_{1} = @τ_{2}

saying that τ_{1} and τ_{2} are equiatomic.

• The boolean order relations:

For every pair τ_{1}, τ_{2} of worlds we put

τ_{1} ⇒ τ_{2} :iff [ τ_{1} ∥ A] < [ τ_{2} ∥ A], for all ω ∈ V al(A) with A := @τ_{1} ∪ @τ_{2}
:iff [ τ_{1} → τ_{2} ] is valid

saying that τ_{1} is subvalent to τ_{2}, and

τ_{1} ⇔ τ_{2} :iff [ τ_{1} ∥ A] = [ τ_{2} ∥ A], for all ω ∈ V al(A) with A := @τ_{1} ∪ @τ_{2}
:iff [ τ_{1} ↔ τ_{2} ] is valid

saying that τ_{1} and τ_{2} are equivalent.

• The theory order relations:

For every pair τ_{1}, τ_{2} of worlds we put

τ_{1} ˆ⇒ τ_{2} :iff τ_{1} ˆ⊆ τ_{2} and τ_{1} ⇒ τ_{2}

saying that τ_{1} is bisubvalent to τ_{2}, and

τ_{1} ˆ⇔ τ_{2} :iff τ_{1} ˆ= τ_{2} and τ_{1} ⇔ τ_{2}

saying that τ_{1} and τ_{2} are biequivalent.

Each of the three relations ˆ⊆ , ⇒, ˆ⇒ is a quasi–order relation, i.e. it is reflexive and transitive on the set of all worlds. Each of the three relations ˆ= , ⇔, ˆ⇔ is the according equivalence relation of the given quasi–order, i.e. for example τ_{1} ˆ= τ_{2} iff τ_{1} ˆ⊆ τ_{2} and τ_{2} ˆ⊆ τ_{1}.

Note, that for the algebra of worlds the biequivalence is the identity relation, i.e.

τ_{1} ˆ⇔ τ_{2} iff τ_{1} = τ_{2}

Relations can be defined as binary operations with B as codomain. For example, ⇒ can be defined as an operation [ ⋯ ⇒ …] that takes two worlds τ_{1} and τ_{2} and returns a bit value

[ τ_{1} ⇒ τ_{2} ] := \begin{cases}! & if τ_{1} ⇒ τ_{2}, i.e. if τ_{1} if subvalent to τ_{2} \\ ? & if τ_{1} ⇏ τ_{2}, i.e. if τ_{1} is not subvalent to τ_{2} \end{cases}

5 More operations

5.1 Negative and positive atoms

An atom α is negative or redundant in a world τ if it doesn’t matter what bit value it takes: for every ω ∈ V al(@τ\[ α]), ω · [ α/? ] is a possible state iff ω · [ α/! ] is a possible state, too. The term “redundant” emphasizes the fact that, if α is redundant in τ, there is an equivalent world without α.

Using double tables, we can determine if α is negative in τ by representing it with the left atoms @τ\[ α] and upper atoms [ α]. α is indeed negative in τ iff the two given bit values are the same in each row.

For example, let τ := [ a ∨ [ c ∧ ¬c] ∨ b]. Obviously, c is redundant / negative in τ, because τ ⇔ [ a ∨ b]. The double table with c as the only upper atom shows that as well, each row is made of just one bit value:

? ! c
? ? ? ?
! ? ! !
? ! ! !
! ! ! !
a b

For a full definition, let us put for every world τ and every atom α (where not necessarily α ∈ @τ has to hold):

• α is negative or redundant for τ iff

[ τ ⇑ [ @τ\[ α] ] ] ⇔ [ τ ⇓ [ @τ\[ α] ] ]

• α is positive or irredundant for τ iff

[ τ ⇑ [ @τ\[ α] ] ] ⇎ [ τ ⇓ [ @τ\[ α] ] ]

If α is an atom in τ, we say that α is negative / positive in τ.

And for every world τ we introduce the notation

−@τ := the ordered list of all negative atoms in τ
+@τ := the ordered list of all positive atoms in τ

Obviously, for every world τ

−@τ ∪ +@τ = @τ
−@τ ∩ +@τ = [ ]

For example, for τ := [ a ∨ [ c ∧ ¬c] ∨ b] there is −@τ = [ c] and +@τ = [ a b].

5.2 Standard reduction

Due to the just given definition, every world τ has an equivalent world which is only made of the positive atoms of τ. Such a world is called a standard reduction of τ and written @|τ. We put

@|τ := [ τ ⇑ +@τ ] = [ τ ⇓ +@τ ]

Consequently, for every world τ there is

τ = [ @|τ ∥ −@τ ]

This theorem is the basis for the so–called extended normal forms of the Bucanon program. If τ is a theory formula, then the PDNF τ_{d} and PCNF τ_{c} of τ are made of irredundant atoms only, so both forms are standard reductions of τ. In order to get not only an equivalent, but also an equiatomic normal form of τ, the negative atoms −@τ are attached again, so [ τ_{d} ∥ −@τ ] is the XPDNF (extended prime disjunctive normal form) of τ and [ τ_{c} ∥ −@τ ] is its XPDNF (extended prime conjunctive normal form).

For example, for τ := [ a ∨ [ c ∧ ¬c] ∨ b]

[ [ ∧a] ∨ [ ∧b] ] is the PDNF of τ, so
[ [ [ ∧a] ∨ [ ∧b] ] ∥ c] is the XPDNF of τ
[ ∧[ a ∨ b] ] is the PCNF of τ, so
[ [ ∧[ a ∨ b] ] ∥ c] is the XPCNF of τ