The Propositional Logic Project

October 2009

One core thesis of the whole "bucephalus approach" to logic is the idea that higher concepts like computability or intelligence could and should be reconstructed and formalized in propositional logic entirely [PL1]. Only, that the state of the subject called propositional logic in its common form is not suitable to fulfil this task.

The problem

Propositional logic sure has become a standard notion of our scientifically educated society, maybe as much as the arithmetic systems of integers, rational and real numbers. Boolean operations are standards in many areas of our computerized daily life, digital logic is the mathematical structure behind the computer hardware and information software.

But different to arithmetic systems and other basic data structures like lists, matrices or regular expressions, propositional algebras are not part of the standard tool repertoire of programming languages. This is certainly due to the cost explosion (see e.g. the boolean satisfiability problem [SAT]) of its default implementation. What we need, is a fast implementation, which allows these structures to be used as basic tools for other programs.

The other problem with propositional logic is its classic algebraization as a (free) boolean algebra [BA], which is only an abstraction of the semantic structure of propositional logic. That way, we loose some of the information. In other words, we need an algebraization that also preserves the syntactic structure of propositional worlds [E].

The solution

The algebraization of propositional logic, the definition of propositional algebra as a double quasi-boolean structure is called theory algebra. Meanwhile, there is also a generalization of these propositional theory algebras towards a theory algebras of relations, which provide an algebraization of predicate logic [ThA].

Fast implementations are now available in two flavors: There is the older Java applet [bucanon], usable as a kind of online pocket calculator for propositional logic. And there is the more recent Haskell package [PropLogic] with an abstract concept for (a theory-algebraic version of) "propositional algebra".

These systems are not based on the indeterministic inference rules of a propositional calculus, but rely on a single canonization, based on so-called Prime Normal Forms. The clear descriptive advantage of canonizations is that all traditional questions of propositional logic (Is φ satisfiable? Does φ ⇒ ψ hold? etc.) are answered with the same single function. The disadvantage however is the non-feasibility of these functions, at least when they are implemented in their naive or "default" way. However, there are also "fast" algorithms, emerging from a deeper study of the whole subject [PNFCanon].

Links and footnotes