# 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 

`ψ := 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
`p``q``ψ`
`0``0``1`
`1``0``0`
`0``1``1`
`1``1``1`
and
`p``q``r``υ`
`0``0``0``1`
`1``0``0``0`
`0``1``0``1`
`1``1``0``1`
`0``0``1``1`
`1``0``1``0`
`0``1``1``1`
`1``1``1``1`
respectively.
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. 

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 `@φ = ψ` . 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 . 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:

• `supRed(φ, S) := conj { ψ | @ψ = S, φ ⇒ ψ }` is the supremum reduction of a theory or formula `φ` onto the atom set `S`,
• `infRed(φ, S) := disj { ψ | @ψ = S, ψ ⇒ φ }` is the infimum reduction of `φ` onto `S`,
• `supElim(φ, α) := conj { ψ | @ψ = @φ\{α}, φ ⇒ ψ }` is the supremum elimination of an atom `α` from the theory or formula `φ`,
• `infElim(φ, α) := disj { ψ | @ψ = @φ\{α}, ψ ⇒ φ }` is the infimum elimination of `α` from `φ`.
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 .

### 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:

• Axioms of theory algebras summarizes the essential properties of (propositional) theory algebras
• World algebras describes the theory algebra of "(binary) worlds", another term for what we called truth tables before. This algebra of truth tables or worlds is the most typical (propositional) theory algebra, because there are no ambiguities, two worlds are bi-equivalent, thus identical in a theory-algebraic sense, if they are equal.
• bucanon is a Java applet that works as an online pocket calculator for theory-algebraic problems. It comes with a series of various documents, in particular a small tutorial for the boolean part and a subsequent tutorial for the theory-algebraic operations on propositional logic.

## 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 . 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. 

### More on the generalization of theory algebras

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

•  Due to the limited range of suitable symbols in HTML, we use `→` for the function type expression, as in `f:A→B` and as the symbol for a subjunction, i.e. `φ→ψ`, which is in some texts also introduced as an abbreviation for `¬φ∨ψ`.
•  The symbols `⊆` and `≈` for the sub- and equi-atomic relations are not our first choice. In the LaTeX-encoded texts we use a more distinguished symbolism, but in HTML there is only a limited amount of widely accepted entities so far.
•  This extension of `φ` by `α`, written `[φ || α]` or `ext(φ,α)`, can be defined in propositional logic with the given operators. For example, we could define `ext(φ, α) := φ ∨ (0 ∧ α)` or alternatively as `φ ∧ (α ∨ ¬α)`.
•  In the actual theory-algebraic interpretion of predicate logic, an existentialization `∃v.φ` corresponds to a supremum elimination of the index `v`, and each `∀` turns into an infimum elimination.