On Some Proporties of Frege Proofs - Aleksanyan, Sona R . (Mathematical Problems of Computer Science, 2021)
In [4] a measure s on propositional formula was defined such that for every tautology ϕ "high" value of s(ϕ) requires the large size of proof in the "weak" propositional systems. In this paper it is shown, that there is a tautology ϕ, the measure s(ϕ) of which has exponential dependence on the size of ϕ, but its proof complexity in Frege systems is polynomially bounded.