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.
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 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].
φ := (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 φ
.
φ
and ψ
are certainly different.
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.)
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
- [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]