Algebraic Semantics for the Logic of Proofs
Amir Farahmand Parsa, Meghdad Ghari
TL;DR
This work develops a richly algebraic treatment of the logic of proofs ${\mathsf{LP}}$. It first builds full ${\mathsf{LP}}_{\sf CS}$ algebras on Boolean bases with operators acting on formulas, proving completeness and a Stone-type representation; it then extends the framework to ${\mathsf{LP}^{B}}$ by equipping justification terms with a Boolean algebra and introducing an equality predicate, obtaining both completeness and bi-representation results. The theory is further advanced by treating ${\mathsf{LP}^{B}}$ over arbitrary term Boolean algebras and over polynomial Boolean algebras, with corresponding completeness and bi-representation theorems. Across these layers, the paper shows that ${\mathsf{LP}}$-type logics admit robust algebraic semantics, including set-algebra representations and bi-representations, while clarifying the role of internalization and representation in the algebraic setting.
Abstract
We present algebraic semantics for the classical logic of proofs based on Boolean algebras. We also extend the language of the logic of proofs in order to have a Boolean structure on justification terms and equality predicate on terms. In the end, the completeness theorem and certain generalizations of Stone's representation theorem are obtained for all proposed algebras.