Holography For Satisfiability I

A Boolean Satisfiability Proof Calculus

Abstract

 We present a meta-computational logic for Boolean Satisfiability that generalizes Holographic Algorithms to higher-dimensional logical manifolds. The logic is used to reason about both satisfiability and unsatisfiability proofs, as functions, which can be integrated and differentiated. We introduce twisted rings of proof integro-differential operators and a dualized algebra over these rings --- along with an algorithmic ultraproduct construction which unifies  an arbitrary number of such rings into a single, discrete topological ring, under bounded witness depth. The resulting framework expresses an algorithmic proof system which derives proofs, surprisingly,  in polynomial-time, with respect to the input size of a 3-SAT formula. As a by-result of these constructions, our framework offers a new descriptive complexity lens on the conflated class, NP ∪ CoNP, which is characterized by an algebraized Second-Order Logic with a Relative Least Fixed Point [A-SO-RLFP] that, in its implications, challenges the Church-Turing thesis, and our current understanding of the class of computable functions.