Аннотация:
Изучаются теории, основанные на классической логике высказываний. Из леммы Сушко следует, что для любой классической пропозициональной теории $T$ и любой подстановки $\varepsilon$ формул вместо пропозициональных переменных множество $\varepsilon^{-1}(T)$ также является классической пропозициональной теорией. В работе доказывается следующее усиление этого утверждения: для всякой непротиворечивой конечно аксиоматизируемой классической пропозициональной теории $T$ существует такая подстановка $\varepsilon$, что $T$ является прообразом множества всех тождественно истинных формул при $\varepsilon$. Приводится алгоритм, который по данной аксиоме теории позволяет найти подстановку, обладающую указанным свойством.
Ключевые слова:решетка теорий классической пропозициональной логики, обращение подстановки, унификация, лемма Сушко.
УДК:510.633
Поступила: 09.02.2019 Исправленный вариант: 26.03.2019 Принята к публикации: 27.03.2019