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

Московский государственный технический университетимени Н.Э. БауманаÌÃÒÓФакультет «Фундаментальные науки»Кафедра «Математическое моделирование»À.Í. ÊàíàòíèêîâÄÈÑÊÐÅÒÍÀßÌÀÒÅÌÀÒÈÊÀÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÊîíñïåêò ëåêöèéÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÄëÿ ñòóäåíòîâ ñïåöèàëüíîñòè<Ïðèêëàäíàÿ ìàòåìàòèêà>ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12Москва2006ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ3.

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

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

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

Дело в том, что формализация —это определенный метод математического исследования, который используется при исследовании теорий на непротиворечивость, наличие зависимых понятий и т.п.Отметим, что при изложении формальной теории приходится выходить за ее рамки, чтобыпроводить содержательный анализ ее результатов. Поэтому вокруг формальной теории возникает другая теория: учение о формальной теории“, которую называют метатеорией.”Метатеория формирует свой язык, расширяющий язык формальной теории, который называется метаязыком. На это было обращено внимание при изложении логики высказываний.Логика высказываний не является формальной теорией, хотя и имеет собственный язык.Все суждения в логике высказываний оказываются за пределами ее языка и устанавливаютсяна базе истинностных функций, которые никак не отражаются в языке логики высказываний.Реально все необходимые выводы логики высказываний можно было бы сделать, не прибегая к ее полной формализации.

Но тогда теряется связь получения тех или иных утвержденийс реальный процессом умозаключений, который и представляет собой подлинное математическое доказательство. Кроме того, логика высказываний в основном сводится к теории булевыхфункций, т.е. к исследованию конечных объектов. Поэтому формальная теория логики высказываний — одна из самых простых и в этом смысле удобна как иллюстрация современногоподхода к формализации в математике.ÔÍ-12ÔÍ-12Об аксиоматическом методе. Современные представления. Исчисления.

Теоремы и вывод.Теория и метатеория. Цели формализации в математике. Логика высказываний и ее формализация — теория K.ÌÃÒÓÌÃÒÓ3.1. ВведениеÌÃÒÓÌÃÒÓÌÃÒÓ24Любая теория имеет множество вариантов формализации. В рамках логики высказываниймы остановимся на одном из этих вариантов, который назовем теорией K.3.2. Основные положения теории NЯзык теории 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. Дерево вывода.Язык теории N — это язык алгебры высказываний. В теории N одиннадцать схем аксиом. Схема аксиом отличается от аксиомы тем, что в ней используются не конкретные переменные, а символы подстановки, вместо которых могут подставляться конкретные формулытеории. При выборе вместо символов подстановки конкретных формул мы получаем конкретную аксиому. Отметим, что можно было бы избежать схем аксиом, но тогда придется вводитьдополнительные правила вывода, которые позволили бы размножить“ аксиому.”Итак, сформулируем одиннадцать схем аксиом теории N :1) X → (Y → 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);10) ¬¬X → X;5) (X → Y ) → ((X → Z) → (X → Y ∧ Z));11) X → ¬¬X.ÌÃÒÓ4) X ∧ Y → Y ;ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123.

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ6) X → X ∨ Y ;В теории N всего одно правило вывода — правило заключения (modus ponens):ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓПредставленная запись означает, что из двух правильных“ формул вида X и X → Y вытекает”правильная“ формула Y .”После введения языка, аксиом и правил вывода формальная теория готова. Дальше можноначинать игру в слова“ и получать теоремы (т.е.

выводимые формулы) этой теории. На”этом, собственно, заканчивается формальная часть и начинается неформальная, т.е. метатеория. Основной вопрос: что дает формальная теория в качестве выводимых формул. Отметим,что добросовестный вывод даже простых теорем оказывается весьма трудоемким, и следуетприбегать к приему, хорошо известному математикам: использовать уже выведенные теоремынаравне с аксиомами.Выводом теории N будем называть последовательность формул X1 , X2 , .

. . , Xn , в которойкаждая формула Xi есть либо аксиома, либо получена из каких-либо предшествующих формулXk , Xm (k, m < i) по правилу modus ponens. Формула X называется выводимой в теорииN , если она является конечной формулой некоторого вывода. Этот факт будем обозначатьследующим образом: ` X.Для нас будет важен условный вывод, или выод из гипотез, при котором некоторые формулы мы предполагаем истинными и на основании этого строим вывод. Такой условный выводиграет промежуточную роль, позволяя рассматривать отдельные части окончательного вывода.Кроме того, условный вывод можно рассматривать как построение вывода из нелогических аксиом, которые присутствуют во всех математических теориях (они характеризуют основныеположения теории). Далее большими греческими буквами будем обозначать списки формултеории N .ÔÍ-12ÔÍ-12X, X → Y.YÌÃÒÓСледует заметить, что фактически вывод представляет собой особую структуру — дерево:каждая формула вывода есть либо аксиома или гипотеза (лист дерева, начальный элементструктуры), либо имеет предшественников, из которых она получена по правилу вывода.

Дляформулы X → X из последнего примера дерево вывода имеет следующий вид:X →XX → (X → X)3.3. Правила естественного выводаÔÍ-12Теорема 3.1 (теорема о дедукции). Если Γ, X ` Y , то Γ ` X → Y .ÌÃÒÓОдна из целей введения исчисления высказываний — анализ используемой практики построения доказательств. В качестве единственного правила вывода в теории взято правило modusponens, в то время как построение доказательств на практике использует и многие другие правила: правило исключенного третьего, доказательство от противного и т.п. Оказывается, чтовсе подобные правила можно получить из аксиом исчисления высказываний и правила modusponens.Веденный символ ` выводимости в исчислении высказываний позволяет строить формулынового типа Γ ` X, которые на содержательном уровне можно интерпретировать так: если”истинны формулы списка Γ, то истинна формула X.

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

Структурные правила естественноговывода. Логические правила естественного вывода. Дополнительные правила естественноговывода: присоединение посылки; закон противоречия; двойное отрицание; доказательство отпротивного; удаление конъюнкции справа. Обобщенное правило введения дизъюнкции.ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓX →(X →X)→(X →(X →X →X)→(X →X))ÌÃÒÓÔÍ-12X → (X → X → X) → (X → X)ÌÃÒÓÌÃÒÓПример 3.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ÌÃÒÓÌÃÒÓ25Выводом из гипотез Γ в теории N будем называть последовательность формул, в которой каждая формула есть либо аксиома, либо формула из списка Γ, либо она получена изпредшествующих формул по правилу modus ponens.