2023/04/02 by Monroe, Hunter
#Computational Complexity (cs.CC) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.2304.00610
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,1t⟩| 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.