A theorem on Cook's conjecture

[martdowd at aol.com]

FOM:

After my unsuccessful attempts to use propositional diagonalization to
construct hard tautologies, I have come to the conclusion that this may
not be possible.  It seems that the tautologies of Cook's conjecture
are the best known conjectural hard tautologies for EF.  Constructing
more fundamental ones remains an elusive problem.  I wrote up a
discussion of the subject, in the course of which I discovered a new
theorem about Cook's conjecture.

I switched to writing this up, resulting in the manuscript
 A Theorem on Cook's Conjecture
 https://www.researchgate.net/publication/363611615

Abstract:
In 1975 Cook conjectured that the representing formulas of the consistency
of PV do not have polynomially bounded extended resolution proofs.
In 2020 the author noted that it is a question of interest, even whether
it is provable in PV from $\Con_{\text PV}$ that such proofs exist.
Here, a conjecture about PV is made, and it is shown that it implies that
this latter question has a negative answer.

Conjecture:
Let $(1)$ be the statement, for any $\LA$ functions $H_j(x)$,
 $\not\vdash\wedge_j\neg\Pi_0(H_j(x))=\bot\Ra w\leq_L x\Ra\neg\Pi_0(w)=\bot$.
Then $(1)$ is true.

($\LA$ is polynomial time arithmetic, $\vdash$ means provable in $\LA$,
$w\leq_L x$ means $|w|\leq |x|$, and $\bot$ is the numeral for the Godel
number of 0=1.)

Theorem:
Let $(2)$ be the statement, for any $\LA$ functions $G$,
$\Con_{\LA}\not\vdash \EF(G(x)) =\Rep_{\Con_{\LA}}(x)$.
Then $(1)$ implies $(2)$.

Martin Dowd

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220916/e53e2d26/attachment-0001.html>