Propositional Algebras

The Truth-Table Semantics of Formulas

Let us take a simple formula and call it phi. In a ghci session, we can set local definitions with a let-expression, say

  PropLogic> let phi = EJ [A 'x', CJ [A 'y', A 'z']]

This is a formula of type PropForm Char and we can confirm its pure and fancy form with

  PropLogic> phi
  EJ [A 'x',CJ [A 'y',A 'z']]
  PropLogic> display phi
  [x <-> [y * z]]

With the atoms function, we obtain the set of atoms {'x','y','z'} occurring in phi. Actually, the result is not a set, but the strictly ordered list ['x','y','z'], the type is Olist Char, where type Olist a = [a] is simply our type synonym for ordered list, which are used to represent finite sets. Recall, that the list of characters is written as a string in Haskell, so we actually obtain

  PropLogic> atoms phi
  "xyz"

A semantics of propositional formulas is defined by its truth table. The idea is pretty standard and we can ask for the usual intuitive display of the truthTable of phi by calling

  PropLogic> display (truthTable phi)
  +---+---+---+-----------------+
  | x | y | z | [x <-> [y * z]] |
  +---+---+---+-----------------+
  | 0 | 0 | 0 |        1        |
  +---+---+---+-----------------+
  | 0 | 0 | 1 |        1        |
  +---+---+---+-----------------+
  | 0 | 1 | 0 |        1        |
  +---+---+---+-----------------+
  | 0 | 1 | 1 |        0        |
  +---+---+---+-----------------+
  | 1 | 0 | 0 |        0        |
  +---+---+---+-----------------+
  | 1 | 0 | 1 |        0        |
  +---+---+---+-----------------+
  | 1 | 1 | 0 |        0        |
  +---+---+---+-----------------+
  | 1 | 1 | 1 |        1        |
  +---+---+---+-----------------+

The first of the eight (non-header) rows is saying that, if we valuate phi with the valuator that assigns false to each of the atoms, then the evaluation of this valuated formula is true. Actually, we can reconstruct this idea stepwise: A valuator is an ordered list of pairs, made of atoms and boolean values. In our case, the atoms are of type Char, thus the valuator is of type Valuator Char:

  PropLogic> let omega = [('x',False),('y',False),('z',False)] :: Valuator Char

Recall our example formula

  PropLogic> phi
  EJ [A 'x',CJ [A 'y',A 'z']]

the omega-valuation of phi is a nullatomic formula

  PropLogic> valuate omega phi
  EJ [F,CJ [F,F]]

and a nullatomic formula can be evaluated to a boolean value, here:

  PropLogic> boolEval (valuate omega phi)
  True

The combination of a valuation and an evaluation is an application and we can do that, too

  PropLogic> boolApply phi omega
  True

These boolean versions of evaluation and application return Bool values, i.e.

  boolEval :: PropForm a -> Bool
  boolApply :: PropForm a -> Valuator a -> Bool

There are also more general versions, returning formulas again,

  eval :: PropForm a -> PropForm a
  apply :: PropForm a -> Valuator a -> PropForm a

(The actual types of all these definitions are a little more complex; but that is not important here. You can check a type of a value v with the :type or :t command, i.e. type :t v after the prompt and the interpreter returns its type. You can also ask the interpreter to return the type for every output with the command :set +t.)

For the given three atoms 'x', 'y', 'z' there are 2^3 = 8 different valuators, and that are the eight rows of the displayed truth table. So, mathematically speaking, a truth table is a second-order boolean function

  (A -> Bool) -> Bool

where A is the given atom set. Such a construction however is not possible in Haskell, we cannot turn an ordered list of atoms into a type. The idea remains the same, but the actual type definition is

  type TruthTable a = (Olist a, Maybe (PropForm a), [([Bool], Bool)])

(The first argument is the head row of the ordered atoms, the second argument is the optional formula that is repeated in the result column, and the third argument is a straight version of the rows, each one of type ([Bool],Bool).)

The Semantic Structure on Formulas

Truth tables provide us with a denotational semantics for formulas. But there are also the common semantic concepts that alltogether make a quasi-boolean structure. All these notions can be defined in terms of the truth tables. Recall, that a formula is called

• satisfiable

  if the result column of its truth table has at least one 1

• valid

  if the result column of its truth table has only 1's and no 0 at all, and

• contradictory

  if there is no 1's, but only 0's.

For our example formula, this is

  PropLogic> satisfiable phi
  True
  PropLogic> valid phi
  False
  PropLogic> contradictory phi
  False

And there are the usual semantic comparison relations: Two formulas phi and psi are called

• equivalent

  if boolApply phi omega = boolApply psi omega, for every valuator omega

• subvalent

  if boolApply phi omega <= boolApply psi omega, for every valuator omega

We can check that automatically with two functions of the same name. But recall the usual Haskell conventions on binary functions: instead of operating on pairs of formulas, like so

  equivalent (form1, form2)

Haskell functions are usually currfied and called by

  equivalent form1 form2

with the option to place the function between the arguments when wrapped inside backticks

  form1 `equivalent` form2

For example

  PropLogic> (CJ [A 'x', A 'y']) `subvalent` (A 'x')
  True
  PropLogic> (SJ [A 'x', A 'y']) `equivalent` (DJ [N (A 'x'), A 'y'])
  True

You can verify the last example by checking that the truth tables of the two formulas are equal. More conveniently, you can use the multiTruthTable function, that takes a list of formulas as input and displays them by one table with one result column for every formula. An example with three formulas is

  PropLogic> display (multiTruthTable [SJ [A 'x', A 'y'], DJ [N (A 'x'), A 'y'], N (CJ [A 'x', N (A 'y')])])
  +--------------------------------+
  | MultiTruthTable                |
  |  1. [x -> y]                   |
  |  2. [-x + y]                   |
  |  3. -[x * -y]                  |
  | +---+---+------+------+------+ |
  | | x | y |  1.  |  2.  |  3.  | |
  | +---+---+------+------+------+ |
  | | 0 | 0 |  1   |  1   |  1   | |
  | +---+---+------+------+------+ |
  | | 0 | 1 |  1   |  1   |  1   | |
  | +---+---+------+------+------+ |
  | | 1 | 0 |  0   |  0   |  0   | |
  | +---+---+------+------+------+ |
  | | 1 | 1 |  1   |  1   |  1   | |
  | +---+---+------+------+------+ |
  +--------------------------------+

The three result columns are identical, the formulas are pairwise equivalent, thus.

The Algebra of Truth Tables

Suppose, phi and psi are two formulas, and ttPhi and ttPsi are their truth tables,

  PropLogic> let ttPhi = truthTable phi
  PropLogic> let ttPsi = truthTable psi

We just instruced a couple of semantic notions for formulas by looking and comparing their truth tables. But we may as well abstract from the form of formulas and consider their truth table semantics right away. In other words, we say that a truth table is satisfiable (valid, contradictory) if it has some (or only, or no) 1 in its result column. And we can apply the same functions on truth tables as well, e.g.

  PropLogic> satisfiable ttPhi

Of course, we always have

  (satisfiable ttPhi) == (satisfiable phi)

And similarly, we adopt the semantic relations for truth tables, and the rule is, that

  (ttPhi `subvalent` ttPsi) == (phi `subvalent` psi)

Furthermore, we introduce the junctors on truth tables in the same fashion: there is a negation

  neg :: TruthTable a -> TruthTable a

which, of course, negates the boolean values in the result column of each table. And there is the conjunction conj, the disjunction disj, the subjunction subj and the equijunction equij that operate in harmony with the formula constructors CJ, DJ, SJ, and EJ, respectively, in the sense that e.g.

  conj [ttPhi, ttPsi] `equivalent` truthTable (CJ [phi, psi])

Propositional Algebras

For every atom type a, we now have a structure on PropForm a and a similar one on TruthTable a. We call such a structure a propositional algebra, the elements of a are the atoms, and the formulas or truth tables are the propositions. We define this abstract kind of structure as a type class in Haskell:

  PropAlg a p

is the type class for a propositional algebra on atom type a and proposition type p. And we already have two instances of this type class for every atom type a, namely

  PropAlg a (PropForm a)
  PropAlg a (TruthTable a)

The concept of a propositional algebra is the core concept of the whole package and the implementation of instances is the main achievement.

Components of a Propositional Algebra

A propositional algebra PropAlg a p on atoms a and propositions p comprises the following functions.

Formula conversions

Every instance of a propositional algebra has two functions to convert propositions to formulas, and backwards:

  toPropForm :: p -> PropForm a
  fromPropForm :: PropForm a -> p

On the formula algebra PropAlg a (PropForm a), these two functions are obviously the identity functions. On the truth table algebra PropAlg a (TruthTable a), the fromPropForm is just another name for

  truthTable :: PropForm a -> TruthTable a

Note however, that the use of fromPropForm requires a specification of the type. Haskell wouldn't know otherwise, to which kind of proposition we want to convert the formula. For example, a call of

  PropLogic> fromPropForm (EJ [A 'x', A 'y'])

returns an error message, but

  PropLogic> fromPropForm (EJ [A 'x', A 'y']) :: TruthTable Char

returns a TruthTable Char value.

The inverse function toPropForm on the other hand is the same as

  truthTableToDNF :: TruthTable a -> PropForm a

which turns a truth table into a Disjunctive Normal Form or DNF. For example,

  PropLogic> let tt = fromPropForm (EJ [A 'x', A 'y']) :: TruthTable Char
  PropLogic> display tt
  +---+---+-----------+
  | x | y | [x <-> y] |
  +---+---+-----------+
  | 0 | 0 |     1     |
  +---+---+-----------+
  | 0 | 1 |     0     |
  +---+---+-----------+
  | 1 | 0 |     0     |
  +---+---+-----------+
  | 1 | 1 |     1     |
  +---+---+-----------+
  PropLogic> let dnf = toPropForm tt
  PropLogic> display dnf
  [[-x * -y] + [x * y]]

You are probably familiar with DNFs (see below). And, as you probably expected, there is also a dual function that returns the Conjunctive Normal Forms

  PropLogic> display (truthTableToCNF tt)
  [[x + -y] * [-x + y]]

Semantic Functions

Most of the semantic properties and relations were explained earlier, but there are also some variations: covalence means that the arguments have at least one valuator in common that makes them true, disvalence is the opposite of covalence, and proper disvalence means disvalence and both arguments are satisfiable. Alltogether, the signature is

  valid           :: p -> Bool
  satisfiable     :: p -> Bool
  contradictory   :: p -> Bool
  subvalent       :: p -> p -> Bool
  equivalent      :: p -> p -> Bool
  covalent        :: p -> p -> Bool
  disvalent       :: p -> p -> Bool
  properSubvalent :: p -> p -> Bool
  properDisvalent :: p -> p -> Bool

The set of junctors is

  false :: p
  true  :: p
  neg   :: p -> p
  conj  :: [p] -> p
  disj  :: [p] -> p
  subj  :: [p] -> p
  equij :: [p] -> p

On the formula algebra PropAlg a (PropForm a), these junctor are the formula constructors themselves

  false = F   true = T   neg = N   conj = CJ   disj = DJ   subj = SJ   equij = EJ

On PropAlg a (TruthTable a), false and true are the two different nullatomic tables with either 0 or 1 in their result table. (Note, that there is one valuator for the empty atom set, namely the empty valuator [].)

We also need an atomic proposition constructor

  at :: a -> p

For formulas, this is again the atomic formula constructor at = A. The atomic truth table of say the atom 'x' is given by

  PropLogic> display (at 'x' :: TruthTable Char)
  +---+---+
  | x |   |
  +---+---+
  | 0 | 0 |
  +---+---+
  | 1 | 1 |
  +---+---+

Note, that we often need to type things for Haskell to indicate the instance we have in mind. For the previous example that means that an untyped call of say

  PropLogic> at 'x'

would issue an error message, because it is not clear, if the result is of type PropForm Char or TruthTable Char or any other instance.

Another algebraization of propositional logic

The previous operations alltogether define what we call the semantic structure of a propositional algebra, and that is the most often used aspect of propositional logic. In fact, this semantic part has an abstract counterpart, called boolean algebra, and it is common to reduce propositional logic to this semantic aspect. (A standard method to do so is the Lindenbaum-Tarski algebra, see e.g. [LTA].)

But our algebraization of propositional logic results in a kind of structure we call theory algebra. That is a specific combination of not just one, but two order structures, namely the semantic as well as the atomic (or syntactic) structure. (See [ThA].)

The Atomic Structure

First of all, there are three functions that return atom sets (i.e. ordered lists of atoms)

  atoms    :: p -> Olist a
  redAtoms :: p -> Olist a
  irrAtoms :: p -> Olist a

For example, if we put

  PropLogic> let phi = EJ [A "first", CJ [A "second", F], A "first"]
  PropLogic> display phi
  [first <-> [second * false] <-> first]

then we already now that atoms returns the atoms (here: Strings), that occur in the formula:

  PropLogic> atoms phi
  ["first","second"]

This atom set is further split into redundant and irredundant atoms:

  PropLogic> redAtoms phi
  ["second"]
  PropLogic> irrAtoms phi
  ["first"]

An atom is redundant in a formula, if there is an equivalent formula without that atom. In this given phi, "second" is redundant and an equivalent formula psi is e.g.

  PropLogic> let psi = N (A "first")
  PropLogic> psi `equivalent` phi
  True

Then, there is a whole variation of atomic properties and relations,

  nullatomic      :: p -> Bool
  subatomic       :: p -> p -> Bool
  equiatomic      :: p -> p -> Bool
  coatomic        :: p -> p -> Bool
  disatomic       :: p -> p -> Bool
  properSubatomic :: p -> p -> Bool
  properDisatomic :: p -> p -> Bool

As the names suggest, a proposition is nullatomic if it has not atoms. And if phi and psi are two propositions, then phi is subatomic to psi, i.e.

  PropLogic> phi `subatomic` psi
  True

if each atom in phi is also an atom in psi. phi and psi are said to be coatomic, if they have at least one common atom. Otherwise, they are disatomic. And proper disatomic means that they are disatomic, and none of them is nullatomic.

Atomic modifiers

The junctions always accumulate the atoms of their arguments, just as the formulas did. The conjunction (or disjunction etc.) of propositions contains all the atoms of the given propositions together. But we have no operation so far, that decreases the number of atoms again. Therefore, we define a couple of atomic modifiers.

Each modifier is of type p -> [a] -> p, i.e. it takes a proposition phi and a list of atoms [a1,...,aN] and it returns a new proposition psi, which should be equivalent to the intial one. The modifier is called a reduction, if psi has exactly the atoms [a1,...,aN]. It is an elimination if psi has the atoms from phi, but without the ones in [a1,...,aN]. And finally, it is an extension (or expansion), if the atoms of psi are the union of the ones in phi and [a1,...,aN].

The extension is the easiest of the modifications, because it always has a solution, i.e. for each phi and [a1,...,aN], there always is an equivalent psi with all the atoms of phi and [a1,...,aN].

An (atomic) extension (or expansion) takes a proposition and a list of atoms, and returns a proposition which is equivalent, but has these additional atoms. For formulas, this can be done in terms of formula constructors according to the rule

  ext phi [a1,...,aN] == CJ [phi, DJ [T, A a1, ..., A aN]]

Note, that the right hand of the equation is indeed equivalent to phi. This is indeed the chosen implementation. For example,

  PropLogic> ext (A 'y') ['x', 'z']
  CJ [A 'y',DJ [T,A 'x',A 'z']]

Reductions and eliminations are more difficult, because they often don't have a solution. Suppose, phi is the formula CJ [A 'x', A 'y', A 'z'] and we want to perform a reduction onto the atoms 'x', 'y'. That is impossible, because there is no formula psi with atoms psi == ['x', 'y'] and psi `equivalent` phi.

However, there always is a supremum (or least upper) and a infimum (or greatest lower) reduction. For example, the supremum reduction supRed phi [a1,...,aN] is the least of all formulas psi so that the a1,...,aN are the atoms of psi (with respect to the subvalence order relation).

Similarly, there is a supremum elimination and a infimum elimination and alltogether, there are five atomic modifiers in a propositional algebra:

  ext     :: p -> [a] -> p
  infRed  :: p -> [a] -> p
  supRed  :: p -> [a] -> p
  infElim :: p -> [a] -> p
  supElim :: p -> [a] -> p

The implementation of these modifiers is usually not a trivial operation and we won't go into the details here. For example

  PropLogic> let ttPhi = truthTable (SJ [A 'x', A 'y', A 'z'])
  PropLogic> display ttPhi
  +---+---+---+---------------+
  | x | y | z | [x -> y -> z] |
  +---+---+---+---------------+
  | 0 | 0 | 0 |       1       |
  +---+---+---+---------------+
  | 0 | 0 | 1 |       1       |
  +---+---+---+---------------+
  | 0 | 1 | 0 |       0       |
  +---+---+---+---------------+
  | 0 | 1 | 1 |       1       |
  +---+---+---+---------------+
  | 1 | 0 | 0 |       0       |
  +---+---+---+---------------+
  | 1 | 0 | 1 |       0       |
  +---+---+---+---------------+
  | 1 | 1 | 0 |       0       |
  +---+---+---+---------------+
  | 1 | 1 | 1 |       1       |
  +---+---+---+---------------+

  PropLogic> display (supElim ttPhi ['y'])
  +---+---+----------------------------------+
  | x | z | [[-x * -z] + [-x * z] + [x * z]] |
  +---+---+----------------------------------+
  | 0 | 0 |                1                 |
  +---+---+----------------------------------+
  | 0 | 1 |                1                 |
  +---+---+----------------------------------+
  | 1 | 0 |                0                 |
  +---+---+----------------------------------+
  | 1 | 1 |                1                 |
  +---+---+----------------------------------+

  PropLogic> display (infElim ttPhi ['y'])
  +---+---+----------------------------------+
  | x | z | [[x + z] * [-x + z] * [-x + -z]] |
  +---+---+----------------------------------+
  | 0 | 0 |                0                 |
  +---+---+----------------------------------+
  | 0 | 1 |                1                 |
  +---+---+----------------------------------+
  | 1 | 0 |                0                 |
  +---+---+----------------------------------+
  | 1 | 1 |                0                 |
  +---+---+----------------------------------+

Additional definitions

Two propositions are called biequivalent, iff they are both equivalent and equiatomic. In terms of Haskell

  p1 `biequivalent` p2  ==  (p1 `equivalent` p2) && (p1 `equiatomic` p2)

Biequivalence is the identity from a theory-algebraic point of view.

The last two functions that make up a propositional algebra PropAlg a p are two "meta properties" that generalize semantic and atomic properties P and relations R for lists of propositions. We say that such a list [q_1,...,q_n] is pointwise P, if P q is True for every q in the list. And it is pairwise R, if q_i R q_j holds for all 1 <= i < j <= n. In Haskell these meta properties are functions

  pointwise :: (p -> Bool) -> [p] -> Bool
  pairwise :: (p -> p -> Bool) -> [p] -> Bool

(Actually, pointwise is just a synonym for the Haskell built-in all.) For example,

  PropLogic> let pL = [A 'x', N (A 'y'), CJ [A 'x', A 'z']]
  PropLogic> :t pL
  pL :: [PropForm Char]
  PropLogic> pointwise satisfiable pL
  True
  PropLogic> pairwise disatomic pL
  False
  PropLogic> pairwise coatomic pL
  False

Summary

The overall signature of the PropAlg type class definition is given by

  class Ord a => PropAlg a p | p -> a where
    -- atomic proposition constructor
    at :: a -> p
    -- boolean junctors
    false :: p
    true :: p
    neg :: p -> p
    conj :: [p] -> p
    disj :: [p] -> p
    subj :: [p] -> p
    equij :: [p] -> p
    -- semantic properties and relations
    valid :: p -> Bool
    satisfiable :: p -> Bool
    contradictory :: p -> Bool
    subvalent :: p -> p -> Bool
    equivalent :: p -> p -> Bool
    covalent :: p -> p -> Bool
    disvalent :: p -> p -> Bool
    properSubvalent :: p -> p -> Bool
    properDisvalent :: p -> p -> Bool
    -- atom sets
    atoms :: p -> Olist a
    redAtoms :: p -> Olist a
    irrAtoms :: p -> Olist a
    -- atomic properties and relations
    nullatomic :: p -> Bool
    subatomic :: p -> p -> Bool
    equiatomic :: p -> p -> Bool
    coatomic :: p -> p -> Bool
    disatomic :: p -> p -> Bool
    properSubatomic :: p -> p -> Bool
    properDisatomic :: p -> p -> Bool
    -- atomic modifiers
    ext :: p -> [a] -> p
    infRed :: p -> [a] -> p
    supRed :: p -> [a] -> p
    infElim :: p -> [a] -> p
    supElim :: p -> [a] -> p
    -- biequivalence
    biequivalent :: p -> p -> Bool
    -- meta properties
    pointwise :: (p -> Bool) -> [p] -> Bool
    pairwise :: (p -> p -> Bool) -> [p] -> Bool
    -- formula conversions
    toPropForm :: p -> PropForm a
    fromPropForm :: PropForm a -> p

Other Parts of the Package

"Default" and "fast" instances and the modular character of the package

In fact, there are more than just the two default instances on formulas and truth tables

  PropAlg a (PropForm a)
  PropAlg a (TruthTable a)

We call them default, because their idea is straight forward and so is their implementation. But the problem with the default instances is that some representations and operations explode, and that makes them not feasible for other than small cases with only a few atoms involved. For example, a truth table on n atoms has 2^n valuators, and checking for subvalence the default way may be of exponential cost as well. Next to the default instances we therefore also provide a couple of fast propositional algebras as well, that aim to be feasible for arbitrary practical situations.

This whole approach is also apparent in the modular design of the package. The four important modules are:

                     PropLogicCore
                     /           \
                    /             \
                   /               \
     DefaultPropLogic              FastPropLogic
                  \                /
                   \              /
                    \            /
                     PropLogicTest

PropLogicCore basically comprises the definition for the PropForm a data type and the PropAlg a p type class. DefaultPropLogic provides the default implementations we discussed so far, but also default implementations of various normalizations. FastPropLogic implements a couple of fast instances for propositional algebras and PropLogicTest provides generators for the various different proposition types, methods to check the correctness and performance of propositional algebra instances.

All modules also come with built-in documentations (see [Doc]).

Normalizations, Canonizations and the Fast Instances of Propositional Algebras

The "fast" instances of Propositional Algebras

Links and Footnotes

[GHC]

http://www.haskell.org/ghc

points to the Glasgow Hakell Compiler.

[Inst]

http://www.bucephalus.org/text/InstallPropLogic/InstallPropLogic.html

describes the installation of the various requirements.

[LTA]

http://en.wikipedia.org/wiki/Lindenbaum-Tarski_algebra

the Wikipedia article on Lindenbaum-Tarski algebras.

[ThA]

http://www.bucephalus.org/text/TheoryAlgebras/TheoryAlgebras.html the guide to literature on Theory Algebras.

[Doc]

The Haskell modules all come with their own HTML documentation (see http://www.bucephalus.org/PropLogic).