Логика предикатов как исчисление

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

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

Определение косвенного вывода в ЛП принципиально ничем не от­личается от подобного определения в ЛВ.

Если каждая ветвь дерева формулы (φ₁, φ₂, ..., φ_n&φ) замкнута, тогда формула φ косвенно выводима из последовательности формул φ₁, φ₂, ..., φ_n

Пусть α и β, как и прежде, обозначают посылки и заключение дока­зательства.

Доказательством заключения β в исчислении ЛП называется вывод β из множества посылок α

Напомним, что доказательство заключения β считается косвенным (от противного), если построен косвенный вывод β из множества посы­лок α.

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

Правила конструирования деревьев в логике предикатов

Правила П*1 - П*12 такие же, как и правила П1 - П12 в логике вы­сказываний.

П*13. Если формула имеет вид φξ, где переменная ξ является связанной, тогда дерево, в которое она входит, начинается или продолжается в каждой своей ветви формулой фа или формулой φf _tn,где константа а и функция f _nуже входят в рассматрива­емую ветвь дерева:

П*14. Ветвь дерева формулы логики предикатов замкнута, если и только если она содержит хотя бы одну формулу ЛП вместе со сво­им отрицанием или хотя бы один n-местный предикатный знак Pⁿ вместе со своим отрицанием - Pⁿтакие, что каждый из них содер­жит n связанных переменных (не обязательно различных), а если кроме связанных переменных имеются также константы или функ­циональные знаки, то знаки Pⁿи - Pⁿв результате правильных под­становок термов вместо связанных переменных могут быть приве­дены к виду P_{t1 n}и - P_{t1 n}(порядок следования термов является существенным). Замкнутые ветви отмечаются знаком *.

П*15. Процесс конструирования дерева формулы начинается с представления подформул, соединяемых главным логическим оператором формулы, и продолжается до тех пор, пока все ее под­формулы не будут представлены в виде ветвей дерева, содержащих только атомарные формулы вида P_{t1 n}или их отрицания.

Правила П*1 - П*12 ничем не отличаются от соответствующих пра­вил логики высказываний. Правило П*13 позволяет проверить, представ­ляют ли ранее введенные термы (константы и функции) расширение фор­мулы со связанной переменной. Правило П*14 обобщает определение замкнутой ветви.

Пример 1

1. Умозаключение: «Некоторые люди тщеславны. Никто не любит тщеславных. Следовательно, некоторых людей никто не любит».

2. Формализация посылок и заключения: U = «люди», Px = «х тще­славен», Qxy = «х любит у».

3. Отрицание заключения:

4. Исключение (снятие) кванторов, знака импликации (знак сим­волизирует этапы и результаты исключения):

5. Дерево косвенного доказательства:

Переменные х и у связаны кванторами общности (x) и (у). Они ис­тинны для любого значения х и у. Значит, допустима подстановка любых термов вместо х и у в дерево доказательства. Для проверки подставляем прежде всего те термы, которые уже входят в дерево доказательства. Вер­шина дерева рассматриваемого доказательства содержит такие термы, как а и f (x). Подставляя константу а и предметную функцию f (x) вместо переменных х и у, видим, что все ветви дерева исследуемого умозаклю­чения оказались замкнутыми. Следовательно, отрицание заключения не­совместимо с посылками. Значит, рассматриваемое умозаключение об­щезначимо.

Пример 2

1. Умозаключение: «Всякий восхищается каким-нибудь артистом. Каждый, кто восхищается кем-либо, уважает его. Следовательно, сущес­твуют люди, которые уважают какого-нибудь артиста».

2. Формализация посылок и заключения: U = «люди», Рху= «х восхи­щается у», Qy = «у - артист», Rxy = «х уважает у».

(х) (Ey) (Qy&Pxy), (x) (y) (Pxy⊃Rxy) I- (Еу) (Ех) Q &Rxy).

3. Отрицание заключения:

4.

5. Дерево косвенного доказательства:

Подстановка предметной функции f (x) вместо связанной переменной у делает все ветви дерева рассматриваемого умозаключения замкнутыми. Следовательно, отрицание заключения несовместимо с посылками. Зна­чит, данное умозаключение общезначимо.

Пример 3

1. Умозаключение: «Автомобиль - достижение научно-технического прогресса. Следовательно, колесо автомобиля - колесо достижения науч­но-технического прогресса».

2. Формализация посылок и заключения: U = «достижения», Рх= «х - автомобиль», Qγ = «у - достижение научно-технического прогрес­са», Яху= «х есть колесо у».

3. Отрицание заключения:

4. Исключение (снятие) кванторов, знака импликации:

5. Дерево косвенного доказательства:

Последовательная подстановка константы bвместо переменных zи у делает все ветви дерева рассматриваемого умозаключения замкнутыми. Следовательно, отрицание заключения несовместимо с посылками. Зна­чит, данное умозаключение общезначимо.

Пример 4

1. Умозаключение: «Каждый любит того, кто в кого-нибудь влюблен. Татьяна Ларина любит Евгения Онегина. Следовательно, все любят Тать­яну Ларину».

2. Формализация посылок и заключения: U = «люди», Pху= «х любит у», a = «Татьяна Ларина», b = «Евгений Онегин».

3.

4. Исключение (снятие) кванторов, знака импликации:

5. Дерево косвенного доказательства:

Подстановка констант а, bи с вместо переменных у, zи х соответс­твенно делает все ветви дерева рассматриваемого умозаключения замкну­тыми. Следовательно, отрицание заключения несовместимо с посылками. Значит, исследуемое умозаключение общезначимо.

Пример 5

1. Умозаключение: «Человек, который написал “Приключения Алисы в стране чудес”, сочинял только необыкновенные сказки. Следовательно, “Приключения Алисы в стране чудес” - необыкновенная сказка».

2. Формализация посылок и заключения: U = «вещи», а= «Приклю­чения Алисы в стране чудес», Рх= «х - человек», Оха= «х написал а», Их = «х - необыкновенная сказка».

3. Отрицание заключения: - Ra.

4. Исключение (снятие) кванторов, знака импликации:

5. Дерево косвенного доказательства:

Одновременная подстановка констант а и bвместо переменных zи у соответственно делает все ветви дерева анализируемого умозаключения замкнутыми. Следовательно, отрицание заключения несовместимо с по­сылками. Значит, проверяемое умозаключение общезначимо.

Пример 6

1. Умозаключение: «Каждый читающий больше других, умнее, чем все остальные. Существует некто, отличный от всех остальных, который читает больше всех. Следовательно, существует некто, отличный от всех остальных, который умнее всех».

2. Формализация посылок и заключения: U = «вещи», Pxy = «х читает больше, чем у»; Qxy = «х умнее, чем у».

3. Отрицание заключения:

4. Исключение (снятие) кванторов, знака импликации:

5. Дерево косвенного доказательства:

Подстановка константы а и предметной функции f(а) вместо пере­менных xи yсоответственно делает все ветви дерева анализируемого умозаключения замкнутыми. Следовательно, отрицание заключения не­совместимо с посылками. Значит, данное умозаключение общезначимо.

Пример 7

1. Умозаключение: «Каждый, кто читает книги, приобретает новые знания. Следовательно, если не существует новых знаний, значит никто не читает никаких книг».

2. Формализация посылок и заключения: U = «вещи», Py = «y- книги», Qxy = «х читает y», Rz = «z- новые знания», Sxz = «xприобретает z».

3. Отрицание заключения:

4. Исключение (снятие) кванторов, знака импликации:

5. Дерево косвенного доказательства:

Одновременная подстановка константы aвместо переменных xи z, константы bвместо переменной yделает все ветви дерева анализируемо­го умозаключения замкнутыми. Следовательно, отрицание заключения несовместимо с посылками. Значит, анализируемое умозаключение об­щезначимо.

Следующие две теоремы доказывают, что всякая логически истинная формула ЛП является доказуемой в построенном исчислении (α обозна­

чает посылки доказательства, β - его заключение). Эти теоремы обобща­ют соответствующие теоремы 4 и 5 главы 4.

Теорема 5.Если можно построить замкнутое дерево формулы (α &- β), тогда вывод заключения β из посылок α является общезначимым.

Доказательство. Допустим, вывод заключения β из посылок α не общезначим и тем самым дерево формулы (α &-β) не замкнуто. Тогда существует по крайней мере одна ветвь, атомарные подформулы и/или их отрицания которой не противоречат друг другу и одновременно истинны. Так как ветвь не замкнута, а ее замыкание необходимо для доказательс­тва выводимости, она может быть далее продолжена с помощью правил конструирования деревьев П*1 - П*15 логики предикатов. Но каждое из правил П*1 - П*12 основано на определенном законе логики - принципе сохранения истины и по определению не может привести к замыканию ветви. Не может привести к замыканию дерева и применение правила П*13. Поскольку если выполняется формула (ξ)φξ, то ни один из ее при­меров вида φα, образующих расширение, не может противоречить ранее введенным формулам.

Следовательно, если ветвь не замкнута, то ни одно из указанных правил никогда не сделает ее замкнутой. Значит, если все ветви дерева формулы (α &-β) замкнуты, тогда не существует ни одной ветви, в кото­рой посылки α были бы истинны, а заключение β ложно. Следовательно, вывод любой тавтологии ЛП с помощью правил П*1 - П*15 всегда обще­значим. QED.

Теорема 6.Если можно построить незамкнутое дерево формулы (α &-β), тогда вывод заключения β из посылок α не общезначим.

Доказательство. Если вывод заключения β из посылок α общезна­чим, тогда, согласно теореме 5, дерево формулы (α &-β), построенное в соответствии с правилами П*1 - П*15, замкнуто. Не существует ни од­ной ветви дерева, в которой были бы одновременно истинны множества формул α и -β. Следовательно, если дерево формулы (α &-β) не за­мкнуто, тогда вывод заключения β из посылок α не является общезначи­мым. QED.

Теоремы 5 и 6 вместе говорят о необходимости и достаточности пра­вил П*1 - П*15 для вывода тавтологий ЛП. Значит, множество этих пра­вил является полным.

7.7.