2 - Исчисление высказываний. Основные положения теории N. Правила естественного вывода. Глобальные свойства теории N (Конспект лекций)

ÔÍ-12ÔÍ-12ÌÃÒÓМосковский государственный технический университетимени Н.Э. БауманаÌÃÒÓФакультет «Фундаментальные науки»Кафедра «Математическое моделирование»ÌÃÒÓÀ.Í. ÊàíàòíèêîâÈ ÒÅÎÐÈß ÀËÃÎÐÈÒÌÎÂÊîíñïåêò ëåêöèéÔÍ-12Москва2009ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12Äëÿ ñòóäåíòîâ êàôåäðû ÈÓ9ÌÃÒÓÌÃÒÓÌÀÒÅÌÀÒÈ×ÅÑÊÀß ËÎÃÈÊÀÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓ2.1. Основные положения теории NÔÍ-12Язык теории N .

Аксиомы (их одиннадцать): 1) X → (Y → X); 2) X → Y → (X → (Y → Z) →(X → Z)); 3) X ∧ Y → X; 4) X ∧ Y → Y ; 5) (X → Y ) → ((X → Z) → (X → Y ∧ Z)); 6) X → X ∨ Y ;7) Y → X ∨ Y ; 8) X → Z → (Y → Z → (X ∨ Y → Z)); 9) X → Y → (¬Y → ¬X); 10) ¬¬X → X;X, X → Y11) X → ¬¬X. Правило вывода(modus ponens). Вывод в теории N . Вывод изYгипотез.

Пример: X → X. Дерево вывода.7) Y → X ∨ Y ;2) X → Y → (X → (Y → Z) → (X → Z));8) X → Z → (Y → Z → (X ∨ Y → Z));3) X ∧ Y → X;9) X → Y → (¬Y → ¬X);4) X ∧ Y → Y ;10) ¬¬X → X;5) (X → Y ) → ((X → Z) → (X → Y ∧ Z));11) X → ¬¬X.6) X → X ∨ Y ;14ÔÍ-121) X → (Y → X);ÌÃÒÓЯзык теории N — это язык алгебры высказываний. В теории N одиннадцать схем аксиом. Схема аксиом отличается от аксиомы тем, что в ней используются не конкретныепеременные, а символы подстановки, вместо которых могут подставляться конкретные формулы теории.

При выборе вместо символов подстановки конкретных формул мы получаемконкретную аксиому. Отметим, что можно было бы избежать схем аксиом, но тогда придетсявводить дополнительные правила вывода, которые позволили бы размножить“ аксиому.”Итак, сформулируем одиннадцать схем аксиом теории N :ÌÃÒÓÔÍ-12ÌÃÒÓНапомним, что полностью формализованная математическая теория (исчисление) выглядиттак. Имеется некоторый язык, позволяющий составлять правильные слова-формулы, которые отражают возможные утверждения теории. Есть некоторый набор формул, изначальнообъявленных истинными (это аксиомы). Кроме того, задан некоторый набор правил преобразования формул, которые позволяют из истинных формул получать новые истинные формулы.Все истинные утверждения теории получаются путем формальных преобразований формул врамках узаконенных правил преобразований.

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

Кроме того, алгебра высказываний в основном сводитсяк теории булевых функций, т.е. к исследованию конечных объектов. Поэтому исчисление высказываний — одно из самых простых и в этом смысле удобно как иллюстрация современногоподхода к формализации в математике.Любая теория имеет множество вариантов формализации. В рамках логики высказываниймы остановимся на одном из этих вариантов, который назовем теорией N .ÔÍ-12ÔÍ-122. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓСледует заметить, что фактически вывод представляет собой особую структуру — дерево:каждая формула вывода есть либо аксиома или гипотеза (лист дерева, начальный элементструктуры), либо имеет предшественников, из которых она получена по правилу вывода.

Дляформулы X → X из последнего примера дерево вывода имеет следующий вид:X → (X → X → X)X → (X → X → X) → (X → X)X →(X →X)→(X →(X →X →X)→(X →X))X → (X → X)ÔÍ-12X →XÌÃÒÓПример 2.1. Построим вывод формулы X → X, где X — какая-либо формула теории N :1) из схемы 1 получаем аксиому X → (X → X);2) из схемы 2, заменяя Z на X и Y на X → X, получаем аксиому X → (X → X) → (X → (X →→ X → X) → (X → X)),3) из двух предыдущих формул по правилу вывода X → (X → X → X) → (X → X);4) из схемы 1 при X → X взамен Y получаем аксиому X → (X → X → X);5) из двух последних формул по правилу вывода X → X.ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓПредставленная запись означает, что из двух правильных“ формул вида X и X → Y вытекает”правильная“ формула Y .”После введения языка, аксиом и правил вывода формальная теория готова.

Дальше можно начинать игру в слова“ и получать теоремы (т.е. выводимые формулы) этой теории. На”этом, собственно, заканчивается формальная часть и начинается неформальная, т.е. метатеория. Основной вопрос: что дает формальная теория в качестве выводимых формул. Отметим,что добросовестный вывод даже простых теорем оказывается весьма трудоемким, и следуетприбегать к приему, хорошо известному математикам: использовать уже выведенные теоремынаравне с аксиомами.Выводом теории N будем называть последовательность формул X1 , X2 , . . . , Xn , в которойкаждая формула Xi есть либо аксиома, либо получена из каких-либо предшествующих формулXk , Xm (k, m < i) по правилу modus ponens. Формула X называется выводимой в теорииN , если она является конечной формулой некоторого вывода.

Этот факт будем обозначатьследующим образом: ` X.Для нас будет важен условный вывод, или выод из гипотез, при котором некоторые формулы мы предполагаем истинными и на основании этого строим вывод. Такой условный выводиграет промежуточную роль, позволяя рассматривать отдельные части окончательного вывода. Кроме того, условный вывод можно рассматривать как построение вывода из нелогическихаксиом, которые присутствуют во всех математических теориях (они характеризуют основныеположения теории). Далее большими греческими буквами будем обозначать списки формултеории N .Выводом из гипотез Γ в теории N будем называть последовательность формул, в которой каждая формула есть либо аксиома, либо формула из списка Γ, либо она получена изпредшествующих формул по правилу modus ponens. При этом конечная формула X любоговывода из гипотез Γ называется выводимой из гипотез Γ, что обозначается следующимобразом: Γ ` X.ÔÍ-12ÔÍ-12X, X → Y.YÌÃÒÓÌÃÒÓВ теории N всего одно правило вывода — правило заключения (modus ponens):ÌÃÒÓÔÍ-12ÌÃÒÓ15ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-122.

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓТеорема 2.1 (теорема о дедукции). Если Γ, X ` Y , то Γ ` X → Y .ÔÍ-12По определению в выводе каждая формула есть либо аксиома, либо гипотеза, либо выводится из предыдущих по правилу modus ponens, т.е. формулы в выводе, строго говоря, могут повторяться. Однако ясно, чтоповторения можно убрать, не нарушая связей в выводе.ÌÃÒÓ*ÔÍ-12J Доказательство строится на анализе последовательности вывода. Фактически надо показать,что для любого вывода Z1 , Z2 , . . . , Zn = Y из гипотез Γ, X существует вывод из гипотез Γформулы X → Y . Доказательство проведем индукцией по длине вывода.При n = 1 конечная формула вывода Zn = Y есть либо аксиома, либо формула из списка Γ,либо формула X (правило modus ponens в данном случае не применялось, так как длина выводаменьше двух).

В первом и втором случаях строим последовательность формул Y , Y → (X → Y )(аксиома схемы 1), X → Y (modus ponens), которая является выводом формулы X и спискагипотез Γ. В третьем случае X = Y и формула X → Y совпадает с выводимой формулой X → X(см. пример 2.1). Таким образом, при n = 1 утверждение доказано.Предположим, что утверждение доказано для всех формул Y , имеющих вывод из гипотезΓ, X длины менее n. Рассмотрим произвольный вывод Z1 , Z2 , .

. . , Zn = Y . Формула Y естьлибо аксиома, либо формула из списка Γ, либо X, либо получена по правилу modus ponens. Впервых трех случаях рассуждения те же, что и при n = 1 (в выводе можно оставить толькопоследнюю формулу и свести дело к n = 1). Рассмотрим случай, когда Y получена по правилуmodus ponens из формул Zk и Zj . В этом случае одна из формул, например Zj , есть импликацияZk → Y .

В соответствии с индукционным предположением из гипотез Γ выводимы формулыX → Zk и X → (Zk → Y ). Объединим два этих вывода, удалив из списка повторения формул,если они есть* . Дополняем полученное объединение следующими тремя формулами:X → Zk → (X → (Zk → Y ) → (X → Y )) (аксиома схемы 2);X → (Zk → Y ) → (X → Y ) (modus ponens);X → Y (modus ponens).В результате получаем вывод формулы X → Y из гипотез Γ.

В соответствии с методом математической индукции утверждение теоремы доказано для конечной формулы любого выводаиз гипотез Γ, X. IÌÃÒÓÔÍ-12ÌÃÒÓОдна из целей введения исчисления высказываний — анализ используемой практики построения доказательств. В качестве единственного правила вывода в теории взято правило modusponens, в то время как построение доказательств на практике использует и многие другие правила: правило исключенного третьего, доказательство от противного и т.п. Оказывается, чтовсе подобные правила можно получить из аксиом исчисления высказываний и правила modusponens.Веденный символ ` выводимости в исчислении высказываний позволяет строить формулынового типа Γ ` X, которые на содержательном уровне можно интерпретировать так: если”истинны формулы списка Γ, то истинна формула X. Это формулы метаязыка, позволяющиеупростить процесс установления того, выводима данная формула или нет.

Само правило modusponens можно трактовать как формулу X, X → Y ` Y . Формулу вида Γ ` X будем называтьсеквенцией. Секвенция — это логическая формула, которая может быть истинной или нет.Чтобы приблизиться к общепринятой практике доказательств, выведем в теории N ряддополнительных правил, называемых правилами естественного вывода. Следующая теорема дает основополагающее правило естественного вывода, в некотором смысле обращающееправило modus ponens. Фактически эта теорема представляет собой утверждение об эквивалентности символа импликации → и символа выводимости `.ÔÍ-12ÔÍ-12Теорема о дедукции: если Γ, X ` Y , то Γ ` X → Y .