Bilattice Logic Properly Displayed

TL;DR

This paper presents a new multi-type display calculus for bilattice logic with conflation, establishing key proof-theoretic properties and leveraging bilattice product representations.

Contribution

It introduces a proper display calculus for bilattice logic with conflation, demonstrating soundness, completeness, and cut-elimination based on a novel multi-type approach.

Findings

Proves soundness and completeness of the calculus.

Establishes cut-elimination and subformula property.

Utilizes bilattice product representation in calculus design.

Abstract

We introduce a proper multi-type display calculus for bilattice logic (with conflation) for which we prove soundness, completeness, conservativity, standard subformula property and cut-elimination. Our proposal builds on the product representation of bilattices and applies the guidelines of the multi-type methodology in the design of display calculi.