хотя бы одна из посылок правила; при применении генерализации зависимости сохраняются. Теперь необходимые ограничения в определении вывода можно сформулировать следующим образом: формула VaA может быть получена по правилу генерализации из А, зависящего от множества допущений А лишь в том случае, когда a не имеет свободных вхождений ни в одну формулу из А. Если имеется вывод из множества допущений Г, последней формулой которого является формула В, говорят, что В выводима из Г (Г |— В). Отношение выводимости в логике предикатов обладает одним важным свойством, которое фиксируется в т. н. дедулцш теореме: если ГА |— В, то Г}—Аз В. Данное свойство существенно упрощает процедуру построения выводов и может быть использовано в качестве производного правила вывода. Другим подобным правилом является т. н. правило эквивалентной замены: если р- A s В, то |— СА = Св (где СА — произвольная формула языка логики предикатов, содержащая в своем составе некоторое вхождение формулы А, а Св—результат замещения выделенного вхождения А в СА формулой В).
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 примет значение И в некоторой модели 426 ЛОГИКА ПРЕДИКАТОВДругое расширение стандартной логики предикатов связано с рассмотрением т. н. обобщенных кванторов (кванторов Генки на). Если в стандартной кванторной приставке любой формулы, находящейся в предваренной нормальной форме, каждый квантор содержится в области действия всех предшествующих ему кванторов, то обобщенные кванторы представляют собой кванторные комплексы, составляющие которых не обязаны более быть упорядочены отношением строгого линейного порядка. Введение обобщенных кванторов позволяет строить адекватные модели достаточно сложных фрагментов естественного языка. В первопорядковой логике предикатов, как уже говорилось, разрешается квалификация только предметных переменных, т. е. кванторы могут быть соотнесены лишь с предметами, индивидами («всякий предмет», «некоторый предмет»). Для логического анализа контекстов, в которых кванторы соотносятся также со свойствами, отношениями, функциями, необходим переход к логике второго порядка. В алфавите ее языка наряду с предикаторными константами Р", Qn, Rn, Р^,... имеются предикаторные переменные различной местности Р1, Q", /Р1, Р,п,— (в алфавит могут быть введены также и предметно-функциональные переменные/, g", /*",/[",.-•)• В атомарных формулах n(t,,t2,...,tn) на месте П могут использоваться как предикаторные константы, так и предикаторные переменные(аналогично,всложныхтермахФ(1],12,...Дп)вроли Ф может выступать теперь предметно-функциональная переменная). «Кванторные» пункты в определении формулы видоизменяются за счет разрешения использовать в формулах видов VolA и ЗаА на месте а не только предметные, но также предикаторные и предметно-функциональные (если они есть в алфавите) переменные. Средствами языка второпорядковой логики предикатов могут быть воспроизведены логические формы многих высказываний, которые нельзя выразить в первопорядковом языке (напр., «У Марса и Земли есть общие свойства» — ЗР(Р(а) л Р(Ь)), «Марс обладает всеми свойствами, присущими каждой планете» — V/\\/x(S(x) z> Рх)) z> P(a)), где константам a, b и S соответствуют термины «Марс», «Земля», «планета»). Семантически логика предикатов второго порядка строится по аналогии с первопорядковой. При распределении значений