Algebraic Semantics for the Logic of Proofs

TL;DR

This paper develops algebraic semantics for the classical logic of proofs using Boolean algebras, extending the language to incorporate Boolean structures on justification terms and equality, and proves completeness and representation theorems.

Contribution

It introduces a novel algebraic framework for the logic of proofs with Boolean structures and extends the language to unify proof terms and equality within this framework.

Findings

Established algebraic semantics based on Boolean algebras

Extended the language to include Boolean structure on justification terms

Proved completeness and generalized Stone's representation theorem

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.