ECCC-Report TR10-054https://eccc.weizmann.ac.il/report/2010/054Comments and Revisions published for TR10-054en-usTue, 30 Mar 2010 17:30:46 +0300
Paper TR10-054
| On the proof complexity of the Nisan-Wigderson generator based on a hard $NP \cap coNP$ function |
Jan Krajicek
https://eccc.weizmann.ac.il/report/2010/054Let $g$ be a map defined as the Nisan-Wigderson generator
but based on an $NP \cap coNP$-function $f$. Any string $b$ outside the range of
$g$ determines a propositional tautology $\tau(g)_b$ expressing this
fact. Razborov \cite{Raz03} has conjectured that if $f$ is hard on average for
P/poly then these tautologies have no polynomial size proofs in the
Extended Frege system EF.
We consider a more general Statement (S) that the tautologies have no polynomial
size proofs in any propositional proof system. This is equivalent to the
statement that the complement of the range of $g$ contains no infinite
NP set.
We prove that Statement (S) is consistent with Cook' s theory PV and,
in fact, with the true universal theory $\tpv$ in the language of PV.
If PV in this consistency statement could be extended to "a bit" stronger theory
(properly included in Buss's theory
$S^1_2$) then Razborov's conjecture would follow, and if it
$\tpv$ could be added too then Statement (S) would
follow.
We discuss this problem in some detail, pointing out a certain
form of reflection principle for propositional logic, and we introduce
a related feasible disjunction property
of proof systems.
Tue, 30 Mar 2010 17:30:46 +0300https://eccc.weizmann.ac.il/report/2010/054