Paper detail

Hoops, Coops and the Algebraic Semantics of Continuous Logic

Büchi and Owen studied algebraic structures called hoops. Hoops provide a natural algebraic semantics for a class of substructural logics that we think of as intuitionistic analogues of the widely studied Łukasiewicz logics. Ben Yaacov extended Łukasiewicz logic to get what is called continuous logic by adding a halving operator. In this paper, we define the notion of continuous hoop, or coop for short, and show that coops provide a natural algebraic semantics for continuous logic. We characterise the simple and subdirectly irreducible coops and investigate the decision problem for various theories of coops. In passing, we give a new proof that hoops form a variety by giving an algorithm that converts a proof in intuitionistic Łukaseiwicz logic into a chain of equations.