$P\ne NP$ is a $\Pi^0_2$ statement:

for each polynomial-time Turing machine $M$ implementing an algorithm attempting to decide SAT, there is a formula $\phi_M$ on which it fails.

If we place a computable bound on the size of $\phi_M$ as a function of $M$ then we can improve this to a $\Pi^0_1$ statement, and hence will have the property $\text{undecidable}\rightarrow\text{true}$, since true $\Sigma^0_1$ statements are provable (in Peano Arithmetic). Of course in a formal sense, any provable statement is equivalent to $0=0$ which is $\Pi^0_1$.

Is it plausible that that $P\ne NP$, but there is no computable bound on $|\phi_M|$? This would mean that there are algorithms that do "arbitrarily well" at solving SAT in polynomial time. That is, relative to their description, they are correct for an Ackermann-function or busy-beaver-function level many $\phi$'s.

But intuitively, there is not much structure in SAT to exploit, and so once you have so many variables $x_1,\ldots,x_v$ that a random assignment of truth values has higher Kolmogorov complexity than $M$: $$K(M)\le v + O(1) $$ then there ought to be a $\phi(x_1,\ldots,x_m)$ on which $M$ fails. Since $K(M)$ has a computable bound as a function of $M$, it would follow that $M\mapsto |\phi_M|$ is computably bounded. This is probably off by a "factor" somewhere; maybe a better way is to say that $P^A\ne NP^A$ for a random oracle $A$, and in that case $\phi_M$ is computably bounded.

So we can make a plausible "computably bounded $P\ne NP$ conjecture" that $M\mapsto \phi_M$ is computably bounded (with a specific bound being incorporated into the conjecture), which does have the property $\text{undecidable}\rightarrow\text{true}$.

$P\ne NP$ is a $\Pi^0_2$ statement:

for each polynomial $p$ and Turing machine $M$ implementing an algorithm attempting to decide SAT, there is a formula $\phi_M$ such that if we look at the computation of $M$ on input $\phi_M$ after $p(|\phi_M|)$ computation steps, $M$ has either not halted or it has answered incorrectly.

(Edit: added more detail to the $\Pi^0_2$ statement above.)

If we place a computable bound on the size of $\phi_M$ as a function of $M$ then we can improve this to a $\Pi^0_1$ statement, and hence will have the property $\text{undecidable}\rightarrow\text{true}$, since true $\Sigma^0_1$ statements are provable (in Peano Arithmetic). Of course in a formal sense, any provable statement is equivalent to $0=0$ which is $\Pi^0_1$.

Is it plausible that that $P\ne NP$, but there is no computable bound on $|\phi_M|$? This would mean that there are algorithms that do "arbitrarily well" at solving SAT in polynomial time. That is, relative to their description, they are correct for an Ackermann-function or busy-beaver-function level many $\phi$'s.

But intuitively, there is not much structure in SAT to exploit, and so once you have so many variables $x_1,\ldots,x_v$ that a random assignment of truth values has higher Kolmogorov complexity than $M$: $$K(M)\le v + O(1) $$ then there ought to be a $\phi(x_1,\ldots,x_m)$ on which $M$ fails. Since $K(M)$ has a computable bound as a function of $M$, it would follow that $M\mapsto |\phi_M|$ is computably bounded. This is probably off by a "factor" somewhere; maybe a better way is to say that $P^A\ne NP^A$ for a random oracle $A$, and in that case $\phi_M$ is computably bounded.

So we can make a plausible "computably bounded $P\ne NP$ conjecture" that $M\mapsto \phi_M$ is computably bounded (with a specific bound being incorporated into the conjecture), which does have the property $\text{undecidable}\rightarrow\text{true}$.

$P\ne NP$ is a $\Pi^0_2$ statement:

for each polynomial-time Turing machine $M$ implementing an algorithm attempting to decide SAT, there is a formula $\phi_M$ on which it fails.

If we place a computable bound on the size of $\phi_M$ as a function of $M$ then we can improve this to a $\Pi^0_1$ statement, and hence will have the property $\text{undecidable}\rightarrow\text{true}$, since true $\Sigma^0_1$ statements are provable (in Peano Arithmetic). Of course in a formal sense, any provable statement is equivalent to $0=0$ which is $\Pi^0_1$.

Is it plausible that that $P\ne NP$, but there is no computable bound on $|\phi_M|$? This would mean that there are algorithms that do "arbitrarily well" at solving SAT in polynomial time. That is, relative to their description, they are correct for an Ackermann-function or busy-beaver-function level many $\phi$'s.

But intuitively, there is not much structure in SAT to exploit, and so once you have so many variables $x_1,\ldots,x_v$ that a random assignment of truth values has higher Kolmogorov complexity than $M$: $$K(M)\le v + O(1) $$ then there ought to be a $\phi(x_1,\ldots,x_m)$ on which $M$ fails. Since $K(M)$ has a computable bound as a function of $M$, it would follow that $M\mapsto |\phi_M|$ is computably bounded. [Caveat: This is probably off by a "factor" somewhere.]

So we can make a plausible "computably bounded $P\ne NP$ conjecture" that $M\mapsto \phi_M$ is computably bounded (with a specific bound being incorporated into the conjecture), which does have the property $\text{undecidable}\rightarrow\text{true}$.

$P\ne NP$ is a $\Pi^0_2$ statement:

for each polynomial-time Turing machine $M$ implementing an algorithm attempting to decide SAT, there is a formula $\phi_M$ on which it fails.

If we place a computable bound on the size of $\phi_M$ as a function of $M$ then we can improve this to a $\Pi^0_1$ statement, and hence will have the property $\text{undecidable}\rightarrow\text{true}$, since true $\Sigma^0_1$ statements are provable (in Peano Arithmetic). Of course in a formal sense, any provable statement is equivalent to $0=0$ which is $\Pi^0_1$.

Is it plausible that that $P\ne NP$, but there is no computable bound on $|\phi_M|$? This would mean that there are algorithms that do "arbitrarily well" at solving SAT in polynomial time. That is, relative to their description, they are correct for an Ackermann-function or busy-beaver-function level many $\phi$'s.

But intuitively, there is not much structure in SAT to exploit, and so once you have so many variables $x_1,\ldots,x_v$ that a random assignment of truth values has higher Kolmogorov complexity than $M$: $$K(M)\le v + O(1) $$ then there ought to be a $\phi(x_1,\ldots,x_m)$ on which $M$ fails. Since $K(M)$ has a computable bound as a function of $M$, it would follow that $M\mapsto |\phi_M|$ is computably bounded. This is probably off by a "factor" somewhere; maybe a better way is to say that $P^A\ne NP^A$ for a random oracle $A$, and in that case $\phi_M$ is computably bounded.

So we can make a plausible "computably bounded $P\ne NP$ conjecture" that $M\mapsto \phi_M$ is computably bounded (with a specific bound being incorporated into the conjecture), which does have the property $\text{undecidable}\rightarrow\text{true}$.