The geometry of logic, algebra and computation

We present a research program relating Logic, Algebra and Computation through decomposition operators, Boolean algebras of dimension n and Boolean vector spaces.

First we introduce the notion of dimension in universal algebra. An algebra has dimension n if it admits a term operation q of arity n+1 and n constants p_1,…,p_n satisfying the fundamental properties of the n-ary if-then-else connective: q( p_i, x_1,…,x_n) = x_i for every i=1,…,n. The constants p_1,…,p_n, which act as n-ary projections, can be, for example, variables in free algebras or lambda calculus, a basis of a vector space, the truth values of a logic, or prime numbers in arithmetics.

Every algebra A of dimension n contains the n-dimensional Boolean algebra (nBA, for short) of its n-central elements. An element c is n-central if it satisfies the equations simultaneously satisfied by the projections p_1,…, p_n. This is equivalent to the requirement that the operator q(c,-,…,-) is a decomposition operator, so that c can decompose the algebra A as Cartesian product of n more simple factors. nBAs are a dimensional generalization of classical Boolean algebras (= 2BA). The classical algebraic structures of mathematics -including groups, rings, fields, Boolean algebras, etc. – are only the dimension 2 case of much richer algebraic world.

We show a representation theorem for nBAs: every nBA is the nBA of n-central elements of a suitable Boolean vector space. As a consequence, every algebra of dimension n can be linearly approximated by a Boolean vector space.

We apply this theory to Logic and Computation:

(1) We generalize two-valued classical propositional logic to n-valued classical propositional logic with a perfect symmetry among the n-truth values. As the Lindenbaum algebra of classical logic is a Boolean algebra, the Lindenbaum algebra of the classical n-valued logic is a Boolean algebra of dimension n. A sequent calculus with n different kinds of sequents (one for each dimension) is provided.

(2) We propose an algebraization of tabular classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables become logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.