bucephalus.org

The Propositional Logic Project

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

• [PL1] I am under the impression, that even predicate logic can be embedded into propositional logic, turning the original hierarchy upside down. And I am not thinking of the "Herbrand" method that takes all primitive relation expressions as propositional atoms, but of a really finite structures.
• [SAT] see e.g. the wikipedia entry on the boolean satisfiability problem (en.wikipedia.org/wiki/Boolean_satisfiability_problem)
• [BA] see e.g. the wikipedia entry on free boolean algebras (en.wikipedia.org/wiki/Free_boolean_algebra)
• [ThA] TheoryAlgebras.html is the guide to the literature on theory algebras.
• [E] To give an impression of this lost information, let us consider the "propositional world" represented by the propositional formula

  φ := (female → ¬male) ∧ (male → ¬female) ∧ (car ∨ ¬car)

  φ is equivalent to the formula

  ψ := female ↔ male

  i.e. from a purely semantic point of view, φ and ψ denote the same world. But the syntax, the "language" of φ is richer than that of ψ, it has an additional atom car. From this syntactical point of view, ψ is a substructure of φ.
  We see the difference of the two worlds also when we take truth tables as the alternative representation. The two tables of φ and ψ are certainly different.

  car female male φ 0 0 0 0 1 0 0 0 0 1 0 1 1 1 0 1 0 0 1 1 1 0 1 1 0 1 1 0 1 1 1 0

  female male ψ 0 0 0 1 0 1 0 1 1 1 1 0

  This demonstrates, that the syntactic information is lost when propositional logic is abstracted into a boolean algebra. But isn't that information really redundant? Well, for many applications it is and to demonstrate the relevance of the theory-algebraic reconstraction is beyond the scope of this text. (But to give two examples anyway, check out The theory-algebraic semantics of predicate logic and Theoretificationisms.)

  [bucanon] see the online applet and the list of docs.

  [PropLogic] http://www.bucephalus.org/PropLogic

  [PNFCanon] The paper called Theory and implementation of efficient canonical systems for sentential calculus, based on Prime Normal Forms develops a system of "fast" algorithms.

  [home] [blog]