Лекция 4. Выводом в теории Т называется любая последовательность формул А1, ,Аn такая, что для всякого i формула Аi есть либо аксиома теории Т

Выводом в теории Т называется любая последовательность формул А1,…,Аn такая, что для всякого i формула Аi есть либо аксиома теории Т, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода.

Лекция 3

Классическое исчисление высказываний (продолжение)

3.1 Система аксиом для исчисления высказываний

Истинностные таблицы позволяют ответить на очень многие важные вопросы, возникающие в исчислении высказываний. Однако (как, например, в геометрии Евклида) часто недостаточно просто аксиоматизировать тот или иной раздел математики, а необходимо применить метод полной формализации, который поможет ответить на ряд важных вопросов, ответить на которые, не применяя метода полной формализации, не удаётся. Пример применения мы увидим несколько ниже в виде исчисления предикатов, т.к. исчисление высказываний ввиду своей простоты таким примером служить не может. Однако общие черты метода формальных теорий (метаматематики или теории доказательств), введённого Д. Гильбертом, опишем сразу и применим этот метод и для исчисления высказываний.

Формальная аксиоматическая теория Т задана, если выполнены следующие условия (читатель найдёт в других учебниках несколько иные условия, но все они оказываются эквивалентными):

а) задано счётное число исходных символов – алфавит теории Т; конечные последовательности (слова) этих символов называются выражениями теории Т;

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

с) выделено некоторое множество формул, называемых аксиомами теории Т; здесь также часто (но далеко не всегда) имеется эффективная процедура, позволяющая выяснить, является ли данная формула аксиомой (эффективно аксиоматизируемая теория);

d) имеется конечное множество отношений R₁,…,R_n между множествами формулами, называемых правилами вывода; для каждого R_i и для каждого натурального j можно эффективно определить, состоят ли данное множество из j формул и данная формула А в отношении R_i, и если да, то формула А называется непосредственным следствием из данных j формул по правилу R_i.

Формула А есть теорема теории Т, если существует вывод в Т, последней формулой которого является А; такой вывод называется выводом формулы А в теории Т.

Понятие теоремы не обязательно является эффективным (как правило, не является эффективным), даже если сама теория эффективно аксиоматизируема. Если множество теорем является эффективно заданным, то теория Т называется разрешимой; в противном случае – неразрешимой. Разрешимая теория такова, что подразумевает существование эффективной процедуры, позволяющей определить по любой формуле, выводима эта формула в Т или нет.

Формула А называется следствием в Т множества формул Г, если в теории Т+Г существует вывод формулы А (теория Т+Г получается из теории Т добавлением всех формул из Г в виде аксиом). Иногда говорят о выводе в Т формулы А из множества формул Г. Члены Г называют гипотезами или посылками. Формальные записи таковы: „_Т А – в теории Т выводима формула А (формула А есть теорема теории Т). Г „_Т А – в теории Т формула А выводима из множества формул Г (далее индекс Т будем часто опускать).

Простейшие свойства выводимости:

а) если ГÍD и Г „ А, то D „ А; в) Г „ А тогда и только тогда, когда в Г существует конечное подмножество D такое, что D „ А; с) если D „ А и Г „ В для любого В из D, то Г „ А. Все приведённые свойства имеют простое толкование, связанное с понятием вывода Попробуйте самостоятельно «перевести» эти свойства на обычный язык. Например, а) если есть вывод из Г и Г есть подмножество D, то, конечно, есть вывод и из D.

Теперь мы готовы ввести формальную аксиоматическую теорию L для исчисления высказываний.

1) символами L (далее символ L иногда опускаем) являются Ø, ®, (,) и буквы А_i, где индексы есть натуральные числа. А_i – пропозициональные буквы (пб), остальные – примитивные связки (пс) и скобки.

2) а) все пб есть формулы (фл); в) если А и В – фл, то (ØА) и (А®В) также фл; с) других фл, кроме полученных по пунктам а) и в), нет.

3) следующие фл суть аксиомы теории L:

А1. (А®(В®А)); А2. (А®(В®С))®((А®В)®(А®С)); А3. ((ØВ ® ØА)®((ØВ ® А)®В)), где А,В и С – любые фл.

4) правило вывода (modus ponens (MP)): В есть непосредственное следствие А и А®В.

Замечание. Как всегда, при записи фл будем придерживаться соглашений относительно исключения скобок.

Отметим, что собственно аксиом – бесконечное множество, которое задано с помощью трёх схем аксиом. Множество аксиом задано эффективно, т.к. относительно любой формулы можно проверить, является она аксиомой или нет.

Наша цель такова: построить систему L так, чтобы множество её теорем совпадало с классом всех тавтологий. Для этого сначала введём остальные связки таким образом: (АÙВ) есть Ø(А®ØВ); (АÚВ) есть ØА®В; (АºВ) есть (А®В)Ù(В®А).

Приведём пример вывода и его записи в теории L.

Утверждение 3.1.1. Для любой фл А „_L А®А (далее нижний символ L опускаем).

Построим требуемый вывод:

(1) (А®((А®А)®А))®((А®(А®А))®(А®А))

аксиома А2 (какие фл подставлены вместо А,В и С?);

(2) А®((А®А)®А) аксиома А1 (тот же вопрос);

(3) (А®(А®А))®(А®А) из 1 и 2 по MP;

(4) А®(А®А) аксиома А1;

(9) А®А из 3 и 4 по MP. Вывод завершен.

Задача. Постройте выводы в L для следующих фл:

а) (ØА®А)®А;

в) А®С из гипотез А®В и В®С;

с) В®(А®С) из гипотезы А®(В®С);

Решения. а) По схеме А3 (ØА®ØА)®((ØА®А)®А) подставляем А вместо В. (ØА®ØА) выведена выше. По МР имеем требуемое.

в) По схеме А1 (В®С)®(А®(В®С)) (вместо А ставим В®С, вместо В - А. Применяем МР и получаем А®(В®С). Из схемы А2 и полученной формулы по МР получаем (А®В)®(А®С). Из посылки (А®В) и полученной последней формулы получаем А®С.

с) По схеме А1 А®(В®С)®[В®(А®(В®С))] (что вместо чего в А1

подставляется?) По МР и посылке имеем [В®(А®(В®С))]. По А2

В®(А®(В®С))®[В®(А®В)®(В®(А®С))] (тот же вопрос, что и ранее (указание: просто на все формулы «навешиваем» впереди В)). По МР и выведенной раньше формуле В®(А®(В®С)) получим [В®(А®В)®(В®(В®(А®С))]. Т.к. посылка (В®(А®В) – пример А1, то применяем снова МР и получаем требуемое.

3.2. Теорема о дедукции для исчисления L.

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

3.2.1. Теорема о дедукции. Если Г – множество фл, А и В – фл и Г,А „ В, то Г „ А®В (Эрбран, 1930 г.).

Доказательство. Пусть В₁,…,В_n – вывод из ГÈ{А} и В=В_n. Индукцией по длине вывода докажем, что Г „ А®В.

Основание индукции. Тогда В=В₁ есть либо элемент Г, либо В=А, либо В – аксиома. В первом и третьем случаях, используя аксиому В®(А®В), получаем Г „ А®В по МР. Во втором случае в силу Утверждения 3.1.1 имеем также Г „ А®В и основание индукции завершено (более детально проверьте этот пункт).

Индукционный шаг. Пусть для всякого i< n наше утверждение доказано, т.е. Г „ А®В_i. Для В_n есть четыре возможности: В_n – аксиома, В_nÎГ, В_n=А или В_n получено по правилу МР из В_j и B_m, где j и m < n, причём В_m имеет вид В_j®В_n. В первых трёх случаях Г „ А®В доказывается так же, как в случае с основанием индукции (обязательно дайте точное доказательство!). В последнем случае применяем индукционное предположение, согласно которому Г „ А®В_j, Г „ А®В_m, т.е. Г „ А®(В_j®B_n). По схеме аксиом А2) имеем „(А®(В_j®B_n))®((A®B_j)®(A®B_n)). Теперь по правилу МР Г „ (А®В_j)®(A®B_n) и снова по МР Г „(А®В_n). Доказательство индукционного шага и всей теоремы о дедукции завершено.

Отметим, что доказательство носит конструктивный характер: оно позволяет по данному выводу В из Г и А построить вывод А®В из Г. Также отметим, что при доказательстве были использованы только схемы А1 и А2. Теорема о дедукции позволяет сократить долгий и не простой иногда вывод нужной формулы.

Следствие 3.2.2. А®В, В®С „ А®С; А®(В®С), В „ А®С. Задача. Докажите Следствие 3.2.2 самостоятельно, используя теорему о дедукции.

Утверждение 3.2.3. Следующие фл являются теоремами L для любых фл А и В:

(а) ØØВ ® В; (b) B ® ØØB; c) ØA®(A®B);

(d) (ØB®ØA)®(A®B); (e) (A®B)®(ØB®ØA);

(f) A®(ØB®Ø(A®B)); (g) (A®B)®((ØA®B)®B).

(h) ((A®B)®A)®A; (k) A®(B®(AÙB)).

(вспомните, что пс Ù есть сокращение!)

Задача. Докажите Утверждение 3.2.3., построив в L выводы.

В качестве примера докажем (а):

1) (ØВ®ØØВ)®((ØВ®ØВ)®В) схема аксиом А3

(укажите, что в этой схеме аксиом есть фл А и фл В);

2) ØВ®ØВ по Утверждению 3.1.1;

3) (ØВ®ØØВ)®В из 1) и 2), в пункте 3.1.1. в Задаче вывод с);

4) ØØВ®(ØВ®ØØВ) схема аксиом 1;

5) ØØВ ® В из 3) и 4), в пункте 3.1.1 в Задаче вывод в).

Теперь мы докажем, что фл теории L является теоремой тогда и только тогда, когда эта фл есть тавтология.

Утверждение 3.2.4. Всякая теорема теории L является тавтологией.

Мы оставляем доказательство Утверждения 3.2.4 читателю (нужно убедиться, что любая аксиома есть тавтология и что правило МР по тавтологиям даёт тавтологию, см. Утверждение 2.2.1).

Указание. Для доказательства 3.2.4. воспользуйтесь таблицами истинностности.

Утверждение 3.2.5. Пусть А – фл и В₁,…,В_n – пб, входящие в А. Пусть задано некоторое распределение истинностных значений для этих пб. Пусть В_i` есть фл В<sub>i</sub>, если В<sub>i</sub> принимает значение 1 и фл ØВ<sub>i</sub>, если В<sub>i</sub> принимает значение 0. Пусть А` есть фл А, если при заданном распределении истинностных значений пб фл А принимает значение 1 и ØА, если фл А принимает значение 0. Тогда В₁`,…,В<sub>n</sub>` „ А`.

Дадим краткое пояснение в виде примера. Пусть фл А = ØВ₁®В₂. Пусть В₁ принимает значение 1, а В₂ – значение 0. Тогда фл А принимает значение 1 и утверждается, что В₁, ØВ₂ „ ØВ₁®В₂.

Доказазательство 3.2.5. Индукция по числу n вхождений пс в А. Основание индукции: n=0 и А есть просто пб В₁. Утверждение сводится к доказательству ØВ₁ „ ØВ₁ или В₁ „ В₁ (см. Утверждение 3.1.1 и примени теорему о дедукции).

Индукционный шаг: пусть Утверждение 3.1.5 верно при любом к< n. 1 случай: А = ØВ и число вхождений пс в В меньше n. Если при заданном распределении истинностных значений пб В принимает значение 1, тогда А принимает значение 0 и В`=В, а А`= ØА. По предположению индукции имеем В₁`,…,В<sub>к</sub>` „ В. Но тогда по Утверждению 3.2.3 (b) и МР В₁`,…,В<sub>к</sub>` „ ØØВ, которое и есть А. Пусть теперь В принимает значение 0, тогда А принимает значение 1 и В`= ØВ и А`=А. По предположению индукции В₁`,…,В<sub>к</sub>` „ ØВ, а это и есть А. 2 случай: А=В®С. Число вхождений пс в В и С меньше n и по индукционному предположению В₁`,…,В<sub>к</sub>` „ В` и В<sub>1</sub>`,…,В_к` „ С`. Если В принимает значение 0, то А принимает значение 1 и В`= ØВ и А`=А. Но тогда В₁`,…,В<sub>к</sub>` „ ØВ и по Утверждению 3.2.3 (c) В₁`,…,В<sub>к</sub>` „ В®С, т.е. А. Если С принимает значение 1, то А принимает значение 1 и С`= С, А`=А. Т.к. В₁`,…,В<sub>к</sub>` „ С(=С`), то по схеме аксиом А1) В<sub>1</sub>`,…,В_к` „ В®С(=А`). Пусть, наконец, В принимает значение 1 и С принимает значение 0. Тогда А принимает значение 0 и А`= ØА, В`=В и С`= ØС. По предположению индукции имеем В<sub>1</sub>`,…,В_к` „ В и В<sub>1</sub>`,…,В_к` „ ØС. Тогда по Утверждению 3.2.3 (f) получаем, что В<sub>1</sub>`,…,В_к` „ Ø(В®С), что и есть А. Индукционный шаг, а с ним и Утверждение 3.2.5 доказаны.

Вопросы и упражнения к Лекции 3.

1. Дайте определения: алфавита, выражения, теоремы, вывода в

формальном исчислении.

2. Сформулируйте теорему о дедукции и поясните, почему она

является вспомогательным правилом вывода.

3. Сформулируйте аксиомы и правила вывода для исчисления L.

4. Сколько аксиом в исчислении L? А сколько схем аксиом?

5. Сколько правил вывода в исчислении L?

6. Что означает, что формула А является следствием множества

формул Г в исчислении L? Может ли Г быть бесконечным

множеством?

Классическое исчисление высказываний (окончание)

4.1. Полнота и разрешимость исчисления L.

Утверждение 4.1.1. Теорема о полноте. Если фл А теории L является тавтологией, то она есть теорема теории L.

Доказательство (Кальмар). Пусть А есть тавтология и В₁,…,В_к - пб, входящие в А. В силу Утверждеия 3.2.5 при всяком распределении истинностных значений пб имеем В₁`,…,В<sub>к</sub>` „ А (т.к. А – тавтология). Отсюда получаем, что если В_к принимает значение 1, то В₁`,…,В`_к-1,В_к „ А, а если В_к принимает значение 0, то В₁`,…,В`_к-1,ØВ_к „ А. А тогда по теореме о дедукции и по Утверждению 3.2.3 (g) В₁`,…,В`_к-1 „ А. Продолжая этот процесс исключения пб, мы получим „ А. Теорема о полноте доказана.

Следствие 4.1.2. Если выражение В содержит все пропозициональные связки и является сокращением для некоторой фл А теории L, то В является тавтологией тогда и только тогда, когда А есть теорема теории L.

Доказательство. Сокращения для связок являются эквивалентными им пропозициональными формами и в силу 2.2.3. их подстановка не изменит логической эквивалентности формул А и В, т.е. формулы А и В являются тавтологиями одновременно. По теореме о полноте В тавтология тогда и только тогда, когда А является теоремой.

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

Утверждение 4.1.3. Система L непротиворечива.

Для доказательства достаточно заметить, что отрицание тавтологии не есть тавтология.

Из непротиворечивости L следует, что есть фл, не являющаяся теоремой L. Но непротиворечивость теории L можно вывести непосредственно из факта существования фл, не выводимой в L. Действительно, т.к. по Утверждению 3.2.3 (с) „ ØА®(А®В), то из противоречивости L и правила МР в L была бы выводима любая фл В (этот факт был бы верен в любой теории с правилом МР, в которой выполнено Утверждение 3.2.3 (с)). Теорию, в которой не все фл выводимы, иногда называют абсолютно непротиворечивой и такое определение применимо к теориям, не содержащим пс отрицания.

Утверждение 4.1.4. Теория L разрешима, т.е. существует эффективная процедура, применимая ко всем формулам L, которая по всякой формуле решает, выводима эта формула в L или нет.

4.2. Другие аксиоматизации для исчисления высказываний.

Приведём здесь только один, самый распространённый, пример аксиоматизации исчисления высказываний. Обозначим эту систему через L₄.

Пс служат ®, Ù, Ú, Ø и упоминавшиеся в формализации для L скобки и пб. Единственное правило вывода – МР. Класс аксиом задаётся следующими схемами:

1.А®(В®А); 2. (А®(В®С))®((А®В)®(А®С)); 3. АÙВ ® А;

4. АÙВ ® В; 5. А®(В®(АÙВ)); 6. А®(АÚВ); 7. В®(АÚВ);

8. (А®С)®((В®С)®(АÚВ®С)); 9.(А®ØВ)®((А®В)®ØА);

10.ØØА®А.

Для связки º применяется обычное сокращение.

Задача. Докажите, что системы L и L₄ имеют одно и то же множество теорем (с точностью до принятых сокращений). Используйте теорему о дедукции. Не забудьте, что при погружении L₄ в L нужно связки-сокращения заменить на их оригиналы в языке L.

4.3. Независимость. Многозначные логики.

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

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

Пусть числа 0,1, …, n являются истинностными значениями и выберем какое-либо число m такое, чтобы 1 £ m £ n. Числа 0, …, m назовём выделенными истинностными значениями. Выберем некоторое число истинностных таблиц, которые представляют собой функции, отображающие множество {0,1,…,n}^к в {0,1,…,n}. Для каждой такой таблицы введем знак, который будем называть соответствующей этой таблице связкой. С помощью этих связок и пб можно строить пф (многозначные!). Всякая такая пф определяет некоторую истинностную функцию из множества {0,1,…,n}^к в множество {0,1,…,n}. Пф называется выделенной, если она принимает только выделенные значения. В этой ситуации говорят, что задана многозначная логика М. Аксиоматическая теория, содержащая пб и связки логики М, называется подходящей для логики М в том и только в том случае, если множество теорем этой теории совпадает с множеством выделенных пф логики М (все эти понятия можно обобщить и на случай логики с бесконечным числом истинностных значений). В этом случае аксиоматическая теория называется полной относительно логики М. Выше была изучена двузначная логика, соответствующая случаю n=1 и m=0, соответствующие связки были определены в пункте 1.2. Выделенные пф назывались тавтологиями. Утверждения 3.2.4 и 4.4.1 говорили, что теория L является подходящей для этой логики аксиоматической теорией. Используя технику многозначных логик, докажем, что все три схемы аксиом теории L являются независимыми.

Утверждение 4.3.1. Схема аксиом А1 является независимой. Доказательство. Рассмотрим таблицы:

А ØА А В А®В

0 1 0 0 0

1 1 1 0 2

2 0 2 0 0

0 1 2

1 1 2

2 1 0

0 2 2

1 2 0

2 2 0

Ясно, что при всяком распределении значений 0,1,2 для букв, входящих в какую-либо фл А, эти таблицы позволяют найти соответствующее значение А. Если А принимает всегда значение 0, то она будет называться выделенной (трёхзначная логика с одним выделенным значением). Можно убедиться, что правило МР сохраняет свойство выделенности. Нетрудно также проверить, что всякая аксиома, получающаяся по схемам А2 или А3, также является выделенной. Также, любая фл, выводимая из А2 и А3 по правилу МР, будет выделенной. Но фл А®(В®А) не является выделенной (эта формула, а точнее пф, принимает значение 2, когда А принимает значение 1 и В принимает значение 2). Это и доказывает независимость схемы А1.

Задача. Докажите независимость схем аксиом А2 и А3, придумав подходящие таблицы для связок ® и Ø в отмеченной трёхзначной логике (при этом задача может быть решена совершенно различными способами). Отметим также, что в случае доказательства независимости нам не нужно доказывать полноту аксиоматики относительно многозначной логики, а только так называемую корректность, т.е. аналог Утверждения 3.2.4.

Продемонстрируем другой способ доказательства независимости схемы аксиом А3. Общий подход в деле доказательства независимости таков: для аксиоматической теории Т нужно построить модель (ниже мы определим понятие модели в некотором частном случае; в общем случае этим занимается специальная ветвь математической логики – теория моделей), в которой бы все аксиомы были «истинны», а аксиома, чья независимость должна быть доказана – нет. Если А – произвольная фл теории L, то пусть фл Р(А) получается из фл А стиранием в ней всех знаков отрицания. Нетрудно теперь заметить, что Р(А1) и Р(А2) – тавтологии, т.к. они просто не меняютсвой вид (в них связка Ø не входит). Правило МР также сохраняет свойство А иметь в качестве Р(А) тавтологию. Теперь достаточно взять следующий частный пример схемы А3: В = (ØА®ØА)®((ØА®А)®А), вычислить Р(В) (вычислите!) и убедиться, что Р(В) не является тавтологией. Если подставить в Р(В) 0 вместо А, то получим 0. Таким образом, схема аксиом А3 является независимой от схем аксиом А1 и А2.

Дата добавления: 2014-01-06