Abstract

Recently an expansion of Ł∏ logic with fixed points has been considered [23]. In the present work we study the algebraic semantics of this logic, namely μŁΠ algebras, from algebraic, model theoretic and computational standpoints. We provide a characterisation of free μŁΠ algebras as a family of particular functions from [0,1]n to [0,1]. We show that the first-order theory of linearly ordered μŁΠ algebras enjoys quantifier elimination, being, more precisely, the model completion of the theory of linearly ordered Ł∏ algebras. Furthermore, we give a functional representation of any Ł∏ algebra in the style of Di Nola Theorem for MV-algebras and finally we prove that the equational theory of μŁΠ algebras is in PSPACE