Interpolation and Quantifiers in Ortholattices

TL;DR

This paper investigates the properties of quantifiers and interpolation in orthologic, a non-distributive logic, providing a proof system, showing the existence of interpolants, and offering an efficient algorithm for their computation.

Contribution

It introduces a sequent-based proof system for quantified orthologic, proves its soundness and completeness, and presents an algorithm for computing interpolants efficiently.

Findings

Orthologic does not admit quantifier elimination in general.

Interpolants always exist in orthologic.

An efficient algorithm for interpolant computation is provided.

Abstract

We study quantifiers and interpolation properties in \emph{orthologic}, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based proof system for quantified orthologic, which we prove sound and complete for the class of all complete ortholattices. We show that orthologic does not admit quantifier elimination in general. Despite that, we show that interpolants always exist in orthologic. We give an algorithm to compute interpolants efficiently. We expect our result to be useful to quickly establish unreachability as a component of verification algorithms.