On Pocrims and Hoops

TL;DR

This paper explores algebraic structures called pocrims and hoops, providing new proofs and identities, and investigates their role in semantics of double negation translations in logic.

Contribution

It introduces a new proof that hoops form a variety and develops an algebraic framework for double negation translations, advancing the algebraic understanding of these logical concepts.

Findings

Hoops form a variety, proven via a new proof.

Double negation mapping in hoops is a homomorphism.

New algebraic results on the applicability of Gentzen and Glivenko translations.

Abstract

Pocrims and suitable specialisations thereof are structures that provide the natural algebraic semantics for a minimal affine logic and its extensions. Hoops comprise a special class of pocrims that provide algebraic semantics for what we view as an intuitionistic analogue of the classical multi-valued {\L}ukasiewicz logic. We present some contributions to the theory of these algebraic structures. We give a new proof that the class of hoops is a variety. We use a new indirect method to establish several important identities in the theory of hoops: in particular, we prove that the double negation mapping in a hoop is a homormorphism. This leads to an investigation of algebraic analogues of the various double negation translations that are well-known from proof theory. We give an algebraic framework for studying the semantics of double negation translations and use it to prove new results about the applicability of the double negation translations due to Gentzen and Glivenko.