Модели теории первого порядка определяются как множества с заданными на них операциями и отношениями, удовлетворяющими аксиомам. К таким моделям относятся, например, частично упорядоченные множества и булевы алгебры.

Теории первого порядка возникли с целью формализации и строгого обоснования математики. В 1901 году Дедекинд предложил первое обоснование арифметики, известное теперь под названием системы аксиом Пеано. В 1908 году Цермело сформулировал аксиомы теории множеств. Так было установлено, что множество натуральных чисел и класс всех множеств тоже являются моделями теорий первого порядка. Это стимулировало развитие теории моделей, основные теоремы которой были доказаны Лёвенгеймом (1915 г.), Скулемом (1920 г.), Гёделем (1930 г.), Мальцевым (1936 г.).

Главное внимание в данной главе будет уделено доказательствам теоремы Мальцева о компактности, теорем Гёделя о непротиворечивости исчисления предикатов и о полноте теории первого порядка. Отметим теоремы Лёвенгейма-Скулема, из которых следует существование счётной модели теории множеств и несчётной модели теории натуральных чисел. Рассмотрим метод резолюций Робинсона (1965 г.) автоматического доказательства предложений исчисления предикатов.

Рекомендуемая литература: /2, 3, 5, 7, 9, 10, 11, 13, 14, 17, 18 /.