Дискретно-непрерывная математика (стр. 10 )

Формула А называется истинной (в данной интерпретации) т. т.т., когда она выполнена на всякой последовательности из ∑.

Формула А называется ложной (в данной интерпретации), если она не выполнена ни на одной последовательности из ∑.

Данная интерпретация называется моделью для данного множества формул Г, если каждая формула из Г истинна в данной интерпретации.

Из этих определений, например, следует: если в данной интерпретации истинны А и то истинно и В; А истинно в данной интерпретации т. т.т., когда в этой интерпретации истинно

Формула А называется логически общезначимой (в исчислении предикатов), если она истинна в каждой интерпретации. (В дальнейшем слова «в исчислении предикатов» будем опускать.) Формула А называется выполнимой, если существует интерпретация, в которой А выполнима хотя бы на одной последовательности из ∑.

Формула А называется противоречием, если формула является логически общезначимой или, что то же самое, если формула А ложна во всякой интерпретации.

Говорят, что формула А логически влечет формулу В, если в любой интерпретации формула В выполнена на всякой последовательности, на которой выполнена формула А. (В общем случае говорят, что формула В является логическим следствием множества Г формул, если во всякой интерпретации формула В выполнена на каждой последовательности, на которой выполнены все формулы из Г.)

Как и в логике высказываний, формула А логически влечет формулу В т. т.т., когда формула логически общезначима.

Логически общезначимые формулы называются законами логики предикатов. Среди них — всякий частный случай произвольной тавтологии логики высказываний (т. е. результат замещения в ней пропозициональных переменных формулами языка логики предикатов). Приведем еще два примера общезначимых формул:

(I) если формула А не содержит

свободных вхождений х;

(ІІ) если терм t свободен для х в А(х).

Как отмечается в [Мендельсон 1984], аксиоматический метод был роскошью при изучении пропозиционального исчисления в силу его простоты и тривиального способа проверки, является ли данная пропозиционльная формула тавтологией, но представляется необходимым при изучении формул, содержащих кванторы. В качестве исходных логических связок возьмем а в качестве квантора Тогда в качестве пропозициональной части можно взять аксиоматизацию С2, предложенную Лукасевичем (см. выше раздел 1.5). Однако в силу сложности формулировки правил подстановки для исчисления предикатов обычно берутся схемы аксиом, каждой из которых соответствует бесконечное число аксиом одного и того же типа. К этим трем схемам аксиом добавляются две только что приведенные общезначимые формулы (I) - (II) с указанными ограничениями. Правилами вывода являются (і) modus ponens и (ii) правило обобщения: из А следует

Теорема дедукции для пропозиционального исчисления без соответствующей модификации не может быть проведена для первопорядковой логики. Например, для любой формулы

А, но не всегдаОднако некоторые слабые варианты

теоремы дедукции могут быть доказаны, например,

если формула А замкнута ито

1.6.3. Основные свойства: полнота, теорема Линдстрёма, неразрешимость

Если с доказательством непротиворечивости (не существует формулы А такой, что трудностей не возникало, то

проблема о полноте оказалась намного сложнее.

Только в 1928 г. в книге Д. Гильберта и В. Аккермана (см. рус­ский перевод 2-го издания, значительно переработанного [Гильберт и Аккерман 1947]) окончательно оформилась концепция первопорядковой логики, или чистой теории квантификащш с кванторами «все» и «некоторые» и была поставлена проблема о доказательстве ее полноты. Эта проблема была решена К. Гёделем в 1930 г., хотя к 1928 г. это доказательство уже имелось у Т. Скулема :

Во всяком исчислении предикатов первого порядка теоремами являются все те и только те формулы, которые логически общезначимы.

Пусть Т есть первопорядковая теория, т. е. множество предложений в языке логики предикатов, замкнутое относительно отношения выводимости. Имеют место два важнейших теоретико-модельных свойства теорий в первопорядковом языке.

Теорема компактности (для счетных языков). Если каждое конечное множество предложений в Т имеет модель, то Т имеет модель,

Компактность имеет место, поскольку во всех выводах используется только конечное множество посылок. Это свойство было уже выявлено К. Гёделем в работе о полноте логики предикатов. Позже (1936) было дано «чисто семантическое» доказательство этой теоремы. ,

Ранее было доказано другое важное свойство первопорядковой логики (1915,1919):

Теорема Лёвенгейма-Скулема. Если Т имеет бесконечную модель, то Т имеет модель любой бесконечной мощности τ, большей или равной мощности теории Т.

Понадобилось продолжительное время, пока П. Линдстрём [Lindstrom 1969] установил, что эти свойства являются характеристическими для первопорядковой логики в следующем смысле:

Теорема Линдстрёма. Логика первого порядка является единственной логикой, замкнутой относительно и

удовлетворяющей теоремам компактности и Лёвенгейма-Скулема

По существу теорема Линдстрёма дает определение первопорядковой логики в терминах ее глобальных свойств и с этими свойствами она является уникальной. Не имеет значения, как мы будем расширять первопорядковую логику - в любом случае теря­ется или свойство компактности, или свойство Лёвенгейма-Ску­лема, или оба вместе. Уже второпорядковая логика, допускающая квантификацию по подмножествам, отношениям и функциям, кроме указанных свойств теряет также свойство полноты.

Первоначально результат Линдстрёма не привлек к себе особого внимания, о чём говорит издание в 1973 г. знаменитой книги Г. Кейслера и (см. русский перевод [Кейслер и Чэн 1977]), где эта теорема вообще не обсуждается. Не обсуждается эта теорема и в [Мендельсон 1984]. Только в третьем издании [Chang and Keisler 1990] уже в предисловии говорится, что этот результат является отправной точкой для развития абстракт­ной теории моделей и вводится новый раздел (2.5), где дается определение «абстрактной логики» как пары классов (l, ), где l есть класс предложений и l есть отношение выполнимости (satis­faction), удовлетворяющее определенным условиям. Наиболее известным примером абстрактной логики как раз и является обычная первопорядковая логика, которая обозначается посред­ством lω, ω.

Теорий первого порядка хватает для выражения многих известных математических теорий и, более того, большинство теорий высших порядков может быть подходящим образом «погружено» в язык первого порядка. Например, многосортная первопорядковая логика, которая также используется при изучении многозначных логик, является переинтерпретацией второпорядковой логики или даже логики высших порядков в первопорядковую с различными видами объектов. (В отличие от однооортной первопорядковой логики, рассмотренной здесь, где все переменные принадлежат к одному и тому же типу, в многосортной логике с каждой переменной связывается собственное множество ее возможных значений. )

Редукция к первопорядковой логике настолько сильна, что мы приходим к рекурсивно-аксиоматизируемому множеству истин.

Очень полезным является расширение первопорядковой логики введением отношения равенства между индивидами. Пусть Т — теория первого порядка, в числе предикатных букв которой имеется Р12. Будем сокращенно писать t = s вместоТеория Т называется теорией первого порядка с равенством, если следующие формулы являются теоремами Т:

— рефлексивность равенства;

— подстановочность равенства,

где х и у - предметные переменные, Р(х, х) — произвольная формула, а Р(х, у) получается из Р(х, х) заменой каких-нибудь (не обязательно всех) свободных вхождений х вхождениями у, с соблюдением условия, чтобы у было свободно для тех вхождений х, которые заменяются.

Наконец, обратим внимание на еще одно фундаментальное свойство приведенного исчисления предикатов, которое относится к проблеме разрешимости, поставленной Д. Гильбертом в 1928 г. Эта проблема, по сравнению с аналогичной проблемой для исчисления высказываний, становится значительно сложнее, поскольку теперь уже приходится иметь дело с проверкой истинности общезначимой формулы в интерпретациях с областями сколь угодно большими конечными, а также бесконечными. А. Чёрч [Church 1936] и А. Тьюринг [Turing 1937] независимо друг от друга, опираясь на уточненное ими понятие вычислимой функции, доказали, что первопорядковое исчисление предикатов неразрешимо..