Let $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.