This project aims to reconstruct the computability concept in terms of propositional algebras. Features of this approach:

- Everything is a propositional formula: a number, a function, a program, a list, etc. This is similar to the lambda calculus, where every concept of a programming language is encoded as a lambda expression.
- A concrete design depends on a concrete choice of a theoretificationism [1], which determines how a proposition turns into a function, and the other way round, how a set of argument-result pairs, i.e. how a binary theory relation is encoded as a proposition again.

The primitive operations, i.e. the whole underlying "virtual machine" is only made of the operations of propositional logic, and this system is effectively implemented [2]. However, it requires a paradigm shift in the reasoning about programming itself. Propositional logic as a whole is a NP-hard problem. And now, we propose our propositional logic system as the primitive base for a more complex programming language. This upside-down perspective has two justifications: our first goal was to show that our propositional machines we want to explore in the formal intelligence project can be run as Turing complete devices. In other words, we just required a mathematical proof that the computability concept is equivalently definable in propositional algebra. The second justification is very pragmatic: just let us see if actual programs run fast enough on a temporary computer system to be practical. Computer power nowadays is so inexpensive, that this practical proof is the only real issue in most cases.

The whole project is only rudimentary realized so far. Many encoding problems are solved and according algorithms are implemented in a Haskell package. But all that is too premature to be published.

- [1] http://www.bucephalus.org/text/Theisms/Theisms.html
- [2] http://www.bucephalus.org/text/PropLogicProject.html effective implementations of propositional logic