Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Р = {Л^, i >1, п > 0 } - непустое, конечное или счетное множество предикатных букв. F = {fP, i > I, п > 1 } - конечное (возможно и пустое) или счетное множество функциональных букв. Верхний индекс предикатной или функциональной буквы указывает число аргументов, а нижний индекс служит для различения букв с одним и тем же числом аргументов. Символы из V, а также символы —i, Vxi ,3xi (i>l), (, ) и ,(запятая) считаются логическими символами, а символы из А, Р и F - специальными символами. Различные теории первого порядка могут отличаться друг от друга составом символов. Например, в некоторых теориях могут совсем отсутствовать функциональные буквы. Из перечня символов видно, что некоторые из них обязательно принадлежат всем теориям первого порядка. Используя введенные символы, порождаются «слова» языка теории. Каждый язык первого порядка задается своей сигнатурой - набором из трех множеств П = {А, F, Р), где, как уже указано А - множество постоянных (констант), F - множество функциональных букв, Р - множество предикатных букв. Символы, не попавшие в сигнатуру, являются общими для каждой теории первого порядка. Сигнатуры теории могут не совпадать. Язык теории первого порядка с сигнатурой D называется языком Q. 2. Формулы теории первого порядка определяются точно так же, как определяются формулы в логике предикатов. 3. Аксиомы теории К разбиваются на два класса: логические аксиомы и собственные аксиомы. Логические аксиомы: каковы бы ни были формулы А, В, С теории К, следующие формулы являются логическими аксиомами теории К\ А1: А^(В^А); А2: (А^(В^>С))^((А^В)^(А^>С)); A3: (—В^—А)^(( —iB^A)^B); А4: Vxi A(Xi) ^A(t), здесь A (Xi) есть формула теории Knt есть терм теории К, свободный для Х/ BA{Xi); А5: Vxi {A^B)^A^VxiB), если формула А не содержит свободных вхождений Х/. Собственные аксиомы. Собственные аксиомы не могут быть сформулированы в общем случае, ибо меняются от теории к теории. В дальнейшем рассмотрим конкретную теорию первого порядка (формальную 123