bucephalus.org
bucephalus.org
Given some atom set A, say A = {p,q,r,s} and the set of propositional formulas on A. Two example formulas are
[1]
The semantic of a formula is given by its truth table. For the two example formulas, that is
ψ := p → q
υ := ¬(p ∧ ¬ q)&and (r → r)
Let
pqψ001100011111and
pqrυ00011000010111010011101001111111respectively.
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
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:
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.
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.
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.
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:
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 φ.
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].
So far the characterization of theory algebras, emerging as an algebraization of propositional logic. We elaborated these ideas in several directions:
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.
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]
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.
→ 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 ¬φ∨ψ.
⊆ 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.
φ by α, written [φ || α] or ext(φ,α), can be defined in propositional logic with the given operators. For example, we could define ext(φ, α) := φ ∨ (0 ∧ α) or alternatively as φ ∧ (α ∨ ¬α).
∃v.φ corresponds to a supremum elimination of the index v, and each ∀ turns into an infimum elimination.