Axioms of theory algebras

www.bucephalus.org

October 2, 2002

Contents

1 Preliminaries 2 1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Definitions of theory algebras 2 2.1 Basic sets, operations and relations . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Characterizations of theory algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.3 Subalgebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.4 Special theories and theory decompositions . . . . . . . . . . . . . . . . . . . . . . . 3

3 Models of theory algebras 4 3.1 The (non–canonic, non–complete) theory algebra of formulas . . . . . . . . . . . . . 4 3.2 The two canonic theory algebras of extended prime normal forms . . . . . . . . . . . 5 3.3 The complete canonic theory algebra of worlds . . . . . . . . . . . . . . . . . . . . . 6

4 Appendix: The axiom system of a complete theory algebra 7

1 Preliminaries

1.1 Overview

Objective of this paper is a concise and exhaustive axiomatic definition of a theory algebra. The final result of this effort is given on the four pages of the appendix (section 4). Of course, this presentation is rather a dense summary than a proper introduction, so at least some explanation is given (section

2) along with the most important models of theory algebras (section 3): the theory algebras based on formulas and worlds.

There is a very close relationship between theories (as abstract elements of a theory algebra), formulas and worlds: Worlds are the most intuitive representation of theories and their properties. But in general, they are not suitable for daily life and computer implementations. This is the real strength of formulas, which can be seen as representations of worlds

— at least if the worlds are finite.

So if you need a gentle introduction into theory algebras, this axiomatic appoach is not the first choice. You should rather consult the various documentations on the mentioned standard models first, also available on www.bucephalus.org.

1.2 Notations

Placeholders or anonymous variables are used to denote the syntax of function and relation symbols. For example, □ξ□ means, that the operation or relation ξ is defined to be written in infix notation.

Next to the standard symbolism we use the following notations:

X\Y := {x ∈ X|x ∉ Y } set sub-

traction

P (X) is the power set of X, i.e.

the set of all its subsets

F in(X) the set of all finite subsets

of X

X^{∗} sequences or lists with components from X

f : X ⟶ Y denotes a function f from X

into Y

R : X ↭ Y denotes a relation R between X and Y

2 Definitions of theory algebras

2.1 Basic sets, operations and relations

(See the first two parts of the axiom system below: signature and axioms.)

A theory algebra is made of two sets

X (theories) A (atoms)

a couple of boolean junctions and relations

⊑ ⊒ ≡ ⊥ ⊤ ⊓ ⊔ ¬ → ↔

and some non–boolean operations and relations

@ @^{−} @^{+} ˆ⊆ ˆ⊇ ˆ= ∥ ⇓ ⇑ @| ˆ⊑ ˆ⊒ ˆ≡

such that a certain set of axioms (see below) is satisfied.

The theory algebra is complete if two more boolean junctors ∏ and ∐ are defined too.^{1}

The theory algebra is canonic, if the biequivalence is the identitiy on X, i.e. if x ˆ≡ y implies x = y, for all x, y ∈ X.

2.2 Characterizations of theory algebras

It is a common exercise in mathematics to reduce the number of operations and axioms in an axiomatic definition. For example, a canonic theory algebra is fully determined by the quadrupel (X , ⊑, A, @ ). Every other relation and operation is then just a derived concept.

It is also possible to define theory algebras in terms of order– and lattice theory, but only if this whole subject is first generalized from posets (sets with a transitive, reflexive and antisymmetric relation) to quasi– ordered sets (sets with a transitive and reflexive relation). In this context, there is a sequence of specializations: quasi–ordered set, quasi–lattice, boolean quasi–lattice, free boolean quasi–lattice, that finally allows to define a theory algebra as a free boolean quasi–lattice with a certain atom structure (A, @ ) attached.^{2}

1Actually, if the theory algebra is not complete, some modifications of the axiom system would have to be made. In particular, every occurence of P (A) in the type definitions would have to be replaced by F in(A) or A^{∗}.

2This whole generalization of lattice theory and reconstruction of theory algebras is subject to a forthcoming paper.

But in practice it is probably more convenient to approach theory algebras as an axiomatic definition of their standard models, namely world algebras^{3} (see below). It can be shown that any given theory algebra on an atom set A is quite the same as the world algebra on A.Or putting it another way, a theory algebra is categorically defined by the cardinality of its atom set A, because:

• Every theory algebra has a canonization, e.g. by replacing X by the quotient set X / ˆ≡ .

• Every theory algebra has a completion, i.e. an embedding into a complete theory algebra.

• If X_{1} and X_{2} are two canonic, complete theory algebras, then X_{1} and X_{2} are isomorph iff A_{1} and A_{2} have the same cardinality.

All this justifies the use of T h(A) as the standard identifier for a whole canonic theory algebra on a given set A.

2.3 Subalgebras

(See the part called subalgebras in the axiom system below.)

For a given atom set A ∈ P (A), T h(A) is the subalgebra of all the theories on A, and F inT h(A) is the subalgebra of all finite theories on A.

If T h(A) is a canonic theory algebra, then it has two distinguished boolean subalgebras, which are no proper theory algebras anymore: the set XT h(A) of all expanded theories on A, where each member x has @ (x) = A, and the set RT h(A) of reduced theories on A, where each member x has @ (x) = @^{+} (x) ⊆ (A).

For example, if the theory algebra is canonic and A = {a} ⊆ A, then

T h(A) = {⊥, ⊥ ∥ A, a, ¬a, ⊤, ⊤ ∥ A}
RT h(A) = {⊥, a, ¬a, ⊤}
XT h(A) = {⊥ ∥ A, a, ¬a, ⊤ ∥ A}

Recall, that e.g. ⊥ ∥ A ˆ≡ a ⊓ ¬a, but ⊥ ∥ A ˆ≢ ⊥, so that ⊥ and ⊥ ∥ A are two equivalent, but different entities in terms of theory algebras.

2.4 Special theories and theory decompositions

(See the according part in the axiom system below.)

A literal is either an atom (positive literal) or a negated atom (negative literal).

Suppose the given the algebra is canonic and complete.

• A theory is an elementary theory or elem^{4} is a direct ⊑–successor of ⊥. Elem(A) denotes the set of all elems with atom set A.

• A theory is a coelementary theory or coelem is a direct ⊑–predecessor of ⊤. Coel(A) is the set of all coelems with atom set A.

Another criterion for elems and coelems on a given A in free quasi–boolean algebras is the fact that they are the literal conjunctions and disjunctions where each atom of A occurs either negative or positive, i.e.

• c ∈ Elem(A) iff there is a B ⊆ A with

c ˆ≡ ∏ {¬b | b ∈ B} ⊓ ∏(A\B)

• d ∈ Coel(A) iff there is a B ⊆ A with

d ˆ≡ ∐ {¬b | b ∈ B} ⊔ ∐(A\B)

This criterion is actually taken as the definition for elems and coelems in (non–canonic) theory algebras, because the first characterization implies that there might be different, but (bi–)equivalent elems and coelems, respectively. But we need these sets to be canonic or minimal, similar to a basis defined in linear algebra.

For example, ¬a_{1} ⊓ a_{2} ⊓ a_{3} ⊓ a_{4} ⊓ ¬a_{5} is an elem on {a_{1}, a_{2}, a_{3}, a_{4}, a_{5}}.

Note, that in non–complete theory algebras and for infinite A, the sets Elem(A) and Coel(A) are empty.

But the set of elems or coelems of a given theory x always makes up x again in the sense that, when

Elem(x) := {c ∈ Elem(@ (x)) | c ⊑ x}
Coel(x) := {d ∈ Coel(@ (x)) | x ⊑ d}

3So the best way of understanding the definition, i.e. the relations and operations of a theory algebra is probably an introduction of a world algebra. See the paper on World algebras, also available on www.bucephalus.org.

4Unfortunately, these successor elements of ⊥ are often called atoms in lattice theory, different to the common definition of atoms in logic and our terminology. Our creation here might not be so lucky either, since now some elements are elementary and others are not. But it does reflect the analogy with sets, because in elementary boolean algebras, every member is a union (i.e. disjunction) of its elems. then

x ≡ ∐ Elem(x) ≡ ∏ Coel(x)

This elementary and coelementary reconstruction of a theory resembles the equivalent representation of a given formula by its natural conjunctive / disjunctive normal form. ^{5}

For example, for a theory x = a ↔ b in a canonic theory algebra, there is

• Elem(x) = {¬a ⊓ ¬b, a ⊓ b}, so that x ≡ (¬a ⊓ ¬b) ⊔ (a ⊓ b)

• Coel(x) = {¬a ⊔ b, a ⊔ ¬b}, so that x ≡ (¬a ⊔ b) ⊓ (a ⊔ ¬b)

The union F ac(A) := ⋃_{B⊆A} Elem(B) of elems is the set of all the factors. In other words, a factor is just a normal literal conjunction, where normal means that no atom occurs positive as well as negative. Dually, a cofactor is a normal literal disjunction.

The factor set F ac(x) of a given theory x is defined to be the set of all subvalent factors of x from F ac(@ (x)). Accordingly, the supervalent cofactors make up the cofactor set Cof(x) of x.

3 Models of theory algebras

3.1 The (non–canonic, non–complete) theory algebra of formulas

Let A be a set of identifiers and F orm(A) the set of boolean formulas^{6}, i.e. the expressions generated from A and at least the symbols ∧, ∨, ¬. For ∧ and ∨ it is very convenient to define them for any finite amount of arguments, including 0 and 1, such as [ ∧] and [ ∧¬a]. For an elegant canonization, the symbol ∥ is also very useful, but it can as well be replaced, for example by using

[ φ ∥ φ_{1} … φ_{n}] := [ φ ∨ [ [ ∨] ∧ φ_{1} ∧ ⋯ ∧ φ_{n}] ]

If ⊑ is the usual subvalence or consequence relation on F orm(A) (also written as ⇒ or ⊧), then (F orm(A), ⊑) is a free boolean quasi–lattice on A. It is really “quasi”, i.e. non–canonic, because there are equivalent, but non–identical formulas like [ a ∧ ¬b] and [ ¬b ∧ a].

The most natural way to define the boolean junctors by means of ∧, ∨ and ¬ is given by

⊥ := [ ∨]
⊤ := [ ∧]
φ_{1} ⊓ φ_{2} := [ φ_{1} ∧ φ_{2} ]
φ_{1} ⊔ φ_{2} := [ φ_{1} ∨ φ_{2} ]
φ_{1} → φ_{2} := [ ¬φ_{1} ∨ φ_{2} ]
φ_{1} ↔ φ_{2} := [ [ φ_{1} ∧ φ_{2} ] ∨ [ ¬φ_{1} ∧ ¬φ_{2} ] ]

But there are plenty of alternative definitions, like

⊥ := ¬[ ∧]
φ_{1} ⊓ φ_{2} := [ φ_{2} ∧ φ_{1} ∧ φ_{2} ] ... etc

By definition, formulas are always finite expressions. So there is no ∏ and ∐ defined on arbitrary sets of formulas, the structure is not complete.

@ (φ) is the atom set occuring in a formula φ. For example, @ [ a ∧ ¬b ∧ ¬a] = {a, b}. For a proper implementation, the result of @ (φ) would rather be an ordered list instead of a finite set, assuming that there is some strict linear order < defined on A.

An atom α is negative or redundant in a formula φ, if there is a formula φ′ equivalent to φ that doesn’t contain α. So, @^{−} (φ) is the negative atom set of φ and @^{+} (φ) := @ (φ)\@^{−} (φ) is its positive atom set.

The atomic and theory order and equivalence relations are introduced as

φ_{1} ˆ⊆ φ_{2} :iff @ (φ_{1}) ⊆ @ (φ_{2})
φ_{1} ˆ= φ_{2} :iff @ (φ_{1}) = @ (φ_{2})
φ_{1} ˆ⊑ φ_{2} :iff φ_{1} ⊑ φ_{2} and φ_{1} ˆ⊆ φ_{2}
φ_{1} ˆ≡ φ_{2} :iff φ_{1} ≡ φ_{2} and φ_{1} ˆ= φ_{2}

The expansion is easy: for every list [ α_{1} … α_{n}] of atoms and formula φ, we put

φ ∥ [ α_{1} … α_{n}] := [ φ ∥ α_{1} … α_{n}]

But for the two reductions ⇑, ⇓: F orm(A)× A^{∗} ⟶ F orm(A) the result would have to be some kind of normal form in general, at least if only boolean formulas allowed. The same holds for @| (φ), the standard reduction of

5Commonly called canonic conjunctive / disjunctive normal form. But this title is incorrect, because e.g. if φ ≡ ⊥, it has many equivalent “canonic” conjunctive normal forms, such as [ [ ∨¬a] ∧ [ ∨a] ] and [ [ ∨¬b] ∧ [ ∨b] ].

6See Bucanon syntax or the Bucanon manual on www.bucephalus.org for a proper definition of boolean and theory formulas. φ, which must be an equivalent form without negative atoms.

A factor is a normal literal conjunction [ λ_{1} ∧ ⋯ ∧ λ_{n}]. We remove all ambiguities by demanding that the atoms of the literals are written in strict linear order, and the order < on A is predifined.

Factors on A = {a_{1}, a_{2}, a_{3}} with a_{1} < a_{2} < a_{3} are, for example: [ ¬a_{1} ∧ a_{2} ∧ ¬a_{3} ], [ a_{1} ∧ ¬a_{2} ∧ ¬a_{3} ], [ ¬a_{1} ∧ ¬a_{3} ], [ ∧] and [ a_{2} ∧ a_{3} ]. Only the first two example factors are elementary or elems on A.

A factor is elementary or an elem on a given atom set A, if it contains all atoms of A.

For a given formula φ, say φ = [ a → b], a factor of φ is a factor γ with γ ⊑ φ, e.g. γ = [ ¬a ∧ b]. Elementary factors or elems of φ are the longest, prime factors of φ are the maxima of all these factors.

Dual to factors, elems and primes, the notions cofactors, coelems and coprimes are defined for formulas.

For every formula φ the following boolean normal form theorems hold:

• φ is equivalent to the disjunction of its elems. (natural DNF) For the example φ := [ a → b] this is: φ ≡ [ [ ¬a ∧ ¬b] ∨ [ ¬a ∧ b] ∨ [ a ∧ b] ]

• φ is equivalent to the conjunction of its coelems. (natural CNF) For the example, φ ≡ [ ∧[ ¬a ∨ b] ]

• φ is equivalent to the disjunction of its primes. (prime DNF or PDNF) For example, φ ≡ [ [ ∧¬a] ∨ [ ∧b] ]

• φ is equivalent to the conjunction of its coprimes. (prime CNF or PCNF) For the example, the natural and the prime CNF are equal: φ ≡ [ ∧[ ¬a ∨ b] ]

These boolean, i.e. equivalent normal forms are not theory normal forms, i.e. biequivalent in general, because they are not always equiatomic to the original form. For example, for φ := [ a → a], the PCNF of φ is [ ∧], but @ (φ) = {a} ≠ {} = @ ([ ∧]). The reason for this atomic difference is the observation, that in some cases — cases where φ contains negative or redundant atoms — the transformation to the normal form might loose this negative atoms. So, in order to obtain an equiatomic normalization, we simply attach all negative atoms by means of expansion: If φ′ is a boolean normal form of φ, then [ φ′ ∥ @^{−} (φ) ] is a theory normal form, i.e. it is biequivalent to φ.

We define this explicitly for the prime normal forms: For every formula φ with negative atoms {α_{1}, …, α_{n}} and α_{1} < ⋯ < α_{n}:

• If Δ is the PDNF of φ then [ Δ ∥ α_{1} … α_{n}] is the extended PDNF or XPDNF of φ.

• If Γ is the PCNF of φ then [ Γ ∥ α_{1} … α_{n}] is the extended PCNF or XPCNF of φ.

For example, the XPCNF of [ a → a] is [ [ ∧] ∥ a].

3.2 The two canonic theory algebras of extended prime normal forms

Let

• XP DNF (A)

be the set of all XPDNF’s on A

• XP CNF (A)

be the set of all XPCNF’s on A

• xpdnf : F orm(A) ⟶ F orm(A)

the XPDNF–canonizer, which assigns the unique biequivalent XPDNF to each given formula

• xpcnf : F orm(A) ⟶ F orm(A)

the XPCNF–canonizer, which assigns the unique biequivalent XPCNF to each given formula

In the sequel, we concentrate on the XPDNF’s, but the dual statements hold for the XPCNF’s as well.

XP DNF (A) is a subset of F orm(A) and with the same subvalence relation ⊑ it immediately becomes a canonic theory algebra. All the boolean junctions, the expansion and reductions are uniquely determined and don’t depend on the concrete definition in F orm(A), they are given by ⊑ due to the canonicity of XP DNF (A). For example, for all Ξ_{1}, Ξ_{2} ∈ XP DNF (A),

Ξ_{1} ⊓ Ξ_{2} = xpdnf([ Ξ_{1} ∧ Ξ_{2} ])
= xpdnf([ Ξ_{2} ∧ Ξ_{1} ∧ Ξ_{2} ]) = ...

However, XP DNF (A) is not a proper substructure of F orm(A), because one thing has changed: the atoms A of F orm(A) are no longer the atoms of XP DNF (A). Instead, the new atom set is

xpdnf(A) = {[ [ ∨[ ∧α] ] ∥ [ ] ] | α ∈ A}

But since xpdnf defines a bijection between the old and new atom set, we rather write α again for each such atomic XPDNF [ [ ∨[ ∧α] ] ∥ [ ] ].

These two canonic theory algebras XP DNF (A) and XP CNF (A) can be implemented effectively.^{7}

7For a precise definition of these algorithms and a concrete software implementation, see the according sources on www.bucephalus.org.

3.3 The complete canonic theory algebra of worlds

Let B be the set of two bit values, e.g. given by B := {0, 1}.

Let A be any set. A valuation of A is a function ω : A ⟶ B. And a world on A is a function that assigns a bit value to each valuation of A. So, a world τ on A is a function τ : (A ⟶ B) ⟶ B.

If A has n elements, then the set B^{A} of all the valuations of A has 2^{n} elements and the set B^{B^{A}} of all worlds on A has 2^{2^{n}} members.

A world on a finite set can be represented by a table. For example, a world τ on A = {a, b} is given by

\begin{matrix}a & b & τ \\ 0 & 0 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 1 \\ 1 & 1 & 1 \end{matrix}

saying that, for example the valuation ω, given by ω(0) = 1 and ω(1) = 1, has the value τ(ω) = 1.

Another — but ambiguous — representation of finite worlds uses boolean formulas. The last example τ is thus represented by [ ¬a ∨ b] or ¬[ a∧¬b] etc. Each formula φ with @ (φ) = A defines a unique world world(φ) on A.

This relation with boolean formulas motivates the introduction of all boolean relations and junctions. If the formula φ_{i} represents the world τ_{i}, then e.g. negation and conjunction of worlds can be defined by

¬τ_{1} := world(¬φ_{1})
τ_{1} ⊓ τ_{2} := world([ φ_{1} ∧ φ_{2} ])

Note that the definition doesn’t depend on the chosen representing formulas, because worlds are canonic, here in the sense that two formulas are biequivalent if and only if they have the same world.^{8}

An alternative and intuitive introduction of these boolean concepts on worlds goes as follows. A world τ on A is also given as a pair (A, Ω), where Ω is the set of all valuations ω of A with τ(ω) = 1. The subvalence ⊑ on worlds is then exactly the order on sets, with

(A, Ω_{1}) ⊑ (A, Ω_{2}) :iff Ω_{1} ⊆ Ω_{2}

But some more explanations are needed for the general case, where the worlds atom sets are not equal.

Note, that the resulting theory algebra of worlds is not only canonic, but also complete. Infinite A do not need extra care.

Let A be any set, then the world algebra generated by A has the carrier set

W orld(A) := {τ : (A ⟶ B) ⟶ B | A ⊆ A}

But note, that the atom set of this resulting theory algebra is not given by A itself, but by the atomic worlds

τ : ({α} ⟶ B) ⟶ B with ω ↦ ω(α)

for α ∈ A, which are given by

\begin{matrix}α & τ \\ 0 & 0 \\ 1 & 1 \end{matrix}

in tabular notation. But again, due to the bijective relation between the elements of A and these atomic worlds, we can simply write α again, without the danger of confusion.

Similarly for elementary worlds or the elems and factors of this algebra, which can simply be written as valuations, although they are defined to be the worlds, where exactly this one valuation has the value 1.

8For a full introduction of all the relations and operations, see The algebra of worlds on www.bucephalus.org.

4 Appendix: The axiom system of a complete theory algebra

Signature

\underline{Sets} X the set of theories A ⊆ X the set of atoms or atomic theories Atom set functions @ : X ⟶ P (A) atom set function @^{−} : X ⟶ P (A) negative atom set function @^{+} : X ⟶ P (A) positive atom set function Atomic relations □ ˆ⊆ □ : X ↭ X subatomic relation □ ˆ⊇ □ : X ↭ X superatomic relation □ ˆ= □ : X ↭ X equiatomic relation Atomic expansion and reduction □ ∥ □ : X × P (A) ⟶ X expander □ ⇑ □ : X × P (A) ⟶ X infimum reductor □ ⇓ □ : X × P (A) ⟶ X supremum reductor @| : X ⟶ X standard reductor Boolean relations □ ⊑ □ : X ↭ X subvalence □ ⊒ □ : X ↭ X supervalence □ ≡ □ : X ↭ X equivalence Boolean junctors ⊥ ∈ X zero junctor or bottom ⊤ ∈ X unit junctor or top ∏ : P (X) ⟶ X infimum junctor or big conjunctor ∐ : P (X) ⟶ X supremum junctor or big disjunctor □ ⊓ □ : X × X ⟶ X meet or small conjunctor □ ⊔ □ : X × X ⟶ X join or small disjunctor

¬ : X ⟶ X negator

□ → □ : X × X ⟶ X subjunctor □ ↔ □ : X × X ⟶ X equijunctor Theory relations □ ˆ⊑ □ : X ↭ X bisubvalence □ ˆ⊒ □ : X ↭ X bisupervalence □ ˆ≡ □ : X ↭ X biequivalence

Axioms for all x, y, z ∈ X and a, b ∈ A and X, Y, Z ⊆ X and A, B ⊆ A :

Boolean relations ⊑ is a quasi–order relation (i.e. reflexive and transitive) ⊒ is a quasi–order relation (i.e. reflexive and transitive) ≡ is an equivalence relation (i.e. reflexive, transitive and symmetric)

x ⊒ y iff x ⊑ y

x ≡ y iff x ⊑ y and x ⊒ y

Junctor axioms ⊥ ⊑ x least element ⊤ ⊒ x greatest element ⊥ ⊔ x ≡ x neutral element of disjunction ⊤ ⊓ x ≡ x neutral element of conjunction x ⊓ ¬x ≡ ⊥ conjunctive complement x ⊔ ¬x ≡ ⊤ disjunctive complement x ⊓ x ≡ x conjunctive idempotence x ⊔ x ≡ x disjunctive idempotence x ⊓ y ≡ y ⊓ x conjunctive commutativity x ⊔ y ≡ y ⊔ x disjunctive commutativity x ⊓ (y ⊓ z) ≡ (x ⊓ y) ⊓ z conjunctive associativity x ⊔ (y ⊔ z) ≡ (x ⊔ y) ⊔ z disjunctive associativity x ⊓ y ≡ ∏{x, y} small conjunction x ⊔ y ≡ ∐{x, y} small disjunction x ⊓ ∐ Y ≡ ∐ {x ⊓ y | y ∈ Y } distributivity x ⊔ ∏ Y ≡ ∏ {x ⊔ y | y ∈ Y } distributivity ¬ ∏ X ≡ ∐ {¬x | x ∈ X} de Morgan ¬ ∐ X ≡ ∏ {¬x | x ∈ X} de Morgan x → y ≡ ¬x ⊔ y subjunction x ↔ y ≡ (x ⊓ y) ⊔ (¬x ⊓ ¬y) equijunction Atom set function

@ (⊥) = {}

@ (⊤) = {}

@ (a) = {a}

@ (x ⊓ y) = @ (x) ∪ @ (y)

@ (x ⊔ y) = @ (x) ∪ @ (y)

@ (∏ X) = ⋃ {@ (x) | x ∈ X}

@ (∐ X) = ⋃ {@ (x) | x ∈ X}

Atomic relations

x ˆ⊆ y iff @ (x) ⊆ @ (y)

x ˆ⊇ y iff @ (x) ⊇ @ (y)

x ˆ= y iff @ (x) = @ (y)

ˆ⊆ is a quasi–order relation (i.e. reflexive and transitive) ˆ⊇ is a quasi–order relation (i.e. reflexive and transitive) ˆ= is an equivalence relation Theory relations

x ˆ⊑ y iff (x ˆ⊆ y and x ⊑ y)

x ˆ⊒ y iff (x ˆ⊇ y and x ⊒ y)

x ˆ≡ y iff (x ˆ= y and x ≡ y)

ˆ⊑ is a quasi–order relation (i.e. reflexive and transitive) ˆ⊒ is a quasi–order relation (i.e. reflexive and transitive) ˆ≡ is an equivalence relation Defining axioms of expansion and reduction

x ∥ A ˆ≡ x ⊓ (⊤ ⊔ ∐ A) ˆ≡ x ⊔ (⊥ ⊓ ∏ A)

x ⇑ A ˆ≡ ∐ {y ∈ X | @ (y) = A and y ⊑ x}

x ⇓ A ˆ≡ ∏ {y ∈ X | @ (y) = A and y ⊒ x}

Atomic and boolean axioms of expansion and reduction

@ (x ∥ A) = @ (x) ∪ A

@ (x ⇑ A) = A

@ (x ⇓ A) = A

x ∥ A ≡ x

x ⇑ A ⊑ x

x ⇓ A ⊒ x

Expansion and reduction of junctions

⊥ ∥ A ≡ ⊥ ⇑ A ≡ ⊥ ⇓ A

⊤ ∥ A ≡ ⊤ ⇑ A ≡ ⊤ ⇓ A

(¬x) ∥ A ≡ ¬(x ∥ A)

(¬x) ⇑ A ≡ ¬(x ⇓ A)

(¬x) ⇓ A ≡ ¬(x ⇑ A)

(x ⊓ y) ∥ A ≡ (x ∥ A) ⊓ (y ∥ A)

(x ⊓ y) ⇑ A ≡ (x ⇑ A) ⊓ (y ⇑ A)

(x ⊓ y) ⇓ A ⊑ (x ⇓ A) ⊓ (y ⇓ A)

(x ⊔ y) ∥ A ≡ (x ∥ A) ⊔ (y ∥ A)

(x ⊔ y) ⇑ A ⊒ (x ⇑ A) ⊔ (y ⇑ A)

(x ⊔ y) ⇓ A ⊑ (x ⇓ A) ⊔ (y ⇓ A)

(∏ X) ∥ A ≡ ∏ {x ∥ A | x ∈ X}

(∏ X) ⇑ A ≡ ∏ {x ⇑ A | x ∈ X}

(∏ X) ⇓ A ⊑ ∏ {x ⇓ A | x ∈ X}

(∐ X) ∥ A ≡ ∐ {x ∥ A | x ∈ X}

(∐ X) ⇑ A ⊒ ∐ {x ⇑ A | x ∈ X}

(∐ X) ⇓ A ≡ ∐ {x ⇓ A | x ∈ X}

Negative and positive atoms

@^{−} (x) = {a ∈ @ (x) | x ⇑ (@ (x)\{a}) ≡ x ⇓ (@ (x)\{a})}

@^{+} (x) = {a ∈ @ (x) | x ⇑ (@ (x)\{a}) ≢ x ⇓ (@ (x)\{a})}

@^{−} (x) ∩ @^{+} (x) = ∅

@^{−} (x) ∪ @^{+} (x) = @ (x)

x ⇑ @^{−} (x) ≡ x ⇑ ∅

x ⇓ @^{−} (x) ≡ x ⇓ ∅

x ⇑ @^{+} (x) ≡ x

x ⇓ @^{+} (x) ≡ x

Reductions onto ∅

x ⇑ ∅ ˆ≡ \{ \begin{matrix}⊥ & if x ≢ ⊤ \\ ⊤ & if x ≡ ⊤ \end{matrix} infimum reduction onto ∅ as tautology criterion

x ⇓ ∅ ˆ≡ \{ \begin{matrix}⊥ & if x ≡ ⊥ \\ ⊤ & if x ≢ ⊥ \end{matrix} supremum reduction onto ∅ as satisfiability criterion

Standard reduction

@| (x) ≡ x

@^{+} (@| (x)) = @ (@| (x)) = @^{+} (x)

@^{−} (@| (x)) = ∅

Subalgebras for every A ∈ P (A) and all X, Y ⊆ X :

Relations between theory sets X ≡ Y :iff (∀x ∈ X.∃y ∈ Y.x ≡ y) and (∀y ∈ Y.∃x ∈ X.y ≡ x) equivalence X ˆ≡ Y :iff (∀x ∈ X.∃y ∈ Y.x ˆ≡ y) and (∀y ∈ Y.∃x ∈ X.y ˆ≡ x) biequivalence Special theory sets on a given atom set T h(A) := {x ∈ X | @ (x) ⊆ A} the set of theories on A F inT h(A) := {x ∈ X | @ (x) ⊆ A and @ (x) is finite } the set of finite theories on A XT h(A) := {x ∈ X | @ (x) = A} the set of expanded theories on A RT h(A) := {x ∈ X | @ (x) = @^{+} (x) ⊆ A} the set of (standard) reduced theories on A Identification of the algebra by its atom set

X = T h(A)

Algebraic closure properties T h(A) is a complete theory algebra XT h(A) is a complete quasi–boolean algebra RT h(A) is a complete quasi–boolean algebra F inT h(A) is a theory algebra Algebraic closure properties of the quotient structures T h(A)/ ˆ≡ is a canonic complete theory algebra XT h(A)/ ˆ≡ = XT h(A)/ ≡ is a complete boolean algebra RT h(A)/ ˆ≡ = RT h(A)/ ≡ is a complete boolean algebra F inT h(A)/ ˆ≡ is a canonic theory algebra Mutual definability

T h(A) ˆ≡ {x ∥ B | x ∈ RT h(A), B ⊆ A}

T h(A) ˆ≡ {x ⇑ B | x ∈ XT h(A), B ⊆ A}

T h(A) ˆ≡ {x ⇓ B | x ∈ XT h(A), B ⊆ A}

XT h(A) ˆ≡ {x ∥ A | x ∈ T h(A)}

XT h(A) ˆ≡ {x ∥ A | x ∈ RT h(A)}

RT h(A) ˆ≡ {@| (x) | x ∈ T h(A)}

RT h(A) ˆ≡ {@| (x) | x ∈ XT h(A)}

Special theories and theory decompositions for all A ∈ P (A) and x ∈ X :

Special theories on a given atom set Lit(A) := A ∪ {¬a | a ∈ A} the literals on A Elem(A) := {∏ {¬b | b ∈ B} ⊓ ∏(A\B) | B ⊆ A} the elementary theories or elems on A Coel(A) := {∐ {¬b | b ∈ B} ⊔ ∐(A\B) | B ⊆ A} the coelementary theories or coelems on A F ac(A) := ⋃_{B⊆A} Elem(B) the factors on A Cof(A) := ⋃_{B⊆A} Coel(B) the cofactors on A Cardinalities

|Lit(A)| = 2|A|

|Elem(A)| = 2^{|A|}

|Coel(A)| = 2^{|A|}

Subvalent characterizations Elem(A) is (bi)equivalent to the set of all subvalent successors of ⊥ Coel(A) is (bi)equivalent to the set of all subvalent predecessors of ⊤ Partition properties ∐ Elem(A) = ⊤ ∥ A and c_{1} ⊓ c_{2} ≡ ⊥ for c_{1}, c_{2} ∈ Elem(A) with c_{1} ≠ c_{2} ∏ Coel(A) = ⊥ ∥ A and d_{1} ⊔ d_{2} ≡ ⊤ for d_{1}, d_{2} ∈ Coel(A) with d_{1} ≠ d_{2} Special theories of a given theory Elem(x) := {c ∈ Elem(@ (x)) | c ⊑ x} the elements of x Coel(x) := {d ∈ Coel(@ (x)) | x ⊑ d} the coelements of x F ac(x) := {f ∈ F ac(@ (x)) | f ⊑ x} the factors of x Cof(x) := {g ∈ Cof(@ (x)) | x ⊑ g} the cofactors of x P rim(x) := {p ∈ F ac(@ (x)) | p ˆ⊆ f for all f ∈ F ac(x) with f ⊑ p} the primes of x Copr(x) := {q ∈ Cof(@ (x)) | q ˆ⊆ g for all g ∈ Cof(x) with q ⊑ g} the coprimes of x Subset relations between special theories of a given theory

Elem(x) ⊆ F ac(x)

Coel(x) ⊆ Cof(x)

P rim(x) ⊆ F ac(x)

Copr(x) ⊆ Cof(x)

Subvalent characterizations P rim(x) is the set of subvalent maxima of F ac(x) Copr(x) is the set of subvalent minima of Cof(x) Elementary reconstructions of expansion and reduction

x ∥ A ˆ≡ ∐ {c ∈ Elem(A ∪ @ (x)) | c ⊑ x}

x ∥ A ˆ≡ ∏ {d ∈ Coel(A ∪ @ (x)) | x ⊑ d}

x ⇑ A ˆ≡ ∐ {c ∈ Elem(A) | c ⊑ x}

x ⇑ A ˆ≡ ∏ {d ∈ Coel(A) | d ⊔ x ≢ ⊤}

x ⇓ A ˆ≡ ∐ {c ∈ Elem(A) | c ⊓ x ≢ ⊥}

x ⇓ A ˆ≡ ∏ {d ∈ Coel(A) | x ⊑ d}

Theory reconstructions and normal forms ∐ Elem(x) ≡ x with ∐ Elem(x) ˆ≡ x for x ≢ ⊥ natural disjunctive normal form ∏ Coel(x) ≡ x with ∏ Coel(x) ˆ≡ x for x ≢ ⊤ natural conjunctive normal form

∐ F ac(x) ≡ x with ∐ F ac(x) ˆ≡ x for x ≢ ⊥

∏ Cof(x) ≡ x  with  ∏ Cof(x) ˆ≡ x for x ≢ ⊤
∐ P rim(x) ≡ x  with  ∐ P rim(x) ˆ≡ @| (x)
∏ Copr(x) ≡ x  with  ∏ Copr(x) ˆ≡ @| (x)

x ≡ ∐ P rim(x) prime disjunctive normal form (PDNF) x ≡ ∏ Copr(x) prime conjunctive normal form (PCNF)

@ (P rim(x)) = @^{+} (x)

@ (Copr(x)) = @^{+} (x)

x ˆ≡ ∐ P rim(x) ∥ @^{−} (x) expanded PDNF (XPDNF) x ˆ≡ ∏ Copr(x) ∥ @^{−} (x) expanded PCNF (XPCNF)