Исследуются модели универсальных формул первого порядка без функциональных символов. Доказывается существование ограниченного числа типов подмоделей, из которых образуются логические модели таких формул. Основываясь на этом, доказывается разрешимость проблемы общезначимо для класса формул, представляющих собой импликации следующего вида. Их посылки — это универсальные формулы, а заключения — формулы первого порядка, сигнатура которых включена в сигнатуру посылок и вхождения атомов одного знака — либо положительные, либо отрицательные. Показано, что ослабление требований на вид заключения импликации приводит к неразрешимому классу.

логическая формула, формулы первого порядка, логическая модель, универсальная формулы, разрешимый класс

Математические вопросы и теория численных методов