Похожие работы
|
2. элементы логики предикатов формулы логики предикатов и их преобразование - страница №3/4
3.2. Общее представление об исчислении предикатовСводка теорииАксиоматический метод, без которого можно было обойтись (ввиду наличия эффективного метода истинностных таблиц) при рассмотрении исчисления высказываний, становится необходимым для изучения формул, содержащих кванторы, поэтому обратимся к теориям первого порядка (или, иначе, элементарным теориям). Слова «первого порядка» указывают на отличие рассматриваемых теорий от таких теорий, в которых либо допускаются предикаты, имеющие в качестве возможных значений своих аргументов другие предикаты и функции, либо допускаются кванторы по предикатам или кванторы по функциям. Теорий первого порядка хватает для выражения известных математических теорий и, во всяком случае, большинство теорий высших порядков может быть подходящим образом «переведено» на язык первого порядка. Фиксируем логико-математический язык первого порядка L. Аксиомами исчисления предикатов (ИП) в языке L называются формулы этого языка, имеющие один из следующих видов: Здесь A, B, C – произвольные формулы языка L, так что каждая строка приведенного списка задает схему аксиом ИП. Фиксируя A, B, C, из каждой из четырнадцати схем аксиом можно получить бесконечное семейство конкретных аксиом. Далее означает правильную подстановку терма вместо переменной с необходимыми переименованиями связанных переменных. Вместо будем иногда несколько неточно писать A(t). В схемах (ип12) и (ип14) формула C не содержит свободной переменной x. С помощью уже рассмотренных нами методов нетрудно убедиться, что все аксиомы ИП суть логические законы, общезначимые формулы (т.е. тавтологии). Фигуры следующих двух видов называются правилами вывода ИП: (MP) , (Gen) . Первое правило вывода носит традиционное латинское название – модус поненс (modus ponens). Второе правило называется правилом обобщения (Gen – от английского слова «generalization»). Оба правила сохраняют логические законы: если выше черты стоят тавтологии, то формула ниже черты также тавтология). Дерево формул (в ИП) есть по определению некоторая двумерная фигура, составленная из формул языка по следующим трем индуктивным правилам: 1) каждая формула A сама по себе является деревом формул, нижней формулой этого дерева формул считается по определению формула A; 2) если и – деревья формул с нижними формулами вида A и соответственно, то фигура есть дерево формул. Говорят, что формула B получена в этом дереве из A и по правилу (MP); нижней формулой результирующего дерева является формула B; 3) если – дерево формул с нижней формулой A и x – переменная, то фигура есть также дерево формул. Говорят, что нижняя формула этого дерева получена из A по правилу (Gen). Последовательность вхождений формул в дерево формул, начинающаяся с нижней формулы дерева и продолжающаяся без пропусков до одной из самых верхних формул дерева, называется ветвью дерева формул. Количество формул в самой длинной ветви дерева называется высотой дерева формул. Верхние формулы дерева формул, не имеющие вида аксиом ИП, называются гипотезами, или открытыми посылками, дерева. Формула B, входящая в вывод, расположена выше формулы A, если существует ветвь вывода, содержащая A и B, причем B в этой ветви встречается позже, чем A. Если формула получена в дереве формул из формулы A по правилу (Gen), а формула B расположена в дереве формул выше рассматриваемого вхождения и содержит свободно x, то говорят, что переменная x варьируется в формуле B. Тогда структурное требование можно выразить следующим образом: в выводе параметры гипотез не варьируются, остаются свободными. Структурное требование выполняется тривиально, если дерево формул не содержит правил (Gen), или если все гипотезы дерева формул суть замкнутые формулы, или если дерево формул вовсе не содержит гипотез. Пусть Г – конечный список формул и A – формула. Говорят, что формула A выводима в ИП из списка формул Г, и пишут ГA, если существует вывод D с нижней формулой A такой, что всякая гипотеза D является членом списка Г. При этом, конечно, некоторые формулы из Г могут и не быть гипотезами D. Говорят, что вывод D формулы A не зависит от таких членов Г. Список Г может быть пуст. Тогда ГA означает, что имеется вывод A без гипотез; тогда пишут A и говорят: формула A выводима в ИП. Саму фигуру ГA называют иногда выводимостью (или, в другой терминологии, секвенцией). Таким образом, чтобы обосновать секвенцию ГA, следует построить вывод в ИП с нижней формулой A, все гипотезы которого находятся среди членов списка Г. Непосредственно использовать выводы в ИП для установления логических законов на практике крайне неудобно. Выводы даже простых формул получаются очень громоздкими, а главное, весьма непохожими на обычные способы рассуждения, применяемые в математике. Поэтому понятие вывода в ИП используется, главным образом, в теоретических исследованиях, где существенно, чтобы выводы имели простую структуру. Практически же выводимость формул и секвенций устанавливается с помощью серии специально подобранных допустимых вспомогательных правил вывода, относящихся непосредственно к секвенциям. С их помощью можно установить, что секвенция выводима, не строя для нее вывод в ИП. Указанные правила уже близко соответствуют обычной практике математического рассуждения, что сильно облегчает доказательство выводимости. Набор этих правил называется техникой естественного вывода. Ключевым фактом здесь является следующая теорема. Е Теорема о дедукции показывает, что для установления импликации Следующие правила называются структурными правилами техники естественного вывода:
Правила 2 – 5 следует понимать как допустимые правила вывода. Это означает, что если дан вывод для секвенций, расположенных выше черты, то можно построить вывод и для секвенций, расположенных ниже черты. В технике естественного вывода данные правила широко употребляются без явного упоминания. Следующую группу образуют логические правила техники естественного вывода. Эти правила разбиваются на группы: для каждой логической связки и квантора – своя группа правил. Кроме того, внутри группы правила делятся на два вида: правила введения, указывающие, как доказывать формулу с данным логическим символом, и правила удаления, указывающие, как использовать формулу с данным логическим символом для доказательства других формул:
На практике логические правила применяются, так сказать, в обратном порядке: нужно установить секвенцию ниже черты, и мы замечаем, что для этого достаточно установить секвенцию выше черты. В этом свете можно заметить, что все правила соответствуют довольно обычным приемам математического рассуждения. Например: -удаление соответствует разбору случаев. Если в некоторой ситуации из AB нужно вывести C, то мы рассуждаем так: если верно AB, то либо A, либо B, и поэтому достаточно разобрать случаи, вывести C из A и вывести C из B по отдельности; -удаление соответствует правилу единичного выбора (в другой терминологии, правилу С). Допустим, что x A(x), и выведем C. Раз существует x, такое, что A(x), то можно рассмотреть (выбрать) одно из таких x. Обозначим его через y. Для этого y верно A(y). Таким образом, достаточно вывести формулу C из A(y). Правило -введения соответствует рассуждению от противного, приведению к абсурду (традиционное латинское название – reductio ad absurdum): чтобы установить A, достаточно, допустив A, получить противоречие, т.е. вывести B и B одновременно для подходящего B. Руководствуясь этими идеями, можно доказывать выводимость логических законов, исходя из их содержательного смысла. Разумеется, в технике естественного вывода можно использовать и другие секвенции, выводимости которых уже установлены, или иные допустимые правила. Еще одно полезное правило – правило подстановки: ГA Г()A() . ПримерыПример 3.3 Построить вывод в ИП для формулы х А у (А(ху)), где А – формула, х и у – различные переменные, причем у не входит свободно в А. В более традиционной (но менее точной) записи это высказывание имеет вид: х А(х)у А(у). РешениеСтроим вывод: х А(х) А(у), (а) это пример схемы аксиом (ип2); у (х А(х) А(у)), (б) по правилу (Gen) из (а), структурное требование выполняется, так как (а) – не гипотеза (а аксиома ИП); у (х А(х)А(у))(х А(х)у А(у)), (в) это пример схемы аксиом (ип12) (существенно, что х А(х) не содержит свободно у); х А(х)у А(у) (г) вытекает из (б) и (в) по правилу (MP). Соответствующее дерево вывода имеет вид: Привести краткое обоснование пяти допустимых структурных правил вывода в ИП). РешениеПравило 1 – из гипотезы A и ввиду АA по (MP) AА. Правила 2 – 4 – тривиально допустимы. Вывод, обосновывающий секвенцию выше черты, обосновывает и секвенцию ниже черты; Правило 5 – из B, AC по теореме о дедукции BАC. Отсюда и из ГА по правилу добавления Г, BАC; Г, BА. Применяя (MP), получим Г, BC. Доказать логические правила техники естественного вывода в ИП (см. с. 59-60). Решение Приведем доказательства некоторых из правил (остальные доказываются аналогично). -введение. Это есть в точности теорема о дедукции. -удаление. Из данных выводов ГA, ГAB вывод для ГB получим с помощью (MP). -введение. Имеем: ГA. Кроме того,AAB (это аксиома). По (MP) ГAB. -удаление. Из данных Г,AC; Г,BC по теореме о дедукции ГAC и ГBC. Кроме того, (AC)((BC)(ABC)) (это аксиома). Дважды применяя (MP), получим: ГABC. По закону тождества (и правилу добавления) Г,ABAB. По (MP) Г,ABC. -удаление. Из Г,A(y)C по теореме о дедукции следует, что ГA(y)C. По правилу обобщения Гy(A(y)C) (здесь существенно, что y не входит свободно в Г). Имеем аксиому y(A(y)C)(y(A(y) C)). По (MP) Гy A(y) C. Аналогично x A(x) yA(y). Отсюда Г,xA(x)yA(y). Следовательно, по (MP) Г,xA(x) C. -введение. Из Г, AВ и Г, BA по теореме о дедукции ГAB, ГBA, Г(AB)(BA), что и означает по определению эквивалентности ГAB. Пример 3.6 Доказать в ИП, что AB(AB). Решение Согласно -введению достаточно установить AB (AB) и (AB) AB. Начнем с первой секвенции. Слева у нее стоит дизъюнкция, поэтому, разбирая случаи согласно - удалению, достаточно установить два факта: Установим только первый, второй устанавливается симметрично. Для вывода отрицания (AB) достаточно допустить AB и вывести противоречие, т.е. использовать -введение. Противоречие будет состоять в выводе A и A. Итак, для вывода A(AB) с помощью -введения достаточно установить: A,ABA и A,ABA. Первая секвенция выводима по закону тождества. Для вывода второй согласно -удалению достаточно показать: A,A,BA, что также следует из закона тождества. Теперь установим: (AB)AB. Здесь наше рассуждение будет косвенным. Согласно -удалению достаточно установить: (AB) (AB). А для этого согласно -введению следует, допустив (AB), вывести противоречие. Мы докажем: (AB),(AB) (AB) и (AB)AB. Первая секвенция, очевидно, выводима по закону тождества. Вторую секвенцию получим по -введению. Достаточно вывести: (AB)A и (AB)B. Мы выведем первую секвенцию, вторая выводится симметрично. Используя - введение, достаточно вывести: (AB),A(AB) и (AB),AAB. Но первая из этих секвенций очевидна, а вторая получается с помощью Вывести AA. РешениеСогласно -удалению достаточно вывести (AA). С этой целью по -введению допустим, что (AA), и получим противоречие: (AA)A, (AA)A. Для вывода первой секвенции (-введение) допустим A и получим противоречие: (AA),A(AA), (AA),AAA. Первая из этих секвенций очевидна, а вторая получается -введением. Аналогично, для получения секвенции: (AA)A достаточно вывести секвенции (AA),A(AA), (AA),AAA, которые доказываются аналогично. Вывести x A(x) x A(x). РешениеC этой целью допустим x A(x) и выведем x A(x), т.е. выведем: x A(x)x A(x). Для этого согласно -удалению выберем новую переменную у и установим A(y)x A(x). Это можно сделать с помощью - введения: A(y), x A(x)A(y) и A(y),x A(x)A(y). Первая секвенция есть закон тождества, а вторая получается -удалением. Пример 3.9 Доказать A(AB). Решение Расположим доказательство в технике естественного вывода прямым образом, «сверху вниз»:
Пример 3.10 Доказать правило подстановки в технике естественного вывода в ИП. РешениеПусть для простоты Г есть список ,. Из ,A по -удалению A, а по -введению A. По правилу обобщения (A). Далее, ((A)(A))' есть аксиома; штрихом здесь обозначена подстановка (). По (MP) (A)', или, что то же самое, . Далее, по -введению . По (MP) , что и требовалось доказать. Задачи3.2. Являются ли выводами в ИП следующие последовательности: а) ; б) , , где - одноместный предикатный символ; в) , , ? 3.3. Каким требованиям должна удовлетворять формула , чтобы следующая последовательность была выводом в ИП: а) , ; б) , ? а) ; б) ; в) . 3.5. Являются ли следующие последовательности формул выводами из Г=, где не содержит свободных вхождений : а) , ; б) , , а) ; б) . << предыдущая страница следующая страница >> |
|