having relatively short formal proofs and the class NP

[David Bernier]

In a first-order logic formal theory of ZFC, suppose we have a sentence S
with n symbols, and we ask if S has a proof in m symbols or less.

According to some (at least) formulations of "formal proof",
the last line is the conclusion, or the thing to be proved.
Say we adopt that convention, so that necessarily n <= m .

Then if W is a string of symbols which is a proof of S,
and W has m symbols, n <= m.

"S has a proof with at most m symbols".

If it's true, the truth can be shown by exhibiting
a formal proof X with at most 'm' symbols.

If each line of a proof can be checked in time
polynomial in 'm', then the whole proof can be checked in time
polynomial in 'm'.

Assuming this is true, then
"S has a proof with at most m symbols" is in NP.

If P = NP, then

"S has a proof with at most m symbols" is in P .

But many quite short provable S won't have any
short proofs.

I don't think this helps with P=? NP.

David Bernier

[Gc]

True. I think then the P=NP algorithm should then be able to tell us
in polynomial time that there is no proof shorter than m for S, where |
S| = n and m depends somehow polynomially from n.