Subreflexive Logic: Completeness without Identity
2026-07-27 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study a version of logic that doesn't assume a statement implies itself (no identity rule), called subreflexive logic. They show this logic has clear rules that are both sound and complete, meaning it works well mathematically. The paper introduces new algebraic structures and category theory tools that help model this logic without accidentally bringing back the usual identity assumption. They also prove that their logic can be simplified by removing unnecessary steps, and they confirm that it works with certain interpretations of implication in classical logic.
substructural logicidentity principlesubreflexive logiccut eliminationHeyting algebraBoolean algebrasemi-algebrassemi-categoriessoundnesscompleteness
Authors
Noah Abou El Wafa, André Platzer
Abstract
This paper shows that the substructural logic without the identity principle A->A (i.e., subreflexive logic) has principled sound and complete semantics and supports a variety of applications. This decidable generalization of propositional logic naturally interprets implication as robust consequence. Subreflexive logic is proved to admit syntactic cut elimination. Heyting and Boolean semialgebras are introduced as generalizations of Heyting and Boolean algebras and are shown to provide complete algebraic semantics without inadvertently reintroducing reflexivity. Semi-adjunctions on semi-categories and (identity-free) (co-)units are defined to give complete semi-categorical semantics. In the classical case, denotational set semantics that interpret implication as robust material implication are proved complete for subreflexive logic.