Рассмотрим формальную аксиоматическую систему для исчисления предикатов.
1. Алфавит:
а) счетное множество предметных переменных x1, x2, …, xn …;
б) конечное (может быть и пустое) или счетное множество предметных констант а1, а2, …;
в) конечное (может быть и пустое) или счетное множество функциональных букв f1, f2, …, fk, …;
г) конечное (может быть и пустое) или счетное множество предикатных букв А1, А2, …;
д) символы логических операций Ø, É, Ù, Ú, Û;
е) символы кванторов ", $;
ж) скобки ( ) и запятая.
2. Правила построения синтаксически правильных формул:
а) всякий атом есть формула;
б) если А и В – формулы и х – предметная переменная, то каждое из выражений ØА, А ÉВ, АÙВ, АÚВ, АÛВ, "хА, $хА есть формула.
3. Система аксиом. Систему аксиом исчисления предикатов составляют система аксиом исчисления высказываний и две дополнительные аксиомы:
а) "х А(х)®А(t), где А(х) – есть синтаксически правильная формула и t – терм, свободный для х в А(х);
б) А(t) ®$х А(х), где А(х) – есть синтаксически правильная формула и t – терм, свободный для х в А(х).
4. Правила вывода:
а) все аксиомы выводимы;
б) правило подстановки термов t1, t2, …, tn вместо хi1, хi2,… хir в А[хi1, хi2,… хir] такой, что А[хi1, хi2,… хir] свободна для t1, t2, …, tn;
в) правило modus ponens;
г) правило обобщения (или правило связывания квантором всеобщности) – если синтаксически правильная формула В ®А(х) при условии, что В не содержит свободных вхождений х, выводима, то выводима будет и формула В ®"х А(х);
д) правило конкретизации (или правило связывания квантором существования) – если А(х) ® В есть выводимая синтаксически правильная формула (теорема) и В не содержит свободных вхождений х, то $х А(х) ®В также теорема;
е) если А – теорема, имеющая квантор всеобщности и/или квантор существования, то одна связанная переменная в А может быть заменена другой связанной переменной, отличной от всех свободных переменных, одновременно на всех областях действия квантора и в самом кванторе.
Если Qn есть n-местная предикатная переменная, a x1,..., xn — предметные переменные, то выражение Qn (x1,..., xn) есть, по определению, атомарная (элементарная) формула. Индекс n у предикатной переменной в атомарной формуле обычно опускается. Содержательно Q (x1,..., xn) означает высказывание, гласящее, что объекты x1,..., xn связаны отношением Q. Формулами считаются атомарные формулы, а также выражения, получаемые из них посредством следующих операций образования новых формул из уже полученных: 1) если j и — формулы, то (j& ), (j ), (jÉ ) и ùj — также формулы; 2) если j — формула и х — предметная переменная, то "xj, $xj — формулы. Определением формулы заканчивается описание языка исчисления предикатов.
Определение 1. Вхождение предметной переменной х в формулу j называется связанным, если х входит в часть j вида $xj или "xj или стоит непосредственно после знака квантора. Несвязанные вхождения переменной в формулу называются свободными.
Если найдётся хоть одно свободное вхождение х в j, то говорят, что переменная х входит свободно в j или является параметром j. Интуитивно говоря, формула j с параметрами выражает некоторое условие, которое превращается в конкретное высказывание, если (конкретизировав предварительно область объектов) приписать определённые значения входящим в формулу параметрам и предикатным буквам. Связанные же переменные не имеют самостоятельного значения и служат (вместе с соответствующими кванторами) для обозначения общих утверждений или утверждений существования.
В общем случае выражение "хi1"хi2 … "хir A(x1, x2, …, xn), где хi1, хi2,… хir являются подмножеством множества переменных x1, x2, …, xn, означает, что для любых значений, придаваемых переменным хi1, хi2,… хir из области определения A(x1, x2, …, xn), истинность A(x1, x2, …, xn) зависит только от свободных переменных, входящих в эту формулу. Аналогичное утверждение справедливо для квантора существования.
Если к формуле A(x1, x2, …, xn) применить n раз какие-либо кванторы, то получится выражение z1х1z2х2 … znхn A(x1, x2, …, xn), где zI Î{", $}, представляющее собой некоторое постоянное высказывание, которое называется замкнутой формулой, т. е. формулой без свободных переменных.
Формулы исчисления предикатов имеют смысл только тогда, когда имеется какая-нибудь интерпретация входящих в нее символов. Под интерпретацией I в исчислении предикатов понимается всякая система, состоящая из непустого множества M, называемого областью интерпретации, и какого-либо соответствия, относящего каждой предикатной букве Аi некоторое n-местное отношение в M (т. е. Mn®{T,F}), каждой функциональной букве fi – некоторую n-местную функцию в M (т. е. Mn®M) и каждой предметной константе аi – некоторый элемент из M.
— формулы, то (j& 