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 within a provably non-Turing model of computation, 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 u 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.