Аксиоматическая система исчисления предикатов

аксиоматическая система исчисления предикатов ЛОГИКА ПРЕДИКАТОВ – раздел современной логики символической, изучающий  рассуждения и другие языковые контексты с учетом внутренней структуры входящих в  них простых высказываний, при этом выражения языка трактуются функционально, т.е.  как знаки некоторых функций или же знаки аргументов этих функций. Важнейшая особенность логики предикатов состоит в том, что т.н. общие имена (напр.,  «человек», «город», «металл»), знаки свойств («белый», «умный», «электропроводный») и знаки отношений («старше», «севернее», «тяжелее») рассматриваются как принадлежащие одной категории знаков, а именно, категории предикаторов – предметно­истинностных  функторов. Предикаторы репрезентируют функции, возможными аргументами которых  являются объекты некоторого универсума рассмотрения, а значениями – истинностные  оценки (в классической логике – это «истина» и «ложь»). Напр., предикатор «человек»  представляет функцию, которая каждому отдельному человеку сопоставляет оценку  «истина», а каждому отличному от человека существу – оценку «ложь». Функция,  соответствующая предикатору «севернее», сопоставляет «истину» каждой такой паре  географических точек, первая из которых действительно расположена севернее второй  (напр., паре <Петербург, Москва>), всем остальным парам географических точек (напр.,  парам <Москва, Петербург> и <Москва, Москва>) эта функция сопоставляет оценку  «ложь». Предикаторы различаются, как говорят, своей местностью: предикаторы,  представляющие предметно­истинностные функции от одного аргумента, называются  одноместными, те, которым соответствуют функции от двух аргументов, – двухместными и т.д. (напр., предикатор «человек» одноместный, а предикатор «севернее» двухместный). Множество тех объектов универсума (или же множество тех n­ок объектов), которым  одноместная (многоместная) предметно­истинностная функция сопоставляет значение  «истина», называется областью истинности соответствующего предикатора. Часто при  построении логики предикатов предикаторам в качестве значений сопоставляются  области их истинности, т.е. свойства (для одноместных предикаторов) и отношения (для  многоместных предикаторов), рассматриваемые с объемной, экстенсиональной точки  зрения. Другой отличительной чертой логики предикатов является использование особого типа  логических символов – кванторов и связываемых ими (квантифицируемых) переменных  для воспроизведения логических форм множественных высказываний.  Квантифицируемые переменные «пробегают» по множеству всех объектов рассмотрения, а роль квантора состоит в указании на ту часть объектов этого множества, для которых  справедливо содержащееся в высказывании утверждение. Наиболее употребимы в логике  квантор общности ∀ (в естественном языке ему соответствуют термины типа «всякий»,  «каждый», «любой», «произвольный») и квантор существования ∃ («существует»,  «найдется», «имеется», «некоторый»). К примеру, логическая форма высказывания  «Некто умен» может быть выражена с использованием квантора ∃ и переменной х,  пробегающей по множеству людей, так; ∃хР(х), где символ  одноместному предикатору «умный», а форма высказывания «Каждый знает кого­нибудь» – посредством формулы ∀х∃уR(х,у), где квантифицируемые переменные х и у пробегают  по тому же множеству, а символ R соответствует двухместному предикатору «знает». Ρ  соответствует  Логика предикатов как раздел символической логики включает в себя логические теории  разных типов, отличающиеся как выразительными возможностями языков, в которых они  формулируются, так и классами выделяемых в них логических законов (см. Закон  логический). В зависимости от типа сущностей, составляющих допустимые в теории области пробега  квантифицируемых переменных, различают логику предикатов первого порядка и логику  предикатов высших порядков. В первопорядковой логике имеется лишь один тип  квантифицируемых переменных – предметные (индивидные) переменные, возможными  значениями которых являются индивиды, отдельно взятые предметы (люди, города, числа  и т.п.). В логике предикатов второго порядка дополнительно вводятся переменные,  пробегающие по признакам индивидов – их свойствам и отношениям между ними (эти  переменные тоже разрешается связывать кванторами, получая выражения типа ∀PA –  «Для всякого свойства Ρ верно, что А», ∃RA – «Существует отношение R, такое что А»);  в логике предикатов третьего порядка разрешается квантификация по признакам  признаков индивидов и т.д. Выделяют также односортные и многосортные системы логики предикатов: в  односортной все переменные, принадлежащие к одному и тому же типу, имеют  одинаковую область пробега; в многосортной с каждой переменной связывается  собственное множество ее возможных значений. Наконец, данный раздел логики включает как классические, так и неклассические  логические теории. В основе классической логики предикатов лежат, прежде всего, общие для всех классических систем логики принципы – двузначности (всякое высказывание  принимает ровно одно из двух значений: «истину» или «ложь»), экстенсиональности  (значение сложного выражения зависит только от значений составляющих его выражений), а также идущая от Аристотеля классическая трактовка истины как соответствия наших утверждений действительности. Кроме того, в классической логике предикатов  принимаются специфические именно для кванторной теории предпосылки  экзистенциального характера – допущение о существовании объектов в предметной  области и существовании денотатов у сингулярных терминов (термин «существование»  здесь следует понимать в смысле известного критерия У.Куайна: «существовать – значит  быть возможным значением квантифицируемой переменной»). В неклассических  предикатных системах в той или иной форме происходит пересмотр указанных  принципов.  – знак отрицания, ∧ – знак  Наиболее фундаментальный статус имеет классическая односортная логика предикатов  первого порядка. Ее язык задается следующим образом. В алфавит вводится некоторая  функционально полная система пропозициональных связок (см. Логика  высказываний, Логические связки), напр. { , ∧, ∨, ⊃} (где  конъюнкции, ∨ – знак дизъюнкции, ⊃ – знак материальной импликации), а также  кванторы ∀ и ∃ (имеется возможность выбрать в качестве исходного символа языка лишь  один из этих кванторов, другой может быть введен по определению). В алфавите  содержится также бесконечный список предметных переменных (х, у, z, x1, …).∙ Среди  нелогических символов обязательно наличие непустого множества предикаторных  констант – аналога предикаторов естественного языка (будем использовать для них  символы Рn, Qn, Rn, Р1 n,..., где верхний индекс n – натуральное число, указывающее на  местность предикаторной константы). Кроме этого в алфавит могут быть введены  нелогические символы других типов: предметные константы (а, b, с, а1,...) – аналоги  собственных имен (знаков отдельных предметов) естественного языка, напр., «Москва»,  «Луна», «медь», а также предметно­функциональные константы различной местности (fn,  gn, hn, f1 значениями которых являются индивиды, напр., «+», «возраст», «расстояние от... до...»).  Иногда в алфавит языка логики предикатов добавляют пропозициональные переменные  (p, q, r, p1,...) – аналоги простых высказываний естественного языка, исходя из  буквального понимания тезиса о том, что логика предикатов является  расширением логики высказываний. Однако данное добавление не является  необходимым: при желании в качестве пропозициональных переменных можно разрешить  использование нульместных предикаторных констант. Техническими символами алфавита являются левая и правая скобки и запятая. n, ...) – аналоги предметных функторов (знаков таких функций, аргументами и  Выражением языка логики предикатов называется любая конечная последовательность  символов ее алфавита. Некоторые из этих выражений являются правильно построенными,  а некоторые нет. В логике предикатов имеется два типа правильно построенных  выражений – термы и формулы. Понятие «терма» вводится следующим индуктивным определением: (1) всякая  предметная переменная – терм; (2) всякая предметная константа – терм; (3) если  местная предметно­функциональная константа, и t1, t2,..., tn – термы, то выражение  t2,..., tn) является термом; (4) ничто иное термом не является.  – n­Φ (tΦ 1,  Среди термов различают простые (указанные в пунктах (1) и (2) данного определения), и  сложные (указанные в пункте (3)), а также замкнутые (не содержащие в своем составе  предметных переменных) и незамкнутые (содержащие переменные). Замкнутые термы  являются аналогами имен естественного языка (как простых, так и сложных), а  незамкнутые – аналогами т.н. именных форм (выражений с переменными, которые могут  быть преобразованы в имена с помощью подстановки конкретных имен на места  переменных, напр., «рост х», «х × 5», «разница в возрасте между x и y»). Понятие формулы также определяется индуктивно: (1) если  предикаторная константа, и t1, t2,..., tn – термы, то выражение П(t1,t2,...,tn) является  формулой; (2) если А – формула, то  А – формула; (3) если А и В – формулы, то  выражения (А∧В), (Α∨В), (А⊃В) также являются формулами; (4) если А – формула, и  ∃ А также являются формулами; (5)  – предметная переменная, то выражения ∀ А и  α ничто иное формулой не является. Внешние скобки в формулах обычно опускают.  – n­местная  α Π  α Заметим, что в определениях терма и формулы используются т.н. синтаксические  переменные (А, В,  различным типам выражений объектного языка. ) – переменные метаязыка, пробегающие по  , tα 1, t2,..., tn,  Φ Π ,  Формулы, соответствующие пункту (1) определения, называют простыми, или  атомарными, а все остальные формулы (которые содержат по крайней мере один  логический символ) – сложными, или молекулярными. α α . Конкретное  Различение замкнутых и незамкнутых формул требует предварительного введения  нескольких синтаксических понятий. Подформула А в составе формул вида ∀ А и  называется областью действия квантора (∀ или ∃) по переменной  вхождение некоторой переменной в некоторую формулу называется связанным, если это  вхождение следует непосредственно за квантором или же находится в области действия  квантора по данной переменной; в противном случае вхождение переменной называется  α свободным. Переменная  α α свободное вхождение   в А; переменная   связана в формуле А, если и только если  существует связанное вхождение  предикатов свободные и связанные переменные различают уже на этапе задания его  алфавита, для них используют различные списки символов. В таком случае разрешается   свободна в формуле А, если и только если существует   в А. (Иногда при формулировке языка логики  ∃ А α α квантификация только связанных переменных, а свободные переменные выступают в роли неквантифицируемых индивидных параметров.) Формула называется замкнутой, если она не содержит свободных вхождений предметных  переменных; в противном случае она является незамкнутой. Замкнутые формулы  являются аналогами высказываний естественного языка (результатом символической  записи любого высказывания является именно замкнутая формула), поэтому их иногда  называют предложениями языка логики предикатов. Незамкнутые формулы  соответствуют т.н. пропозициональным формам – выражениям естественного языка с  переменными (напр., «x выше у», «х смелый»), из которых могут быть образованы  высказывания посредством операций константного или кванторного замыкания (напр.,  «Эверест выше Арарата», «Существует x такой, что x смелый»). Семантическое построение классической односортной логики предикатов первого  порядка может осуществляться различными способами. Сформулируем наиболее  естественную, теоретико­множественную объектную семантику описанного выше языка. Первый этап ее построения – задание класса допустимых интерпретаций нелогических  символов языка. С этой целью выбирается некоторое множество U, называемое областью  интерпретации (универсумом); единственным ограничением, накладываемым на U,  является требование его непустоты. Приписывание значений нелогическим символам  релятивизируется относительно выбранной предметной области. Его можно осуществить  посредством специальной интерпретирующей функции I. Эта функция сопоставляет  произвольной предметной константе k некоторый объект из универсума U: I(k)∈U (при  этом становится очевидным, что предметные константы имеют тот же тип значений, что  имена естественного языка, и могут рассматриваться в качестве параметров последних),  n­местной предикаторной константе  экстенсионально понимаемые свойство или отношение на U, т.е. некоторое множество  упорядоченных n­ок объектов из универсума: І(П) ⊆ Un (Un – n­ная декартова степень  множества U). Имеется и другая возможность – сопоставить константе   n­местную  функцию, аргументами которой являются элементы универсума, а возможными  значениями И («истина») и Л («ложь»): І(П) есть функция типа Un   {И, Л}. Во втором  случае предикаторные константы рассматриваются как знаки предметно­истинностных  функций. Произвольной n­местной предметно­функциональной константе  интерпретирующая функция сопоставляет в качестве значения n­местную операцию,  заданную на множестве U (ее аргументами и значениями являются элементы универсума): І(Ф) есть функция типа Un   в качестве значения обычно приписывают   U.→ Π Π →  Φ Интерпретирующую функцию I, релятивизированную относительно некоторой  предметной области U, a точнее – пару , называют моделью или возможной  реализацией. Выбор конкретной модели детерминирует значения всех замкнутых термов и замкнутых формул языка логики предикатов. Для определения значений незамкнутых  термов и формул необходимо дополнительно зафиксировать, распределить значения  предметных переменных (таковыми, как и для предметных констант, являются элементы  универсума).  φ Следующим этапом семантического построения логики предикатов является  формулировка точных правил установления значений правильно построенных выражений  ее языка (т.е. термов и формул) в рамках выбранных модели  и распределения  значений предметных переменных. φ  являются объекты из U. Значения предметных  Значениями термов в  при  констант и переменных уже определены посредством функций I и  (tΦ 1, t2,..., tn) является тот объект из U, который представляет  Значением сложного терма  собой результат применения операции І(Ф) к n­ке значений (в этой же модели и при этом  же распределении) термов t1, t2,..., tn. Пусть, напр., в качестве универсума выбрано  множество натуральных чисел, предметно­функциональная константа f  проинтерпретирована как операция сложения, а предметные константы а и b как числа 2 и 3. Тогда значением терма f(a,b) в соответствующей модели будет результат сложения 2 и  3, т.е. число 5. φ  соответственно.   φ φ ) термов t Формулы языка логики предикатов принимают в модели  при распределении  ровно одно из двух значений – И или Л. Атомарная формула вида II(t1, t2,..., tn) принимает  – при трактовке предикаторных констант как знаков экстенсионально понимаемых  свойств и отношений – значение И, если и только если n­ка значений (в данной модели и  при данном распределении  І(П), когда n > 1, или обладает свойством І(П), когда n = 1. Если же предикаторные  константы интерпретируются как знаки предметно­истинностных функций, то П(t1, t2,...,  tn) примет значение И в том и только в том случае, когда результат применения подобной  функции І(П) к указанной n­ке объектов даст И. В упомянутой в предыдущем примере  конкретной модели и при интерпретации предикаторной константы R как отношения  «меньше» формула R(a,b) примет значение И, т.к. 2 действительно меньше 3, а формула  R(b,a) – значение Л, поскольку 3 не находится в указанном отношении к 2. 1, t2,..., tn действительно находится в отношении  Условия истинности и ложности формул, главными знаками которых являются  φ пропозициональные связки, сохраняются (с необходимой привязкой к  и  ) такими  же, как в классической логике высказываний. ∃ А)α φ , если и только если ее подкванторная часть Семантические определения для кванторных формул таковы: ∀ А (соответственно  истинна в модели  при распределении  А принимает значение И в той же модели при любом (при некотором) распределении  значений предметных переменных, отличающемся от  Другими словами: формула ∀ А истинна в том случае, когда А оказывается истинной,  α какой бы объект из U мы ни приписали в качестве значения переменной   (сохранив при  этом значения остальных переменных), а ∃ А истинна, если в универсуме найдется такой  объект, что при сопоставлении его в качестве значения переменной  оказывается истинной. φ α  не более, чем значением  .  α  формула А  α α α  ψ Завершающим этапом в построении логики предикатов является введение понятий закона  этой теории (общезначимой формулы) и различных логических отношений между  формулами. Наиболее важным из них является отношение логического следования  (см. Следование логическое), поскольку его наличие составляет критерий  корректности дедуктивных умозаключений. Говорят, что формула значима (истинна) в модели  при некотором распределении φ значений предметных переменных, если и только если данная формула принимает  значение И в этой модели при этом распределении. Формулу называют значимой  (истинной) в модели , если она значима в ней при любом распределении элементов  U предметным переменным. Формула называется общезначимой на множестве U (U­ общезначимой), если она значима в каждой модели с универсумом U.Формула называется  универсально общезначимой (или просто – общезначимой), если она общезначима на  любом (непустом) множестве. Факт общезначимости формулы А обычно выражается в  метаязыке следующей записью: |=А. Общезначимые формулы – это законы логики  предикатов, поскольку они истинны при любых допустимых в данной теории  интерпретациях нелогических символов. Конкретизация понятия логического следования в логике предикатов осуществляется  следующим образом: из множества формул Г логически следует формула В (Г |= В), если  и только если в любой модели и при любом распределении значений предметных  переменных, при которых истинна каждая формула из Г, формула В также примет  значение «истина». В сформулированном выше семантическом варианте правила установления значений  формул имеют отчетливо выраженную объектную направленность: они предполагают, что  при решении вопроса об истинности или ложности происходит соотнесение выражений  языка с нелингвистическими сущностями (индивидами, свойствами, отношениями,  функциями, связанными с некоторой предметной областью). Альтернативой объектной интерпретации формул языка логики предикатов является т.н. подстановочная  интерпретация. Смысл ее состоит в формулировке таких критериев истинности и  ложности предложений языка, которые бы не предполагали соотнесения последних с  внеязыковой действительностью, а опирались бы только на информацию о значениях  элементарных, атомарных предложений (в подобном стиле обычно строится логика  высказываний, где при установлении значений формул необходимо лишь, чтобы каким­то  – неважно каким – образом было осуществлено распределение значений для  пропозициональных переменных). Т.о., при подстановочной интерпретации мы, скорее,  имеем дело не с обычной трактовкой истины как соответствия предложений  действительности, а с тем, что иногда называют «истинностью в теории», где теория  понимается, по существу, в синтаксическом аспекте – как дедуктивно замкнутое  множество предложений языка. Ѵ  распределяет значения для элементарных предложений языка  α Технически «подстановочная» семантика логики предикатов может быть сформулирована следующим образом. Значения здесь естественно сопоставлять лишь замкнутым  формулам, поскольку именно эти формулы представляют собой предложения теории и  могут оцениваться как истинные или ложные в ней. Задается функция оценки V,  отображающая множество замкнутых формул вида П(t1, t2,..., tn) на множество {И, Л}  (содержательно –  теории). Правила установления значений замкнутых формул видов  А, А∧В, А∨В, A⊃B  – стандартные. Формула ∀ А (соответственно  если и только если данное значение при V имеет любой (соответственно по крайней мере  один) результат подстановки в формулу А замкнутого терма t вместо всех свободных  вхождений переменной  теории, если и только если соответствующее бескванторное утверждение справедливо для любого (хотя бы для одного) сингулярного термина, принадлежащего словарю данной  теории). Класс замкнутых формул, принимающих при оценке V значение И, как раз и  представляет собой некоторую теорию в описанном выше смысле. Можно далее ввести  понятия закона логики предикатов (логически истинного предложения теории): |= А тогда и только тогда, когда при любой оценке V (т.е. в любой теории) А принимает значение И. α  (содержательно – общее (частное) предложение истинно в  ∃ А) примет значение И при оценке V,  α Множество формул, являющихся законами классической логики предикатов первого  порядка, вообще говоря, бесконечно. Среди них – каждый подстановочный случай  произвольной тавтологии логики высказываний (т.е. результат замещения в ней  пропозициональных переменных формулами языка логики предикатов). Вот некоторые  другие наиболее важные типы общезначимых формул. Законы удаления квантора общности и введения квантора существования: ∀ A α ⊃ A(t), A(t) ⊃ ∃ A,α   где A(t) – результат правильной подстановки терма t вместо всех свободных вхождений  предметной переменной   в формулу А (подобная подстановка называется правильной,  α когда никакое из заменяемых вхождений  по переменной, входящей в состав терма t).  в А не находится в области действия квантора  α Законы взаимовыразимости кванторов: ∀ A α ≡  ∃α A  – знак эквиваленции, которую можно ввести посредством определения (A  ∃ A α ≡  ∀α A ≡ ≡  В)  (где  ≡Df (А ⊃ В) ∧ (В ⊃ А)). Законы перестановочности кванторов: ∀α∀ A β ⊃ ∀β∀ A,α ∃α∃ A β ⊃ ∃β∃ A,α ∃α∀ A β ⊃ ∀β∃ Aα  ≡ ∃α A,  ≡ ∀α A,  (≡ ∀ Aα ∧∀ B),α Законы пронесения и вынесения кванторов: ∀α A  ∀ (Aα ∧B)  (∃ A α ⊃ ∀ B) α ⊃ ∀ (A α ⊃ B), ∀ (Aα ∨B)  ∀ (A α ⊃ B)  ∀ (B α ⊃ A)  (в формулах последних шести типов переменная a не должна содержаться свободно в  формуле А).  (≡ ∃ Aα ∨∃ B),α  (≡ ∀ A α ⊃ ∃ B),α  (A≡ ∧∃ B),α  (A ≡ ⊃ ∃ B),α  (≡ ∀ B α ⊃ A) ∃α A  ∃ (Aα ∨B)  ∃ (A α ⊃ B)  ∃ (Aα ∧B)  ∃ (A α ⊃ B)  ∃ (B α ⊃ A)   (A≡ ∨∀ B),α  (A ≡ ⊃ ∀ B),α  (≡ ∃ B α ⊃ A), Как известно, помимо семантического представления логических теорий имеется другой,  синтаксический метод их построения – в виде логических исчислений. Суть этого метода  состоит в формулировании точных правил оперирования со знаками (формулами языка),  позволяющими без использования каких­либо семантических понятий («интерпретация»,  «модель», «истина») осуществлять обоснование логических законов и форм корректных  рассуждений. При этом в исчислениях постулируется лишь некоторый минимум  дедуктивных средств, дающий тем не менее возможность обозреть все бесконечное  множество законов и модусов правильных рассуждений соответствующей логической  теории. Существует много различных способов построения логических исчислений (Исчисление  секвенций, Натуральный вывод, Аналитические таблицы), в том числе и классического  исчисления предикатов первого порядка. Исторически первыми появились  аксиоматические исчисления (исчисления гильбертовского типа), в которых, как и при  аксиоматическом представлении логики высказываний, статусом аксиом наделяется  конечное число общезначимых формул и постулируется некоторый набор правил вывода.  Однако в силу сложности формулировок правил подстановки, используемых в этом  случае, удобнее строить аксиоматическое исчисление предикатов со схемами аксиом,  каждой из которых соответствует бесконечное число аксиом одного и того же типа. Примером одной из возможных аксиоматизаций логики предикатов может служить  следующая: в качестве исходного логического символа алфавита, наряду с  пропозициональными связками  некоторый полный набор схем аксиом классического исчисления высказываний (они  , ∧, ∨, ⊃). Дополнительно вводятся две схемы аксиом, задающих смысл  задают смысл  квантора ∀: закон удаления квантора ∀ Aα ⊃A(t) и один из законов пронесения квантора  ∀ (Aα ⊃В)⊃(А⊃∀ В) с указанными ранее ограничениями. В исчислении имеется также  α два правила вывода: , ∧, ∨, ⊃, выбирается лишь квантор ∀. Постулируется  (modus ponens), (генерализация). Квантор существования вводится по определению: ∃ A α ≡ Df ∀α A. Следующий этап в построении исчисления – введение понятий доказательства и вывода, а  также синтаксических аналогов понятия общезначимой формулы и отношения  логического следования – понятия теоремы и отношения выводимости. Доказательством называют непустую конечную последовательность формул, каждая из  которых либо является аксиомой исчисления, либо получена из предшествующих формул последовательности по одному из исходных правил вывода. Последняя формула  доказательства называется теоремой или доказуемой в исчислении формулой  (метаутверждение «А – теорема» принято записывать так: |–А). Вывод из множества допущений Г отличается от доказательства тем, что в нем разрешено  дополнительно использовать формулы из Г. Однако, если ставится задача адекватного  воспроизведения отношения логического следования, понятие вывода должно быть  дополнено наложением некоторых ограничений на применение правила генерализации  (дело в том, что – в отличие от modus ponens – из посылки А данного правила не следует  логически его заключение ∀ A). Указанная проблема может быть решена различными  α способами, напр., введением понятия вывода с варьируемыми переменными. Довольно  естественным представляется другой путь, основанный на понятии зависимости формул  вывода от допущений: каждое допущение зависит от самого себя; аксиома не зависит от  допущений; результат применения modus ponens зависит от тех допущений, от которых  зависит хотя бы одна из посылок правила; при применении генерализации зависимости  сохраняются. Теперь необходимые ограничения в определении вывода можно  сформулировать следующим образом: формула ∀ A может быть получена по правилу  генерализации из А, зависящего от множества допущений Δ, лишь в том случае, когда  имеет свободных вхождений ни в одну формулу из Δ. Если имеется вывод из множества  допущений Г, последней формулой которого является формула В, говорят, что В  выводима из Г (Г |– В). α  неα Отношение выводимости в логике предикатов обладает одним важным свойством,  которое фиксируется в т.н. дедукции теореме: если Г,А |– В, то Г |– A⊃В.Данное  свойство существенно упрощает процедуру построения выводов и может быть  использовано в качестве производного правила вывода. Другим подобным правилом   С≡ в (где СА –  является т.н. правило эквивалентной замены: если |– А  произвольная формула языка логики предикатов, содержащая в своем составе некоторое  вхождение формулы А, а Св – результат замещения выделенного вхождения А в  СА формулой В).  В, то |– С ≡ А  Правило эквивалентной замены используется, в частности, при осуществлении процедуры  приведения формул языка логики предикатов к какому­либо стандартному,  каноническому виду. Наиболее известным каноническим типом формул языка логики  предикатов являются предваренные нормальные формы. Формула находится в  предваренной нормальной форме, если она имеет вид Q1α1Q2α2…QnαnB, где каждое  Qi есть ∀ или ∃, переменные α1,α2,..., αn попарно различны и В не содержит кванторов  (т.е. формула начинается кванторной приставкой, после которой следует бескванторная  формула). Доказуемо метаутверждение о том, что для любой формулы языка логики  предикатов существует логически эквивалентная ей формула в предваренной нормальной  форме (при приведении формул к данному каноническому виду используются законы  вынесения кванторов, причем иногда более сложные, чем указанные выше). Разновидностью предваренных являются т.н. сколемовские нормальные формы –  замкнутые формулы, в которых всякий квантор существования предшествует в  кванторной приставке всякому квантору общности. Для каждой формулы А языка логики предикатов без предметных и предметно­функциональных констант, но с бесконечным  числом предикаторных констант произвольной местности существует формула В в сколемовской нормальной форме, равносильная ей по доказуемости (т.е. такая, что |– А,  если и только если [– В). Первопорядковая логика может быть модифицирована за счет расширения выразительных возможностей ее языка. Наиболее естественным расширением является введение  отношения равенства между индивидами (тождества индивидов). Вовлечение этого  отношения в сферу логического анализа оправдано тем, что оно не менее  фундаментально, чем исследуемые в логике отношения присущности свойства предмету,  включения класса в класс и др. Если в алфавит вводятся предметно­функциональные  константы, то отношение равенства позволяет удобным образом выражать утверждения о  результатах применения соответствующих функций к различным аргументам. Кроме того, использование знака данного отношения (=) обеспечивает более адекватный анализ  многих естественно­языковых контекстов, напр. т.н. исключающих высказываний. Так,  логическая форма высказывания «Всякий металл, кроме ртути, находится в твердом  состоянии» может быть выражена с использованием предикатора равенства формулой  ∀х((Р(х)∧ (х = а)) ⊃ Q(x))∧ Q(a), где константы а, Р, Q соответствуют дескриптивным  терминам «ртуть», «металл», «находится в твердом состоянии». Классическая логика предикатов с равенством строится следующим образом. Алфавит  пополняется выделенной двухместной предикаторной константой равенства =.  Появляется новый тип формул: t1 = t2, где t1 и t2 – термы. В семантике константе = в  качестве значения сопоставляется множество всех пар , где u – элемент универсума U (или же предметно­истинностная функция, которая ставит в соответствие значение И  только парам одинаковых объектов из U). Формула t1 = t2 примет значение И в некоторой  φ модели  при распределении   значений предметных переменных, если и только если значения термов t1 и t2 в данной модели при данном распределении совпадают. Остальные  семантические понятия остаются прежними. Адекватное аксиоматическое представление логики предикатов с равенством можно  получить за счет присоединения дополнительных схем аксиом: схемы рефлексивности  равенства ∀ ( Α β ( ))), где  Α β ( ) – есть результат замены некоторого числа (необязательно всех) свободных  вхождений переменной  должны находиться в области действия кванторов по  , причем заменяемые вхождения не  ) и схемы замены равного равным  β ) на переменную  α β ⊃ (  =  ) Α α ⊃  ( α α α  =  α α  в А( ∀α∀ß(   .β Средствами логики предикатов с равенством может быть определен квантор, особенно  часто встречающийся в математических контекстах, «существует единственный»  (символически – ∃!): ∃! A( α α ≡ Df∃ (А( α ∧∀ß(A(ß) ⊃  ) β α  =  )). α ) Язык логики предикатов первого порядка является удобным средством для строгого  построения на его основе конкретных, прикладных теорий. В этом случае вместо  абстрактных предметных, предикаторных и предметно­функциональных констант в  алфавит вводятся конкретные термины словаря теории – имена объектов ее предметной  области, знаки их свойств и отношений, знаки заданных на данной области предметных  функций. Сами прикладные первопорядковые теории (их часто еще называют  элементарными) строятся обычно аксиоматически. К логической части (аксиомам и  правилам вывода исчисления предикатов) добавляется собственная часть прикладной  теории – постулаты, отражающие закономерности ее предметной области. Простейшими примерами первопорядковых теорий являются т.н. логики отношений:  теория отношения эквивалентности (при этом в язык вводится его знак, напр. ≅, и  добавляются аксиомы, указывающие на свойства данного отношения: ∀ (α α≅ ) – α рефлексивность, ∀α∀ß( β ≅  ) γ ⊃     α ≅  ) – транзитивность), теория отношения частичного порядка (вводится символ этого  отношения, напр., ≤, и собственные аксиомы рефлексивности, транзитивности, а также  ∀α∀ß(( α β  =  ) – антисимметричность) и др. ) – симметричность,  ∀α∀ß∀ (( β α ⊃   ≤  α β  ≤  γ α ≅     &   &  γ  α ≅   β ⊃   β ≅  α β )  Наиболее известным примером элементарной теории является система формальной  арифметики Пеано. Ее исходные нелогические символы – имя 0, знаки функций ´  (прибавления единицы), + (сложения), ∙ (умножения); в алфавите содержится также  символ =. Знаки других арифметических объектов, свойств, отношений и функций  вводятся посредством определений (напр., 1 = Df0´)∙ Далее к логическим аксиомам  добавляются собственно арифметические. Еще одним побудительным мотивом расширения выразительных возможностей языка  логики предикатов является стремление к более адекватному логическому анализу  контекстов естественного языка. Так, точное воспроизведение структуры описательных  имен предполагает обогащение ее языка операторами дескрипции, ведь в стандартном  первопорядковом языке выразим лишь один тип сложных имен – образованных с  использованием предметных функторов. Обычно различается два оператора дескрипции – ε оператор определенной дескрипции   и оператор неопределенной дескрипции  введении их в язык логики предикатов в нем появляется новые типы сложных термов –  ια α    («некий  из числа тех, которые удовлетворяют условию А»), где   – предметная переменная, а А –  формула. Поскольку теперь определение терма содержит ссылку на понятие формулы,  оба понятия – терма и формулы – вводят совместным индуктивным определением.  Логические системы с оператором определенной дескрипции были построены и изучены  А («тот самый единственный а, который удовлетворяет условию А») и  . При  εαΑ α ι Б.Расселом, а Д.Гильбертом было сформулировано  ­исчисление – обобщение  первопорядковой логики предикатов за счет добавления  ­термов. ε ε Другое расширение стандартной логики предикатов связано с рассмотрением т.н.  обобщенных кванторов (кванторов Генкина). Если в стандартной кванторной приставке  любой формулы, находящейся в предваренной нормальной форме, каждый квантор  содержится в области действия всех предшествующих ему кванторов, то обобщенные  кванторы представляют собой кванторные комплексы, составляющие которых не обязаны  более быть упорядочены отношением строгого линейного порядка. Введение обобщенных  кванторов позволяет строить адекватные модели достаточно сложных фрагментов  естественного языка. n,... имеются предикаторные переменные  n,... (в алфавит могут быть введены также и предметно­ n,...). В атомарных формулах П(t1,t2,...tn) на месте Π В первопорядковой логике предикатов, как уже говорилось, разрешается квантификация  только предметных переменных, т.е. кванторы могут быть соотнесены лишь с  предметами, индивидами («всякий предмет», «некоторый предмет»). Для логического  анализа контекстов, в которых кванторы соотносятся также со свойствами, отношениями, функциями, необходим переход к логике второго порядка. В алфавите ее языка наряду с  предикаторными константами Рn, Qn, Rn, Р1 различной местности Рn, Qn, Rn, Р1 функциональные переменные fn, gn,hn, f1 могут использоваться как предикаторные константы, так и предикаторные переменные  (аналогично, в сложных термах  функциональная переменная). «Кванторные» пункты в определении формулы  видоизменяются за счет разрешения использовать в формулах видов ∀ А и  ∃ А на месте α α  не только предметные, но также предикаторные и предметно­функциональные (если  они есть в алфавите) переменные. Средствами языка второпорядковой логики предикатов могут быть воспроизведены логические формы многих высказываний, которые нельзя  выразить в первопорядковом языке (напр., «У Марса и Земли есть общие свойства» –  ∃Р(Р(а)∧Р(b)), «Марс обладает всеми свойствами, присущими каждой планете» –  ∀P(∀x(S(х) ⊃ Р(х)) ⊃ Р(а)), где константам a, b и S соответствуют термины «Марс»,  «Земля», «планета»).  может выступать теперь предметно­ (tΦ 1, t2,∙∙∙,tn) в роли  Φ α Семантически логика предикатов второго порядка строится по аналогии с  первопорядковой. При распределении значений переменных предикаторным и предметно­ функциональным переменным приписываются сущности тех же типов, которые  сопоставляются в модели соответствующим константам. Правила установления значений  термов и формул незначительно адаптируются с учетом синтаксических особенностей  второпорядкового языка. Понятие общезначимой формулы – обычное. Синтаксическое построение логики предикатов второго порядка сталкивается с  фундаментальной проблемой метатеоретического характера – класс общезначимых  формул второпорядковой логики принципиально не аксиоматизируем, не формализуем,  т.е. не существует исчисления, класс теорем которого совпадал бы с классом  общезначимых формул. Тем не менее в качестве второпорядкового исчисления  предикатов обычно рассматривают некоторую неполную формальную систему, которая  получается естественным обобщением первопорядкового исчисления. Логика предикатов второго порядка является очень богатой логической теорией. В ней,  напр., может быть определен предикатор равенства:  определение по своей сути повторяет лейбницевский принцип «тождественности  неразличимых»: равными, тождественными объявляются объекты, обладающие  одинаковыми свойствами). α β ≡ Df∀P(Р(  =    ) α ≡Ρ( )) (это  β Один из возможных путей расширения выразительных средств логики второго порядка  состоит во введении в ее язык предикаторов более высоких ступеней, «предикаторов от  предикаторов». Они выражают свойства свойств или отношений, отношения между  свойствами или отношениями. Так, в контексте «Отношение родства симметрично»  термин «симметрично» репрезентирует свойство отношения (родства), а в контексте  «Щедрость и скупость – противоположные качества» термин «противоположно»  представляет отношение между свойствами (щедростью и скупостью). При указанном  подходе натуральные числа 0, 1, 2,... могут рассматриваться как свойства свойств и  определяться средствами второпорядковой логики предикатов следующим образом: 0(Р)  ≡ DF ∃хР(х), 1(Р) ≡ DF∃хР(х), 2(Р)≡ DF∃х∃у( x = y∧Р(х)∧Р(у)∧∀z(P(z) ⊃ (z = х∨z = у)))  и т.д. Среди неклассических систем логики предикатов следует особо выделить т.н. свободную  логику – нестандартную теорию квантификации, при построении которой отказываются  от обязательного существования индивидов в области интерпретации, а также допускают  пустоту термов. Часто неклассические исчисления предикатов строятся так, что их отличие от  классического проявляется – в самой системе аксиом и правил вывода – лишь на  пропозициональном уровне: вместо схем аксиом классического исчисления высказываний  выбираются схемы аксиом соответствующего неклассического пропозиционального  исчисления (подобным образом обычно строятся кванторные системы интуиционистской логики и минимальной, многие системымодальной логики и релевантной логики). В этом  отношении специфичным является конструктивное исчисление предикатов, в котором  (наряду с модификацией пропозициональной части) принимаются особые, характерные именно для кванторной теории постулаты, формализующие т.н. принцип Маркова  (простейшая формулировка данного принципа такова: ∀х(Р(х)∨ Р(х)) ⊃ ( ∃хР(х)). ∃хP(х) ⊃  Весьма нетривиальной и интересной с философской точки зрения оказалась проблема  построения кванторных расширений модальных логик, известная также как проблема  квантификации в модальных контекстах. При попытке построения модальной логики  предикатов возникает ряд существенных трудностей содержательного характера, на  которые обратил внимание У.Куайн. Помимо известных проблем, связанных с  нарушением принципа взаимозаменимости в неэкстенсиональных контекстах (а модальные контексты – один из их типов), обнаружилось, что к неожиданным результатам в  модальной логике приводит применение правила введения квантора существования  (знаменитый куайновский парадокс Вечерней и Утренней звезды); во многих кванторных  модальных системах ряд теорем не согласуются с интуицией (к ним относятся, напр.,  формула Баркан ◊∃xР(х) ⊃ ∃х◊Р(x), позволяющая заключать от возможности  существования к актуальному существованию некоторого объекта, теорема ∀x∀y(x = y ⊃  □х = у), означающая необходимость любого утверждения о равенстве). Но главной  причиной философской ущербности модальной логики предикатов, по мнению У.Куайна,  является реанимация в ее рамках схоластического понятия модальностей de re  (модальностей, квалифицирующих характер связи признака с предметом) и причастность  этой теории эссенциализму (метафизической концепции, согласно которой предметы сами по себе – независимо от того, как они представлены в языке, – обладают некоторыми  свойствами необходимо, а некоторыми случайно). В современной модальной логике, особенно в результате разработки ее точных  формальных семантик, удалось снять многие возражения У.Куайна. Так, А.Смульяном  была установлена необходимость учета областей действий дескрипций при замене  равного равным в модальных контекстах. С.Крипке предложил способ построения  богатых систем модальной логики предикатов без формулы Баркан и других  парадоксальных законов. Т.Парсонс точными методами продемонстрировал  непричастность данных теорий эссенциализму, показал, что можно развивать модальную  логику в антиэссенциалистском ключе – с отрицанием эссенциалистского принципа в  качестве аксиомы. Тем не менее проблема адекватной экспликации кванторных  модальных контекстов языка, особенно эпистемических контекстов (утверждений о  знании, мнении, вере), и по сей день остается актуальной. Особую важность для логики предикатов, как и для любой логической теории,  представляет исследование ее метатеоретических свойств (см. Металогика). В связи с  наличием двух способов построения логических теорий – семантического и синтаксического (в виде исчислений) – возникает вопрос о соотношении класса  общезначимых в семантике формул и множества теорем исчисления. Классическое  исчисление предикатов первого порядка семантически непротиворечиво (корректно), т.е.  каждая его теорема универсально общезначима. Наличие данного свойства  обосновывается стандартным методом: демонстрируется общезначимость всех аксиом  исчисления и инвариантность его правил вывода относительно свойства «быть  общезначимой формулой». Более трудным оказалось доказательство семантической полноты первопорядкового  исчисления предикатов, т.е. того, что всякая универсально общезначимая формула  является теоремой исчисления. Впервые этот результат был получен К. Гёделем (1930).  Позднее Л.Генкин предложил изящный (хотя и неконструктивный) метод доказательства  полноты, существенно опирающийся на лемму Линденбаума (о возможности расширения  любого непротиворечивого множества формул логики предикатов до непротиворечивого  насыщенного множества). Еще более простой метод, использующий технику т.н.  модельных множеств, был разработан Я.Хинтиккой. Наличие свойств семантической  непротиворечивости и полноты у первопорядкового исчисления предикатов  свидетельствует о том, что оно представляет собой адекватную формализацию  семантически построенной логики предикатов, т.е. что у важнейших понятий –  общезначимой формулы (закона логики) и логического следования (имеющего место  между посылками и заключением в корректном рассуждении) – имеются точные  синтаксические аналоги. Данное свойство, как уже было сказано ранее, отсутствует у  логики предикатов второго порядка. Исчисление предикатов (как первопорядковое, так и второпорядковое) обладает также  свойством синтаксической непротиворечивости, т.е. не существует формулы А, такой,  что |–А и |– А. Однако, в отличие от классического исчисления высказываний,  исчисление предикатов не является синтаксически полным (максимальным,  непополнимым), т.е. к нему можно присоединить в качестве новой аксиомы некоторую  недоказуемую формулу так, что полученная система окажется синтаксически  непротиворечивой. Синтаксическая неполнота исчисления предикатов имеет серьезное в  методологическом отношении следствие: обеспечивается возможность построения на базе данной логической системы нетривиальных прикладных теорий за счет присоединения их  собственных постулатов, не обладающих статусом логических законов. Особую важность применительно к логике предикатов имеет исследование проблемы  разрешения. А.Чёрчем был получен фундаментальный результат, свидетельствующий о  том, что в общем случае эта проблема не имеет решения: не существует алгоритма,  позволяющего для произвольной формулы языка логики предикатов решить вопрос о том, является ли она законом данной теории, т.е. любое адекватное понятие закона логики  предикатов существенным образом неэффективно, не содержит алгоритмической  процедуры распознавания элементов своего объема. Тем не менее в некоторых частных случаях проблема разрешения находит свое решение.  Установлено, напр., что логика предикатов разрешима относительно свойства «быть  общезначимой формулой на множестве с конечным числом элементов». Алгоритм  проверки формул логики предикатов на общезначимость в области, содержащей n  объектов, состоит в элиминации кванторов и преобразовании данной формулы в формулу  языка логики высказываний (для последнего проблема разрешения решена). При  устранении кванторов общности и существования используется их связь с  пропозициональными связками конъюнкции и дизъюнкции, соответственно: если a1, а2,...,  аn – имена всех объектов данной конечной области, то утверждение ∀хА(х) эквивалентно  утверждению A(a1) ∧ А(a2) ∧... ∧  (Α αn), а ∃хА(х) эквивалентно  (Α a1)∨ (Α a2)∨...∨ (Α an). Разрешимой является т.н. логика одноместных предикатов – фрагмент логики  предикатов, формулы которого не содержат предикаторных констант местности большей  1. Можно показать, что любая подобная формула с k предикаторными константами  универсально общезначима тогда и только тогда, когда она общезначима во всех конечных областях не более чем с 2k элементами (а этот вопрос, как уже было сказано, может быть  решен эффективным образом). Разрешающая процедура имеется также для некоторых типов формул, приведенных к  предваренной нормальной форме. Напр., вопрос об универсальной общезначимости  формул с кванторной приставкой ∃ 1α ∃α2..∃αn может быть сведен к вопросу о ее  общезначимости на одноэлементном множестве, подобный вопрос о формулах с  приставками ∀α1∀α2...∀αn и ∀α1∀α2...∀αn∃ß1∃ß2...∃ßm сводится к вопросу об  общезначимости на множестве из n элементов. Создание логики предикатов связано с именами Г.Фреге, Б.Рассела и А.Уайтхеда.  Современные формулировки классического первопорядкового исчисления предикатов и  его детальный анализ был осуществлен Д.Гильбертом и его учениками В.Аккерманом и  П.Бернайсом. Большую роль в оформлении точной теоретико­множественной семантики  логики предикатов сыграли работы А.Тарского. Значительный вклад в установление  метатеоретических свойств логики предикатов внесли Л.Лёвингейм,  Т.Сколем, К.Гёдель, А.Чёрч, Ж.Эрбран, Л.Генкин. Серьезные научные результаты в  данной области были получены также Г.Генценом, Л.Кальмаром, С.Клини,  В.Крейгом, У.Куайном, А.А.Марковым, А.И.Мальцевым, П.С.Новиковым, В.А.Смирновым, К.Шютте и многими другими  исследователями. Литература: 1. Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947; 2. Предикатов исчисление (Есенин­Вольпин А.С.). – В кн.: Философская  энциклопедия, т. 4. М., 1967; 3. Клини С.К. Введение в метаматематику. М., 1957; 4. Мендельсон Э. Введение в математическую логику. М., 1976; 5. Новиков П.С. Элементы математической логики. М., 1973; 6. Смирнов В.А. Формальный вывод и логические исчисления. М., 1972; 7. Чёрч А. Введение в математическую логику, т. I. М., 1960; 8. А philosophical companion to first­order logic, ed. R.I.G.Hughe, 1993; 9. From Frege to Gödel: A source book in mathematical logic 1879–1931, Harvard  University Press, 1967; 10.Smullyan R.M. First­order Logic. N. Y., 1968. В.И.Маркин Свойства формализованного исчисления предикатов Формализованное исчисление предикатов (ФИП) развито достаточно глубоко, и теперь,  как и в случае формализованного исчисления высказываний, надлежит рассмотреть  свойства (или метатеорию) этого исчисления. Но теперь в области предикатов логика  достигает такой выразительной силы, что становится логическим основанием конкретных  математических теорий, и теоремы (по сути, метатеоремы) о логике рассуждений  достигают поистине философской глубины. Оправданность аксиоматизации , то  , т.е. из  Теорема оправданности аксиоматизации утверждает, что если  синтаксической выводимости следует семантическая выводимость. Ее очевидным  следствием будет утверждение о том, что всякая теорема ФИП является общезначимой  формулой (тавтологией) логики предикатов. Смысл этой теоремы состоит в утверждении  фактически того, что мы не были "излишне щедры" в выборе аксиом и правил вывода для  нашего формального исчисления и не включили в их число ничего лишнего, ибо  доказуемыми в этом исчислении оказываются лишь общезначимые формулы логики  предикатов. Доказательство этой теоремы не очень сложное, и мы получим ее в качестве  следствия несколько более общей теоремы. Обратное же утверждение "если  то  скромности", и для всякой общезначимой формулы логики предикатов в нашем ФИП  вполне достаточно формальных средств, чтобы доказать ее), уже не столь очевидно, и  доказательство его, приводимое дальше, потребует от нас значительно больших усилий.  (т.е. при выборе аксиом и правил вывода мы не проявили и "излишней  ,  Теорема оправданности имеет глубокий смысл: она оправдывает наши занятия  математикой, убеждая в том, что наши логические рассуждения и умопостроения не  уводят нас от смысла и от практики. Теорема 29.1. Если в алгебраической системе  множества  в   и из   и  .  синтаксически выводима формула  , то   также выполняется   выполняются все формулы из  Доказательство разделим на три этапа. На первом этапе отметим, что каждая аксиома  ФИП есть тождественно истинная формула. Что касается аксиом   исчисления  высказываний, то их тождественная истинность установлена нами в алгебре высказываний (см. теоремы 3.1 з, 3.3, а, л). Общезначимость аксиом  21.13.  установлена в теореме   и На втором этапе покажем, что все три правила вывода, используемые в ФИП, обладают  следующим семантическим свойством. Если алгебраическая система  для всех посылок правила вывода, то  данных формул с помощью данного правила вывода. Докажем это утверждение для трех  из правил вывода.  будет моделью и для формулы, получаемой из   служит моделью  Правило MP. Допустим, что  любую подстановку  высказываний  результате подстановки предметных констант  и высказывание   констант из  , то есть   и   и  . Докажем, что тогда  . Возьмем  . Тогда, по условию, каждое из  , получаемых соответственно из формул   в  , будет истинным. Тогда истинным будет   и  . Это и означает, что  . , где  ) высказывание  ∀­правило. Допустим, что  а   обозначает все свободные предметные переменные в формулах  Тогда сделанное допущение означает, что для любых элементов  носитель алгебраической системы  Рассмотрим теперь высказывание  при любом  истинно. Если же  высказывание  вытекает истинность для таких  влечет истинность высказывания  истинно. Итак, высказывание  означает, что  . В самом деле, если   высказывания   для тех  .  и покажем, что оно истинно в   ложно, то рассматриваемое высказывание   истинно, то, по отмеченному выше, истинным будет и  . Поскольку оно будет истинным при любом  , то отсюда   не входит свободно в формулу  ,   — кроме  ).  и   (в   (где   истинно в   —  .  . Это, в свою очередь,    , для которых  . Это и   истинно для любых  ∃­правило. Подобно предыдущему правилу, доказывается, что если  то  . , (в частности,  формулы  .  . Если   и   из множества  ). Покажем, что каждый элемент этой   формулы в рассматриваемом выводе. При  , если   — аксиома, то она общезначима и, в частности,  Наконец, на третьем этапе докажем утверждение самой теоремы. Пусть  Последнее означает, что имеется вывод  формул  последовательности является формулой, выполняющейся в  индукцией по номеру  по условию,  Предположим теперь, что при всех  есть  . Рассмотрим формулу  выше,  одному из трех правил вывода, то (на основании выполнимости всех предыдущих формул  в  есть  последовательности  доказана. . Доказательство проведем  , то,  .  , то   получена из предыдущих формул последовательности по  ) в силу утверждений (см. второй этап) заключаем, что и  . Окончательно заключаем, что все формулы   все формулы   выполняются в   или   — аксиома, то, как отмечено  истинны в  , в частности  . Теорема полностью . Если  . Если же   выполняется в  , то  Следствие 29.2 (теорема оправданности). Из синтаксической выводимости следует  семантическая выводимость, т. е. если  , то  . Доказательство. Пусть   и пусть  выполняются все формулы из , то есть  определению семантического следствия это и означает, что   — любая алгебраическая система, в которой  . По  . Тогда по доказанной теореме  . Следствие 29.3. Всякая доказуемая формула является общезначимой (т.е. любая  теорема истинна): если  , то  . Доказательство получается из предыдущего следствия при  . Непротиворечивость формализованного исчисления предикатов Важнейшим компонентом критерия оправданности всякой математической теории  является ее непротиворечивость, т.е. невозможность доказательства в ней некоторого  утверждения и его отрицания одновременно. Трудности, связанные с доказательством  этого свойства математических теорий (а одной из причин этих трудностей, несомненно,  было отсутствие в содержательных математических теориях точного понятия  доказательства), привели к тому, что в математике более естественным стал другой  признак непротиворечивости теории, основанный на возможностях реализации этой  теории, ее моделируемости. Но в то же время этот подход и привел к возникновению  парадоксов в математике, которые, в свою очередь, привели к возникновению науки об  основаниях математики и к концепциям формального подхода к понятиям доказательства и математической (аксиоматической) теории. Одной из задач этого подхода была  выработка такого формального понятия доказательства, при котором для конкретной  математической теории понятие ее формальной непротиворечивости совпало бы с  понятием ее содержательной непротиворечивости. Факт такого совпадения, в силу  точности определения доказательства, становится математической теоремой (точнее,  метатеоремой). Отметим, что привыкание в математике к эквивалентности этих двух  понятий непротиворечивости было непростым. В частности, неприятие современниками  неевклидовых геометрий Лобачевского–Бояи объясняется также и тем, что законность  этих теорий обосновывалась отсутствием в них противоречий — аргументом,  совпадающим по существу с современным понятием формальной непротиворечивости.  Геометрические модели для этих теорий, доказывающие их содержательную  непротиворечивость, были найдены позднее. Наша задача состоит в том, чтобы в рамках формализованного (узкого) исчисления  предикатов дать точные определения двух понятий непротиворечивости и установить их  эквивалентность. Напомним, что формула логики предикатов называется общезначимой, если она истинна в любой интерпретации, и противоречивой, если она ложна в любой интерпретации, т.е.  если ее отрицание общезначимо. Эти семантические понятия, связывающие  непротиворечивость с истинностью, позволяют сформулировать понятие семантически  непротиворечивой теории. Определение 29.4. Формальная теория называется семантически непротиворечивой,  если ни одна из ее теорем (формул) не является противоречивой, т. е. ложной при  любой ее интерпретации. Аналогично, множество  семантически непротиворечивым, если ни одна формула, выводимая из  является противоречивой.  формул называется  , не  В теореме 16.1 доказано, что всякая теорема формализованного исчисления высказываний общезначима (тождественно истинна), а потому не является противоречивой. Это  означает, что формализованное исчисление высказываний семантически непротиворечиво. Аналогичная теорема доказана и для формализованного исчисления предикатов (см.  следствие 29.3 из теоремы 29.1 выше). Значит, и ФИП семантически непротиворечиво.  Семантическая непротиворечивость ФИВ и ФИП означает, что эти формальные теории  пригодны для описания любых классов алгебраических систем, т.е. они войдут в теории  этих классов составными частями, что вполне соответствует общенаучному принципу  универсальности законов логики (Лейбниц формулировал его как выполнимость  логических законов "во всех мыслимых мирах").  есть теория множества   всех своих моделей, а  , т.е. для   семантически непротиворечива, если и только если   существует модель. Если отождествить пригодность математической теории, ее  Произвольная формальная теория  значит, теория  теории  целесообразность с ее семантической непротиворечивостью, то можно сказать, что  сформулированный критерий пригодности теории известен уже давно. Отыскание модели  для теории до возникновения оснований математики было единственным общепризнанным методом доказательства "законности" теории. Математическая логика выработала аналог  этого критерия, не опирающийся на наличие модели теории — внешний фактор по отношению к теории, а опирающийся на внутренние свойства самой теории, — понятие  синтаксической непротиворечивости теории.  называется синтаксически (или дедуктивно, Определение 29.5. Формальная теория  или формально) непротиворечивой, если не существует такой формулы  являются теоремами теории   невыводимыми являются одновременно  формула и ее отрицание. Аналогичное определение можно сформулировать и для  произвольного множества  непротиворечивым, если из   формул:   невыводимы одновременно формула и ее отрицание.  называется синтаксически  , т.е. в  , что   и    В теореме 16.9 доказана синтаксическая непротиворечивость формализованного  исчисления высказываний. Аналогично доказывается следующая теорема. Теорема 29.6. Формализованное исчисление предикатов синтаксически  непротиворечиво. Доказательство. Допустим противное, т.е. предположим, что ФИП синтаксически  противоречиво. Значит, найдется такая формула  Тогда по следствию 29.3 из теоремы 29.1 формулы Fa ­,Fбудут общезначимыми, что  невозможно на основании определения общезначимости. будут теоремами ФИП.  , что   и  Теперь перейдем к установлению взаимосвязей между понятиями семантической и  синтаксической непротиворечивости. Наша задача состоит в том, чтобы доказать их  эквивалентность. Начнем с достаточно простой, но важной леммы. Лемма 29.7. Если множество формул имеет модель, то это множество  семантически непротиворечиво. Доказательство. Если множество  выводимая из  противном случае она была бы ложна и в  означает, что   семантически непротиворечиво. , не является противоречивой, т.е. ложной во всякой интерпретации, ибо в   (что невозможно в силу теоремы 29.1). Это и   формул имеет модель  , то ни одна формула,  Теорема 29.8. Если множество формул семантически непротиворечиво, то оно  синтаксически непротиворечиво.  формул узкого исчисления  Доказательство. Допустим, что некоторое множество  предикатов семантически непротиворечиво, но противоречиво синтаксически.  Следовательно, из него выводима некоторая формула  выводима и их конъюнкция (по правилу введения конъюнкции)  ложна в любой интерпретации, что означает, что множество  противоречиво. Получаем противоречие, доказывающее, что  непротиворечиво.  семантически   синтаксически   и ее отрицание  . Но тогда из  . Но эта формула    Непосредственно из предыдущих леммы и теоремы вытекает такое следствие. Следствие 29.9. Если множество формул имеет модель, то оно синтаксически  непротиворечиво. Теорема Гёделя о существовании модели Утверждение, обратное следствию, также оказывается справедливым. Но с  конструктивной точки зрения оно оказывается более глубоким. Смысл его состоит в том,  что всякое множество формул не только имеет модель, но эту модель можно  конструктивно построить. Доказательство этого факта как раз и заключается в изложении метода такого построения. Это еще одна из замечательных теорем Гёделя (теорема о  существовании модели), относящаяся к важнейшим теоремам математической логики.  Она доказана Гёделем в 1930 г. Теорема 29.10 (теорема Гёделя о существовании модели). Любое синтаксически  непротиворечивое множество  сигнатуры   замкнутых формул узкого исчисления предикатов   имеет модель. ▼  Доказательство Теоремы о непротиворечивости формул предикатов Теорема Гёделя о существовании модели позволяет доказать теорему, обратную к  теореме 29.8, и они вместе образуют следующую важную метатеорему. Теорема 29.11 (о непротиворечивости). Множество формул узкого исчисления  предикатов семантически непротиворечиво тогда и только тогда, когда оно  синтаксически непротиворечиво. Доказательство. Необходимость есть теорема 29.8. Обратно, если множество формул  синтаксически непротиворечиво, то по теореме 29.10 оно имеет модель, а тогда по лемме  29.7 оно семантически непротиворечиво. Наконец, объединим в одну метатеорему следствие из теоремы 29.8 и теорему 29.10.  Получим следующее. Теорема 29.12 (о непротиворечивости). Множество формул узкого исчисления  предикатов синтаксически (дедуктивно) непротиворечиво тогда и только тогда,  когда оно имеет модель. Приведем интересный комментарий, который дает теореме о непротиворечивости  известный логик Р. Линдон, по мнению которого доказательства (дедуктивной)  непротиворечивости какой­либо теории посредством указания ее модели широко  распространены в абстрактной математике. Менее очевидное из утверждений теоремы о  непротиворечивости — о существовании модели у каждой дедуктивно непротиворечивой  теории — используется далеко не так часто. Возможно, это объясняется тем, что  математики не слишком­то большое значение придают понятию существования; теорему о непротиворечивости можно как раз и рассматривать как скромное, но зато точное  выражение довольно­таки расплывчатого мнения, что существование в математике — это  не что иное, как непротиворечивость. Возможности применения теоремы о непротиворечивости к проблемам установления  непротиворечивости конкретных теорий весьма ограниченны: дело в том, что построение  модели обычно требует принятия в метаязыке допущений, значительно более сильных,  нежели те, которые выражаются предметной теорией. Другой путь установления  непротиворечивости какой­нибудь аксиоматической теории состоит в том, чтобы с  помощью чисто синтаксических рассмотрений показать, что в данной теории нельзя доказать тождественно ложную формулу. Область применения этого метода, однако,  также невелика. Теорема Гёделя не позволяет надеяться на получение доказательства  непротиворечивости теории, если не допускать в теории, предназначенной для такого  доказательства на метаязыке, по меньшей мере столь же сильных средств, что и в  рассматриваемой предметной теории. Убеждение в непротиворечивости достаточно  сложных математических теорий базируется в конечном счете на интуиции и опыте. Полнота и адекватность формализованного исчисления предикатов  противоречиво. Допустим на время, что это не так. Тогда по теореме  . Покажем, что тогда множество  Доказав теорему Гёделя о существовании модели (теорема 29.10), можно доказать  теорему, обратную теореме оправданности (следствие 29.2 из теоремы 29.1), т.е.  утверждение о том, что из семантической выводимости следует синтаксическая  выводимость. В самом деле, пусть  формул  29.10 это множество имеет модель  из  . Из последнего, ввиду условия  Получаем противоречие. Итак, множество  выводима любая формула, в частности  имеем  теоремой ФИВ, по правилу MP заключаем, что   противоречиво. Значит, из него  . Тогда по теореме о дедукции   является  . Учитывая, что, кроме того, формула  , т.е. на  выполняется формула  , следует, что на   выполняется и формула   и все формулы  .  . Итак, мы доказали, что если  29.1 из теоремы 29.2, приходим к следующей важной метатеореме. , то  . Объединив это утверждение со следствием  Теорема 29.13 (теорема адекватности). Формула  множества формул  из  .  синтаксически выводима из   тогда и только тогда, когда она семантически выводима Если теорема оправданности означала, что при выборе аксиом и правил вывода мы не  были слишком щедры (настолько, что сможем доказать лишь общезначимые формулы), то  обратная теорема — теорема адекватности — означает, что при этом выборе мы не были  и излишне скупы (ровно настолько, что сможем доказать всякую общезначимую  формулу). Заметим, что нетрудно показать, что теорема о существовании модели вытекает из  теоремы адекватности. В самом деле, предположим, что  множество формул, не имеющее модели. Тогда ясно, что для любой формулы  справедливо семантическое следование  следует, что  противоречие с условием.  — непротиворечивое    . В силу теоремы адекватности отсюда   для любой  , что означает противоречивость множества  , в  Теорема 29.14 (теорема Гёделя о полноте ФИП). Класс доказуемых замкнутых  формул совпадает с классом общезначимых (или тождественно истинных)  формул:  . Доказательство. Эта теорема непосредственно вытекает из предыдущей при  .  — свободные предметные переменные в формуле  Справедлива она и для открытых формул. В самом деле, если  где  квантора общности это будет равносильно тому, что  теореме 29.14 это равносильно тому, что  выводимости последнее утверждение равносильно тому, что  ,  , то в силу определения  . По  . В силу свойств  . Неполнота формализованного исчисления предикатов в абсолютном и узком  смыслах В учебнике обсуждаются два понятия полноты аксиоматической теории: абсолютная  полнота и полнота в узком смысле (см. определение 27.6). Доказанная теорема 29.14  может быть истолкована как некая внешняя полнота формализованного исчисления  предикатов, его полнота относительно логики предикатов: в этой теории могут быть  формально доказаны все общезначимые формулы логики предикатов. Рассмотрим  вопросы внутренней полноты формализованного исчисления предикатов, т.е. выясним,  будет ли эта теория абсолютно полной и полной в узком смысле (см. определения 27.5 и  27.6). Поскольку на основании теоремы 29.14 множество теорем формализованного  исчисления предикатов совпадает с множеством тавтологий (общезначимых формул)  логики предикатов, а в логике предикатов существуют выполнимые, но не общезначимые  формулы, формализованное исчисление предикатов не является абсолютно полной  теорией. Здесь ситуация аналогична соответствующей ситуации в формализованном  исчислении высказываний. Что же касается полноты формализованного исчисления  предикатов в узком смысле, то исчисление предикатов (в отличие от исчисления  высказываний, см. теорему 28.4) таким свойством не обладает. Для доказательства  приведем пример формулы, не являющейся теоремой формализованного исчисления  предикатов, добавление которой к аксиомам исчисления предикатов (с сохранением  правил вывода) приводит к непротиворечивой формальной аксиоматической теории. Пример 29.15. Рассмотрим формулу  . Нетрудно убедиться в  том, что она не является общезначимой (приведите пример конкретного одноместного  предиката, превращающего эту формулу в ложное высказывание). Поэтому на основании  теоремы К. Гёделя о полноте она не доказуема в формализованном исчислении  предикатов. С другой стороны, добавив к аксиомам формализованного исчисления  предикатов рассматриваемую формулу, получим непротиворечивую формальную  теорию  . Ее непротиворечивость можно доказать следующим образом. Рассмотрим модель этой теории на одноэлементном множестве  данная формула тождественно истинна на  определить для каждого натурального  причем  новой теории  истинных на  образом, доказывается утверждение: всякая теорема теории  одноэлементном множестве   и  . . Далее, учитывая, что на   лишь два n­местных предиката  . Ясно, что   можно  ,   и   тождественно истинны на этой модели и правила вывода от тождественно   формул приводят к тождественно истинным на   формулам. Таким  , нетрудно доказать, что все аксиомы   тождественно истинна на  Следовательно, если бы для некоторой формулы  теории  невозможно. Поэтому расширенная теория  неполноту в узком смысле формализованного исчисления предикатов. , то они были бы тождественно истинны на одноэлементном множестве   непротиворечива, что и доказывает   обе формулы   и   были теоремами  , что  Теорема компактности Мы уже отмечали (см. теорему 15.3, б) и неоднократно использовали тот простой факт,   тогда и только  непосредственно вытекающий из определения понятия вывода, что  тогда, когда   формул.  Теорема адекватности, установленная на основании выдающейся теоремы Гёделя о  существовании модели, позволяет получить из этого тривиального соображения  аналогичную теорему семантического содержания, уже отнюдь не столь очевидную.  — некоторое конечное подмножество множества  , где  Теорема 29.16 (теорема К. Гёделя–А. И. Мальцева). Если  конечного подмножества   имеет место  . , то для некоторого Доказательство. Если  , то по теореме 29.13 (теорема адекватности)  сделанного перед настоящей теоремой замечания найдется такое конечное  подмножество  теоремы 29.1) заключаем, что  , что  . . Отсюда по теореме оправданности (следствие 29.2 из  . В силу  Следствие 29.17(локальная теорема К. Гёделя—А. И. Мальцева). Множество  замкнутых формул узкого исчисления предикатов сигнатуры  только тогда, когда каждое его конечное подмножество имеет модель.  имеет модель тогда и     имеет модель. Тогда  Доказательство. Необходимость очевидна. Обратно, пусть каждое конечное  подмножество множества  (Если бы это было не так, то для некоторой формулы  и  и   было бы синтаксически противоречиво, а значит, по теореме 29.12  не имело бы модели, что противоречило бы условию.) Следовательно, по теореме 29.10 о  существовании модели множество  , а значит, нашлось бы такое конечное подмножество  , то есть   имелись бы выводимости     — синтаксически непротиворечиво.   имеет модель. Следствие доказано. , что   В заключение приведем еще одну теорему о формулах узкого исчисления предикатов и их моделях. Теорема 29.18 (Лёвенгейм–Сколем). Пусть  замкнутых формул узкого исчисления предикатов сигнатуры  то   — счетная сигнатура и  . Если   имеет счетную модель.  — множество  имеет модель,  Доказательство. Пусть  имеет модель. Тогда (по теореме 29.12)  множества формул может быть построена, как в доказательстве теоремы 29.10.  Построенная таким образом модель будет счетной: она состоит из   и множество   синтаксически непротиворечиво и модель этого   формул элементов  из констант   и всех термов (не содержащих переменных), построенных  . Эти термы можно занумеровать, например, по следующему правилу: где   — последовательность простых чисел. Эта теорема может быть доказана и в более общей мощностной формулировке: если  множество   формул имеет бесконечную модель и мощность множества всех букв, из  которых составлены формулы из  , равна  существует модель множества  мощности  , то для любой бесконечной мощности  .   Укажем два следствия этой теоремы: 1) если  — множество формул мощности  бесконечные модели любых мощностей, превышающих  ; , имеющее бесконечную модель, то   имеет  2) всякое конечное множество или счетное непротиворечивое множество формул либо  имеет только конечные модели, либо имеет бесконечные модели любых мощностей. Теорема Лёвенгейма–Сколема дает ряд поразительных следствий двух типов: одни из них гласят, что некоторая теория имеет неожиданно обширные модели, другие — что теория  имеет неожиданно узкие модели. Дальнейшее развитие эта мысль получит в следующей  лекции.