How does one decide whether a theorem is qualitatively complex rather than hard?
Namely, how does one know when the proof of the theorem is irreducibly complex up to the least amount of computational steps required for a theorem's proof to Q.E.D.
Asked
Active
Viewed 70 times
1 Answers
0
Proof complexity is mainly studied for propositional calculus. To extend the notion to typical "real" math theorems that require the expressiveness of first-order logic, you could define the complexity of a theorem to be the number of steps in its shortest natural deduction proof.
I don't think there's a practical way to compute this, though; you'll essentially have to just enumerate all possible proofs in order of length, checking to see if they prove the given sentence. If you don't already know that the given sentence (or its negation) is provable (i.e. that the sentence is not independent), there's no way to know when to stop searching.
More precisely, there's no computable function $L$ from strings to numbers such that whenever $\varphi$ is provable, $L(\varphi)$ is an upper bound on the length of the shortest proof of $\varphi$. If there were, then we could solve the halting problem by letting $\varphi$ be the statement that a given program halts and then checking all possible proofs up to length $L(\varphi)$ to see if $\varphi$ is provable.
In other words, as we consider longer and longer sentences, we encounter theorems that require "very long" proofs: any upper bound on proof complexity grows faster than any computable function.
Karl
- 11,446
-
Not necessarily, if the theorem proof complexity is irreducible, then the alphabet is least onerous and least amount of use of primitives. Yes? I think it's not that far from ascertaining the least possible use of primitives and length of the theorem to make sure that the Kolmogorov complexity is the least great out of any other for a theorem. Why doesn't a function such as L exist, Sir? I'm under the impression that one can exist that is least complex in length, and primitives. – Shawn W. Mar 19 '21 at 21:38
-
Kolmogorov complexity is somewhat different from proof complexity, but it's also not computable. A brute-force program that outputs the shortest proof of an input sentence is easy to write, but it will necessarily run forever on certain inputs; there's no computable way to know when to stop searching. – Karl Mar 23 '21 at 04:28
Therefore, is it possible for a proof to be irreducibly complex in a manner of quantifying the complexity mentioned above to take the least amount of time to compute?
– Shawn W. Mar 19 '21 at 18:07