Proof complexity characteristics in the Frege systems and Frege systems with substitution rule (simple and multiply) are investigated in this paper. For given tautology φ the notion of minimal-determinative disjunctive normal form Ɗ_min (φ) is introduced and it is proved that the steps of shortest Frege proof of φ is no more, than c∙s∙Ɩ, where s is some characteristic of Ɗ_min (φ), Ɩ is the size of φ and c is some constant, depending of Frege systems choice. It is show also that for given n the sequence of formulas with the size n can be constructed such, that the characteristic s is equal n, n² , n³ ,…, n^{[√nlog_n 2]} . It is proved also, that there exist the sequence of tautologies with the size n, the proof steps and proof sizes of which both in Frege systems and in Frege with substitution are equal by order n and n² accordingly. Also it is proved that there exist the sequence of tautologies with the size n, the steps of which in the systems with simple substitution are no less than n, while in the systems with multiply substitution are no more than log₂ n.

proof complexity characteristics, Frege systems, Frege systems with substitution rule, determinative conjunct, minimal-determinative disjunctive normal form

Mathematical problems and theory of numerical methods