Self-reference and solution independence are central to hard combinatorial instances. We ask whether Boolean \(K\)-SAT can exhibit both, giving a finite propositional analogue of Gödel's incompleteness theorems. Solution independence is formalized via factorial moments of the satisfying-assignment count. Constant-width random \(K\)-SAT fails: overlapping assignments create correlations and exponential second moment. We use a random CNF ensemble with logarithmic width \(K=O(\log N)\) at the subcube-covering threshold \(M=Θ(N^{2+\varepsilon})\). There it converges to Poisson, so unsatisfiable and uniquely satisfiable formulas coexist. Using the unique solution, a single-clause replacement yields a SAT/UNSAT pair sharing the same unsigned incidence graph. We prove structural irreducibility: every local subinstance of size at most \(N^c\), \(0<c<1\), has identical local views, so no deterministic or bounded-error clause-query evaluator at that scale can distinguish unique satisfiability from unsatisfiability. This is a finite self-referential construction, not itself a time-complexity lower bound. We quantify the local--global gap: any transcript of \(t=N^{1-δ}\) queries leaves \(N-o(N)\) bits of witness entropy. Expansion preservation plus size--width, size--degree, and pseudoexpectation trade-offs gives linear Resolution width, linear PC/PCR and SOS degree, and exponential proof size for the unsatisfiable companions; analogous bounds hold for semantic Cutting Planes and restricted Positivstellensatz. These bounds are uniform over support-preserving signings, even after observing the unique solution. These \(2^{Ω(N)}\) proof-size lower bounds are consistent with SETH, suggesting SETH is a finite projection of Gödel incompleteness onto resource-bounded computation. The hardness is quantum-invariant and limits local statistical learning.

翻译：暂无翻译