О полиномиальных ограничениях сложностей выводов в системах Фреге

Ранее одним из авторов было введено понятие определяющего множества переменных пропозициональной формулы, позволившее выделить множество трудноопределяемых тавтологий, сложности выводов которых в ряде систем доказательств классического исчисления высказываний (секвенциальной системе без правила сечения, системе резолюций, системе, основанной на методе расщепления, системе неравенств “Cutting planes”, ограниченных системах Фреге) оцениваются снизу экспонентой от длины выводимой формулы. В настоящей работе доказывается, что для получения суперполиномиальной нижней оценки шагов (длины) выводов в системах Фреге наличия свойства трудноопределяемости недостаточно: приводится пример последовательности трудноопределяемых формул, имеющих полиномиально ограниченные сложности выводов в любой системе Фреге.