On the complexity of finding falsifying assignments for Herbrand disjunctions

DOI10.1007/S00153-015-0439-6zbMATH Open1378.03043arXiv1411.3304OpenAlexW1530232604MaRDI QIDQ892133FDOQ892133

Pavel Pudlák

Publication date: 18 November 2015

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Abstract: Suppose that $Phi$ is a consistent sentence. Then there is no Herbrand proof of $egPhi$, which means that any Herbrand disjunction made from the prenex form of $egPhi$ is falsifiable. We show that the problem of finding such a falsifying assignment is hard in the following sense. For every total polynomial search problem $R$, there exists a consistent $Phi$ such that finding solutions to $R$ can be reduced to finding a falsifying assignment to an Herbrand disjunction made from $egPhi$. It has been conjectured that there are no complete total polynomial search problems. If this conjecture is true, then for every consistent sentence $Phi$, there exists a consistence sentence $Psi$, such that the search problem associated with $Psi$ cannot be reduced to the search problem associated with $Phi$.

Full work available at URL: https://arxiv.org/abs/1411.3304

zbMATH Keywords

falsifying assignmentHerbrand theorempolynomial search problem

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20) Complexity of computation (including implicit computational complexity) (03D15)

Cites Work

• Title not available (Why is that?)
• How easy is local search?
• The provably total search problems of bounded arithmetic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic
• Logical Foundations of Mathematics and Computational Complexity

Cited In (9)

• Towards a unified complexity theory of total functions
• The classes PPA-\(k\): existence from arguments modulo \(k\)
• TFNP: An Update
• Towards a Unified Complexity Theory of Total Functions
• INCOMPLETENESS IN THE FINITE DOMAIN
• Using binary patterns for counting falsifying assignments of conjunctive forms
• NEW RELATIONS AND SEPARATIONS OF CONJECTURES ABOUT INCOMPLETENESS IN THE FINITE DOMAIN
• Note on constrained long choice with multiple beginning elements
• The classes PPA-\(k\): existence from arguments modulo \(k\)

This page was built for publication: On the complexity of finding falsifying assignments for Herbrand disjunctions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q892133)