On non-monotonous properties of some classical and nonclassical propositional proof systems

В настоящей работе для систем Фреге, секвенциальных систем с правилом сечения и систем натуральных выводов классической и неклассических логик исследовано соотношение количества шагов выводов неминимальных тавтологий и их минимальных тавтологий. Доказано, что для каждой из рассмотренных систем существуют такие последовательности неминимальных тавтологий $\psi_n$, каждая из которых имеет единственную минимальную $\varphi_n$ и для каждого $n$ наименьшее количество шагов выводов фомул $\varphi_n$ по порядку больше наименьшего количества шагов выводов фомул $\psi_n$.