Generalising Equational Logic

The fundamental result from which categorical logic sprang in the 1960’s is an equivalence between the category theoretic notion of Lawvere theory and the logical notion of equational theory. The notion of Lawvere theory was also seen to be equivalent to that of finitary monad on the category Set.

The definition of finitary monad immediately makes sense on a wide variety of categories other than Set, in particular (subject to a mild extension from finiteness to countability) on the category of omega-cpo’s, which has been fundamental to the study of denotational semantics. So one wonders whether the ideas of Lawvere theory and equational theory can be extended in a way that one can readily use in practice and that extends the above equivalences.

In fact, over recent years, the definition of Lawvere theory has been extended in a numbers of ways that retain the equivalence with monads and do indeed play a helpful role in denotational semantics, in particular in regard to modelling computational effects that appear in otherwise functional languages, such being for example side-effects and exceptions in ML.

But what about extending the definition of equational theory? An answer is not entirely straightforward. The key problem is the notion of arity: in ordinary equational theories, each operation has an arity given by a natural number. Extending that to account for countability is routine. But for an axiomatic treatment, the most immediate natural notion of arity has more complex structure than that of a natural number, and that plays havoc with the ideas of composite operation and equation between composite operations.

I believe that is now resolvable by focusing on what are called discrete Lawvere theories. The proposal is to see this idea through to resolution.