Intuitionistic frege systems are polynomially equivalent

В работе (Cook, Reckhow, 1979) было доказано, что две произвольные классические системы Фреге полиномиально моделируют друг друга. Аналогичное доказательство не проходит в случае интуиционистских систем Фреге, так как последние могут содержать невыводимые допустимые правила вывода. Правило вывода $A/B$ называется выводимым в некоторой системе доказательств $S$, если формула $A\to B$ выводима в $S$. Правило $A/B$ называется допустимым в $S$, если для всех подстановок $\sigma$ из выводимости формулы $\sigma(A)$ следует выводимость формулы $\sigma(B)$. В данной работе мы показываем, как устранить все применения допустимых правил, увеличивая сложность исходного доказательства не более чем полиномиально. Следовательно, две произвольные интуиционистские системы Фреге полиномиально эквивалентны. Библ. – 20 назв.