(Dual) Hoops Have Unique Halving

TL;DR

This paper explores the extension of continuous logic with a halving operator, using algebraic structures called hoops, and highlights the role of automated theorem proving in establishing key algebraic laws.

Contribution

It introduces a new logical extension with a halving operator and connects it to algebraic structures called hoops, advancing the theoretical understanding of continuous logic.

Findings

Prover9 successfully proved an important algebraic law.

The semantics of the extended logic are based on specialized hoops.

The extension aims to improve the model theory for continuous structures.

Abstract

Continuous logic extends the multi-valued Lukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The semantics of these logics can be given using specialisations of algebraic structures known as hoops. As part of an investigation into the metatheory of propositional continuous logic, we were indebted to Prover9 for finding a proof of an important algebraic law.