I don’t think so. There are only O(k^N) strings of length N. It would be very strange if there were only finitely many true claims about the integers.
Here is a proposed proof sketch, by the way.
Suppose for contradiction that there were some N such that all true claims about natural numbers had proofs of length less than N. Necessarily, there is a least such N, call it N’, for which that’s true. Take P as some proposition with a proof of length N’. Take P2 as some other proposition. The proof of (P and P’) is going to have length longer than N’, since it has to include P as a subproof and at least one additional line for P and P’.
This violates our assumption, QED.
P and P’ doesn’t seem like a very interesting proposition, but I don’t know a way to formalize “interesting”. I think there are probably are only finitely many claims that a finite mathematical mind can possibly find interesting.
Pretty sure this can’t happen. We stipulated that we had the shortest proof for P. How did P and P’ get proved without proving P first? Or alternatively, without there being a shorter proof available for P without P’?
What if P = “The prime numbers are infinite or there are exactly 1337 of them” and P’ = “There are not exactly 1337 prime numbers.”
The shortest way to prove P involves proving (P and P’), which is the statement “The prime numbers are infinite.” It would take a roundabout argument indeed to exclude all finite cardinalities besides 1337, without also excluding 1337 and accidentally proving (P and P’).
I don’t have an example to hand. I just have a feeling that there might be some case where the shortest proof of (P and P’) is a component of the shortest proof of P, rather than the other way around.
I don’t think so. There are only O(k^N) strings of length N. It would be very strange if there were only finitely many true claims about the integers.
Here is a proposed proof sketch, by the way. Suppose for contradiction that there were some N such that all true claims about natural numbers had proofs of length less than N. Necessarily, there is a least such N, call it N’, for which that’s true. Take P as some proposition with a proof of length N’. Take P2 as some other proposition. The proof of (P and P’) is going to have length longer than N’, since it has to include P as a subproof and at least one additional line for P and P’.
This violates our assumption, QED.
P and P’ doesn’t seem like a very interesting proposition, but I don’t know a way to formalize “interesting”. I think there are probably are only finitely many claims that a finite mathematical mind can possibly find interesting.
I don’t think this necessarily follows. Suppose the last few lines of the proof of P read something like:
Pretty sure this can’t happen. We stipulated that we had the shortest proof for P. How did P and P’ get proved without proving P first? Or alternatively, without there being a shorter proof available for P without P’?
What if P = “The prime numbers are infinite or there are exactly 1337 of them” and P’ = “There are not exactly 1337 prime numbers.”
The shortest way to prove P involves proving (P and P’), which is the statement “The prime numbers are infinite.” It would take a roundabout argument indeed to exclude all finite cardinalities besides 1337, without also excluding 1337 and accidentally proving (P and P’).
I don’t have an example to hand. I just have a feeling that there might be some case where the shortest proof of (P and P’) is a component of the shortest proof of P, rather than the other way around.