Propositional proof systems, the consistency of first order theories and the complexity of computations
Jan Krajı́ček, Pavel Pudlák · Journal of Symbolic Logic · 1989
Abstract We consider the problem about the length of proofs of the sentences saying that there is no proof of contradiction in S whose length is < n. We show the relation of this problem to some problems about propositional proof systems.