An algebraic presentation of predicate logic (extended abstract)

Abstract

We present an algebraic theory for a fragment of predicate logic. The fragment has disjunction, existential quantification and equality. It is not an algebraic theory in the classical sense, but rather within a new framework that we call 'parameterized algebraic theories'. We demonstrate the relevance of this algebraic presentation to computer science by identifying a programming language in which every type carries a model of the algebraic theory. The result is a simple functional logic programming language. We provide a syntax-free representation theorem which places terms in bijection with sieves, a concept from category theory. We study presentation-invariance for general parameterized algebraic theories by providing a theory of clones. We show that parameterized algebraic theories characterize a class of enriched monads. © 2013 Springer-Verlag.