Hoops, Coops and the Algebraic Semantics of Continuous Logic

TL;DR

This paper introduces continuous hoops (coops), algebraic structures that provide semantics for continuous logic, extending the theory of hoops and exploring their properties and decision problems.

Contribution

It defines continuous hoops, characterizes their simple and irreducible forms, and connects them to continuous logic, offering new insights and algorithms for their algebraic properties.

Findings

Coops provide a natural algebraic semantics for continuous logic.

Characterization of simple and subdirectly irreducible coops.

An algorithm to convert intuitionistic Łukasiewicz logic proofs into equations.

Abstract

B\"{u}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 {\L}ukasiewicz logics. Ben Yaacov extended {\L}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 {\L}ukaseiwicz logic into a chain of equations.