Proof-system domination by conservative extensions conjecture

About 4 years old · traced to

Let QQ be a propositional proof system. A theory T\mathcal{T} is a conservative extension of a base theory when it extends that theory without proving any new sentences in the base theory’s original language. Conservative-extension domination conjecture. For every propositional proof system QQ, there is a conservative extension T\mathcal{T} of ZFC or PA that outperforms QQ in proving tautologies. Moreover, adjoining an undecidable statement as a new axiom to T\mathcal{T} to form a conservative extension T′\mathcal{T}' further improves T\mathcal{T} in proving tautologies. The conjecture connects the nonexistence of optimal propositional proof systems with undecidability and the effect of adding axioms, but the source provides no resolution.

References

Primary source

Hunter Monroe, “Average-Case Hardness of Proving Tautologies and Theorems”, arXiv:2205.07803 (2022).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.