Т. А. Сливина математическая логика и теория алгоритмов

Замечание. Ранее в главе 2 было построено классическое исчисление высказываний, содержащее 11 аксиом. Однако может быть построено исчисление высказываний с меньшим числом аксиом (в частности, с логическими аксиомами 1) – 3).
Специальные аксиомы. Они не могут быть сформулированы в общем случае, так как меняются от теории к теории.
Теория первого порядка, не содержащая собственных аксиом, очевидно, представляет собой чисто логическую теорию. Она носит название исчисления предикатов первого порядка.
Во многих теориях, которые могут быть аксиоматизированы как теории первого порядка, используется понятие равенства. Оно вводится путем добавления двухместного предиката « х = у » и в связи с этим добавляются две специальные аксиомы: 1) x (х = х); 2) Если х, у, z – различные предметные переменные и F(z) – формула, то xy(x = yF(x) = F(y)).
Правила вывода. Как и в исчислении высказываний, будем пользоваться понятиями вывода из совокупности формул (высказываний) Н. Высказывания, входящие в Н, будем называть допущениями (или посылками). Если последним высказыванием в выводе из Н стоит высказывание А, то будем говорить, что предложение А выводимо из Н и записывать: Н├А. В частном случае, если Н = , то пишут ├А.
В число правил вывода теории первого порядка включаются два правила:
1. Правило заключения (или modus ponens):
Если ├ А и ├ АВ, то ├ В.
2. Правило связывания квантором всеобщности (или правило обобщения):
Если ├ А, то ├ .


§ 2. Примеры математических теорий из алгебры, анализа, геометрии
1. Теория частичного упорядочения.
Пусть теория Т содержит одну предикатную букву и не содержит функциональных букв и предметных констант. Вместо формул и обычно пишут х₁ < х₂ и х₁ не < х₂ .
Пусть Т содержит две специальные аксиомы:
а) (  ) – иррефлективность;
б)    – транзитивность.
Всякая модель этой теории называется частично упорядоченной структурой.