425
ЛОГИКА ПРЕДИКАТОВ Правило эквивалентной замены используется, в частности, при осуществлении процедуры приведения формул языка логики предикатов к какому-либо стандартному, каноническому виду. Наиболее известным каноническим типом формул языка логики предикатов являются предваренные нормальные формы. Формула находится в предваренной нормальной форме, если она имеет вид Q^Q^.-.Q^B, где каждое Q. есть V или 3, переменные а , а2,..., ап попарно различны и В не содержит кванторов (т. е. формула начинается кванторнои приставкой, после которой следует бескванторная формула). Доказуемо метаутверждение о том, что для любой формулы языка логики предикатов существует логически эквивалентная ей формула в предваренной нормальной форме (при приведении формул к данному каноническому виду используются законы вынесения кванторов, причем иногда более сложные, чем указанные выше). Разновидностью предваренных являются т. н. сколемовские нормальные формы — замкнутые формулы, в которых всякий квантор существования предшествует в кванторнои приставке всякому квантору общности. Для каждой формулы А языка логики предикатовбезпредметныхи предметно-функциональных констант, но с бесконечным числом предикаторных констант произвольной местности существует формула В в сколемовс- кой нормальной форме, равносильная ей по доказуемости (т. е. такая, что |— А, если и только если |— В). Первопорядковая логика может быть модифицирована за счет расширения выразительных возможностей ее языка. Наиболее естественным расширением является введение отношения равенства между индивидами (тождества индивидов). Вовлечение этого отношения в сферу логического анализа оправдано тем, что оно не менее фундаментально, чем исследуемые в логике отношения присущности свойства предмету, включения класса в класс и др. Если в алфавит вводятся предметно-функциональные константы, то отношение равенства позволяет удобным образом выражать утверждения о результатах применения соответствующих функций к различным аргументам. Кроме того, использование знака данного отношения (=) обеспечивает более адекватный анализ многих естественно-языковых контекстов, напр. т. н. исключающих высказываний. Так, логическая форма высказывания «Всякий металл, кроме ртути, находится в твердом состоянии» может быть выражена с использованием предикатора равенства формулой Vx((P(jt) л-.(х = a)) =>Q(x)) A-iQ(a), где константы а, Р, Q соответствуют дескриптивным терминам «ртуть», «металл», «находится в твердом состоянии». Классическая логика предикатов с равенством строится следующим образом. Алфавит пополняется выделенной двухместной предикаторной константой равенства =. Появляется новый тип формул: t, = t2, где t, и t2 — термы. В семантике константе = в качестве значения сопоставляется множество всех пар <���и, иglt;, где и — элемент универсума U (или же предметно-истинностная функция, которая ставит в соответствие значение И только парам одинаковых объектов из U). Формула t, = t2 примет значение И в некоторой модели при распределении ф значений предметных переменных, если и только если значения термов t, и t2 в данной модели при данном распределении совпадают. Остальные семантические понятия остаются прежними. Адекватное аксиоматическое представление логики предикатов с равенством можно получить за счет присоединения дополнительных схем аксиом: схемы рефлексивности равенства Va(a=a) и схемы замены равного равным VaV?(a = ? z> (A(a) z> A(?))), где A(?) — есть результат замены некоторого числа (необязательно всех) свободных вхождений переменной a в А(а) на переменную ?, причем заменяемые вхождения не должны находиться в области действия кванторов по ?. Средствами логики предикатов с равенством может быть определен квантор, особенно часто встречающийся в математических контекстах, «существует единственный» (символически - 3!): 3! А(а) = Df 3a(A(a)AV?(A(?)=)? = а)). Язык логики предикатов первого порядка является удобным средством для строгого построения на его основе конкретных, прикладных теорий. В этом случае вместо абстрактных предметных, предикаторных и предметно-функциональных констант в алфавит вводятся конкретные термины словаря теории — имена объектов ее предметной области, знаки их свойств и отношений, знаки заданных на данной области предметных функций. Сами прикладные первопорядковые теории (их часто еше называют элементарными) строятся обычно аксиоматически. К логической части (аксиомам и правилам вывода исчисления предикатов) добавляется собственная часть прикладной теории — постулаты, отражающие закономерности ее предметной области. Простейшими примерами первопорядковых теорий являются т. н. логики отношений: теория отношения эквивалентности (при этом в язык вводится его знак, напр. =, и добавляются аксиомы, указывающие на свойства данного отношения: Va(a=a) — рефлексивность, VaV?(a=?z>?=a) — симметричность, VaV?Vy((a=?&? ^у) =эа =у) — транзитивность), теория отношения частичного порядка (вводится символ этого отношения, напр., < , и собственные аксиомы рефлексивности, транзитивности, а также VaV? ((a