V.Arvind, J.Köbler, M.Mundhenk, J.Torán:
Nondeterministic instance complexity and hard-to-prove tautologies

Appeared in: Symposium on Theoretical Aspects of Computer Science 2000. Lecture Notes in Computer Science, #1770:314--323, Springer Verlag, 2000.

Abstract:
In this note we first formalize the notion of hard tautologies using a nondeterministic generalization of instance complexity. We then show, under reasonable complexity-theoretic assumptions, that there are infinitely many propositional tautologies that are hard to prove in any sound propositional proof system.