Theory Algebras

October 2009

From propositional logic to theory algebra

Quick remainder on the syntax and semantics of propositional logic

Given some atom set A, say A = {p,q,r,s} and the set of propositional formulas on A. Two example formulas are [1]

ψ := p → q
υ := ¬(p ∧ ¬ q)&and (r → r)
The semantic of a formula is given by its truth table. For the two example formulas, that is
Let B := {0,1} the set of boolean values and the atom set of a formula φ. Then formally speaking, the truth table of φ is a function of type (@φ → B) → B. Let denote the usual subvalence relation (more commonly called entailment or consequence relation) and the according equivalence relation. For example,
p ⇒ p ∨ ¬r
¬p ∨ r ⇔ p → r

From propositional logic to boolean algebra

Boolean structures are very important structures in mathematics. A typical example is the power set structure P(S), i.e. the set of all the subsets of a given set S. There are at least two ways to define them formally:

  1. As boolean algebras, i.e. a set S with an unary ¬ and two binary operators and , according neutral elements 0 and 1 and so that certain properties (associativity, mutual distributivity, idempotency etc.) are satisfied.
  2. As boolean lattices, i.e. a set S with a partial order (i.e. reflexive, antisymmetric and transitive relation [W-po]) on S, so that there is a least 0 and a greatest element 1, each two elements x, y have a unique least upper x ∨ y and a greatest lower bound x ∧ y.
It turns out, that both definitions denote the same structure. [W-ba]

We just used the same symbols 0,1,¬,, for boolean structures, that we use for propositional formulas before. That is justified, because propositional logic is very much a boolean structure with the according components. But not entirely. In a decent boolean structure, equivalent elements are equal, i.e. the order relation is antisymmetric (φ⇒ψ and ψ⇒φ always implies φ=ψ). Propositional formulas are often equivalent, but different, e.g. ¬(p ∨ ¬r) and r ∧ ¬p. The subvalence relation on formulas is not antisymmetric. It is only a quasi-order (reflexive and transitive [W-qo]) and not a partial order. The least upper bound of two formulas φ and ψ e.g. does always exist, but there are infinitely many equivalent ones, e.g. φ∨ψ, ψ∨φ, ψ∨φ∨0, etc.

The structure on propositional formulas needs a modification to become a proper boolean structure, and the default way to do this is nowadays usually called the Lindenbaum-Tarski algebra [W-lta]. The procedure in general is the so-called the quotient structure in mathematics and the basic idea is the replacement of the single formulas φ by their equivalent classes [φ] := {ψ | ψ ⇔ φ}. On these equivalence classes, the order is now re-defined by [φ] ⇒ [ψ] iff φ ⇒ ψ, and this is now a decent partial order relation. The least upper bound of two members is given by [φ] ∨ [ψ] := [φ ∨ ψ], and similarly for all the other boolean operations.

From propositional logic to theory algebra

The just described algebraization of propositional logic ends thus with a proper boolean algebra, and this is usually considered the standard algebraization of propositional logic. But this standard is questionable and indeed in many circumstances, this algebraization does not preserve all the required properties of propositional logic. We have defined an alternative version under the title of theory algebra. A boolean algebra is the structure induced by the semantic subvalence relation . A theory algebra comprises a second, the syntactic relation, that compares the atom sets. [2]

Let us go back to the truth tables, e.g. the truth table of υ = ¬(p ∧ ¬ q)&and (r → r). Formally, this truth table is a function (@υ → B) → B with @υ = {p,q,r}. The formula ψ = p → q is equivalent to υ, in the Lindenbaum algebra [ψ] and [υ] are identical. But the truth table of ψ is a function of type ({p,q} → B) → B, and that is different to the truth table of υ. Next to the semantic quasi-order relation , there is also the syntactic quasi-order relation, the subatomic relation, defined by φ ⊆ ψ iff @φ ⊆ @ψ. Accordingly, there is also the derived equivalence relation, the equiatomic relation, φ ≈ ψ iff @φ = ψ [3]. And in a theory-algebraic sense, two formulas are identical if and only if they are bi-equivalent, i.e. semantically and syntactically equivalent.

The boolean junctors , , etc. are atomic accumulators in the sense that @(φ ∧ ψ) = @φ &cup @ψ etc. A theory algebra has also an operator called extension that takes a formula φ and an atom α (or a set of atoms) and returns the resulting formula φ' with φ' ⇔ φ and @φ' = @φ ∪ {α}, i.e. φ' is equivalent to φ, but has an extended atom set [4]. Next to the extension, there is also an elimination of a specified atom from a given formula, or similarly, a reduction of a given formula onto a specified set of atoms. But different to the extension, this is not possible with an equivalent result, at least not in general. There is however always a unique supremum (or greatest lower bound) and infimum, i.e. elimination and reduction come in two flavors:

Of course, conj denotes the conjunction or g.l.b. operator, but we may as well use infimum or minimum in the propositional formula case, it does not make a difference here, and similarly for disj. In actual implementations of theory-algebraic propositional logic, the previous four operations are quite difficult to realize. Nevertheless, there are well-defined algorithms and we used them in several software versions [5].

More on propositional theory algebras

So far the characterization of theory algebras, emerging as an algebraization of propositional logic. We elaborated these ideas in several directions:

From propositional theory algebra to theory algebras of relations

It turned out, that the whole design so far could be extended in the same spirit towards an algebraization of predicate logic. The concept of a theory algebra is therefore generalized as well, and in its most general form this is now a theory algebra of relations.

Schematic relations and their algebra

We mentioned the truth table (or binary world) as the typical representation of a propositional theory algebra. Consider the truth table of the initial example υ, depicted as the table diagram and formalized as a function of type ({p,q,r} → B) → B. An alternative formalization is that of a schematic relation [6]. The set {p,q,r} is now called the index set, the schema X is the record that maps each index to its domain, in this case the domain for each one is the boolean value set B = {0,1}, e.g. X(p) = Xp = Xq = Xr = B. The overall domain of the whole relation is the cartesian product ⊗X of X, here the 23=8 records that map p, q, r to one member of B, each. Finally, the relation itself is defined by this schema or domain (as its type) and the graph, which is a subset of the domain, namely exactly the 6 of the 8 records, for which the truth table is true (or 1) in the result column. Different to truth tables, these schematic relations may have arbitrary, even infinite index sets, an arbitrary domains for each index and arbitrary graphs.

A theory algebra of relations is made of these schematic relations. It has a semantic and a syntactic structure similar to the propositional case, with the same boolean junctions (negation, conjunction etc.) and an extension, infimum and supremum eliminations and reductions. [7]

More on the generalization of theory algebras

All this is well-elaborated meanwhile in a book-size text called Theory algebra of relations [8]. Some additional chapters and the algebraization of predicate logic is treated in an upcoming text which is currently only in a draft [9] version.

Links and footnotes

The following Wikipedia entries provide more information and links on some of the notions we discussed:

[home] [blog]