424
ЛОГИКА ПРЕДИКАТОВ смысле. Можно далее ввести понятия закона логики предикатов (логически истинного предложения теории): |= А тогда и только тогда, когда при любой оценке V (т. е. в любой теории) А принимает значение И. Множество формул, являющихся законами классической логики предикатов первого порядка, вообще говоря, бесконечно. Среди них — каждый подстановочный случай произвольной тавтологии логики высказываний (т. е. результат замещения в ней пропозициональных переменных формулами языка логики предикатов). Вот некоторые другие наиболее важные типы общезначимых формул. Законы удаления квантора общности и введения квантора су- шествования: VoAz>A(t), A(t)=>3aA, где A(t) — результат правильной подстановки терма t вместо всех свободных вхождений предметной переменной а в формулу А (подобная подстановка называется правильной, когда никакое из заменяемых вхождений а в А не находится в области действия квантора по переменной, входящей в состав терма t). Законы взаимовыразимости кванторов: VaA=-За-А, ЗаА=-• Va-A (где = — знак эквиваленции, которую можно ввести посредством определения (А = В) = w (A z> В) л (В z> A)). Законы перестановочности кванторов: VaV?A => V?VaA, ЗоЗрА => ЗрЗаА, 3aV?A z> V?3aA Законы пронесения и вынесения кванторов: Va-тА = Заа-А, За-А^Va-A, Va(A л В) = ( VaAA л VaB), За(А v В) = (aaA v ЗаВ), (ЗаА з VaB) з Va(A з В), За(А з В) = (VaA з ЗаВ), Va(A v В) = (AvVaB), За(А л В) = (А л ЗаВ), Va(A з В) = (А з VaB), 3a(A з В) = (А з ЗаВ), Va(Bz>A) = (3aBz>A), 3a(Bz>A) = (VaBz>A) (в формулах последних шести типов переменная a не должна содержаться свободно в формуле А). Как известно, помимо семантического представления логических теорий имеется другой, синтаксический метод их построения — в виде логических исчислений. Суть этого метода состоит в формулировании точных правил оперирования со знаками (формулами языка), позволяющими без использования каких-либо семантических понятий («интерпретация», «модель», «истина») осуществлять обоснование логических законов и форм корректных рассуждений. При этом в исчислениях постулируется лишь некоторый минимум дедуктивных средств, дающий тем не менее возможность обозреть все бесконечное множество законов и модусов правильных рассуждений соответствующей логической теории. Существует много различных способов построения логических исчислений (Иотслате irwimw, Натуральный вывод, Аналитические таблицы), в том числе и классического исчисления предикатов первого порядка. Исторически первыми появились аксиоматические исчисления (исчисления гильбертовского типа), в которых, как и при аксиоматическом представлении логики высказываний, статусом аксиом наделяется конечное число общезначимых формул и постулируется некоторый набор правил вывода. Однако в силу сложности формулировок правил подстановки, используемых в этом случае, удобнее строить аксиоматическое исчисление предикатов со схемами аксиом, каждой из которых соответствует бесконечное число аксиом одного и того же типа. Примером одной из возможных аксиоматизаций логики предикатов может служить следующая: в качестве исходного логического символа алфавита, наряду с пропозициональными связками -I, л, v, з, выбирается лишь KBamopV. Постулируется некоторый полный набор схем аксиом классического исчисления высказываний (они задают смысл -ц л, v, з. Дополнительно вводятся две схемы аксиом, задающих смысл квантора V: закон удаления квантора Vaz> A(t) и один из законов пронесения квантора Va(A з В) з (А з VaB) с указанными ранее ограничениями. В исчислении имеется также два правила вывода: АЕ? ? (modusponens), —^- (генерализация). В VaA Квантор существования вводится по определению: ЗаА =^-1 Va-A Следующий этап в построении исчисления — введение понятий доказательства и вывода, а также синтаксических аналогов понятия общезначимой формулы и отношения логического следования — понятия теоремы и отношения выводимости. Доказательством называют непустую конечную последовательность формул, каждая из которых либо является аксиомой исчисления, либо получена из предшествующих формул последовательности по одному из исходных правил вывода. Последняя формула доказательства называется теоремой или доказуемой в исчислении формулой (метаугверждение «А — теорема» принято записывать так: |—А). Вывод из множества допущений Г отличается от доказательства тем, что в нем разрешено дополнительно использовать формулы из Г. Однако, если ставится задача адекватного воспроизведения отношения логического следования, понятие вывода должно быть дополнено наложением некоторых ограничений на применение правила генерализации (дело в том, что—в отличие от modus ponens—из посылки А данного правила не следует логически его заключение VaA). Указанная проблема может быть решена различными способами, напр., введением понятия вывода с варьируемыми переменными. Довольно естественным представляется другой путь, основанный на понятии зависимости формул вывода от допущений: каждое допущение зависит от самого себя; аксиома не зависит от допущений; результат применения modus ponens зависит от тех допущений, от которых зависит хотя бы одна из посылок правила; при применении генерализации зависимости сохраняются. Теперь необходимые ограничения в определении вывода можно сформулировать следующим образом: формула 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 примет значение И в некоторой модели <U, I> при распределении ф значений предметных переменных, если и только если значения термов 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<?&?<a) zxx = ?) — антисимметричность) и др. Наиболее известным примером элементарной теории является система формальной арифметики Пеано. Ее исходные нелогические символы — имя 0, знаки функций ' (прибавления единицы), + (сложения), • (умножения); в алфавите содержится также символ =. Знаки других арифметических объектов, свойств, отношений и функций вводятся посредством определений (напр., 1 =Dr 0'). Далее к логическим аксиомам добавляются собственно арифметические. Еще одним побудительным мотивом расширения выразительных возможностей языка логики предикатов является стремление к более адекватному логическому анализу контекстов естественного языка. Так, точное воспроизведение структуры описательных имен предполагает обогащение ее языка операторами дескрипции, ведь в стандартном первопорядковом языке выразим лишь один тип сложных имен — образованных с использованием предметных функторов. Обычно различается два оператора дескрипции — оператор определенной дескрипции i и оператор неопределенной дескрипции е. При введении их в язык логики предикатов в нем появляется новые типы сложных термов — lOtA («тот самый единственный а, который удовлетворяет условию А») и еосА («некий а из числа тех, которые удовлетворяют условию А»), где a — предметная переменная, а А — формула. Поскольку теперь определение терма содержит ссылку на понятие формулы, оба понятия — терма и формулы — вводят совместным индуктивным определением. Логические системы с оператором определенной дескрипции были построены и изучены Б. Расселом, а Д. Гильбертом было сформулировано е-исчисление — обобщение первопорядковой логики предикатов за счет добавления е-термов.
