Ruling Out Short Proofs of Unprovable Sentences is Hard
share
If no optimal propositional proof system exists, we (and independently Pudlák) prove that ruling out length t proofs of any unprovable sentence is hard. This mapping from unprovable to hard-to-prove sentences powerfully translates facts about noncomputability into complexity theory. For instance, because proving string x is Kolmogorov random (x∈R) is typically impossible, it is typically hard to prove "no length t proof shows x∈R", or tautologies encoding this. Therefore, a proof system with one family of hard tautologies has these densely in an enumeration of families. The assumption also implies that a natural language is NP-intermediate: with R redefined to have a sparse complement, the complement of the language {⟨ x,1^t⟩| no length t proof exists of x∈R} is also sparse. Efficiently ruling out length t proofs of x∈R might violate the constraint on using the fact of x∈R's unprovability. We conjecture: any computable predicate on R that might be used in if-then statements (or case-based proofs) does no better than branching at random, because R appears random by any effective test. This constraint could also inhibit the usefulness in circuits and propositional proofs of NOT gates and cancellation – needed to encode if-then statements. If R defeats if-then logic, exhaustive search is necessary.
READ FULL TEXT