P vs. NP and Godel's Theorems
if P!=NP then this means that for some fixed $k$ not all true sentences $\phi$ of ZF have a proof of length ≤ $|ϕ|^k$.

You do not need to assume $P \neq NP$ to prove this claim. If all true sentences $\phi$ of ZF have a proof of length $\leq |\phi|^k$ then the halting problem could be solved by enumerating all proofs of &quot;$M$ is halting&quot; and &quot;$M$ is not halting&quot; up to that size. So it's not possible for all true sentences to have a short proof. Instead of  $|\phi|^k$ we can take a function that grows even faster, e.g. $2^{2^{2^{|\phi|}}}$. There's no computable limit on how long a proof can be compared to its statement.
However, to speak about true sentences, we are assuming implicitly that ZF already has a model. So this reasoning does not prove that ZF is consistent - it assumes it from the start. There's no contradiction between &quot;not all true statements have a short proof&quot; and &quot;all statements have a short proof&quot; if there are no true statements.