On the complexity of finding falsifying assignments for Herbrand disjunctions

DOI10.1007/S00153-015-0439-6MaRDI QIDQ892133zbMATH OpenOpenAlexFDO

Publication date 18 November 2015

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

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

falsifying assignment Herbrand theorem polynomial search problem

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

Abstract: Suppose that

P h i

is a consistent sentence. Then there is no Herbrand proof of

e g P h i

, which means that any Herbrand disjunction made from the prenex form of

e g P h i

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

P h i

such that finding solutions to

R

can be reduced to finding a falsifying assignment to an Herbrand disjunction made from

e g P h i

. It has been conjectured that there are no complete total polynomial search problems. If this conjecture is true, then for every consistent sentence

P h i

, there exists a consistence sentence

P s i

, such that the search problem associated with

P s i

cannot be reduced to the search problem associated with

P h i

.

Recommendations

Cites work

Cited in

(10)

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)