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

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙΓ`X ∧YΓ`X ∧Yд. Правилаиудаления конъюнкции справа вытекают из правила удалеΓ`XΓ`Yния конъюнкции (но также могут быть получены из схем аксиом 6 и 7). Например, первое изэтих правил получается применением правила сечения и правила удаления конъюнкции:Γ`XВторое правило удаления конъюнкции справа можно получить аналогично. #Правила естественного вывода и их следствия позволяют доказать выводимость широкогокруга секвенций. Однако отметим, что наиболее тяжело устанавливаются выводимости видаΓ ` X ∨ Y . Правило введения дизъюнкции сводит задачу к выводу более сильного утвержденияΓ ` X или Γ ` Y .Пример 3.3.

На практике для доказательства утверждения вида X ∨ Y можно рассуждатьтак: пусть X не верно, т.е. истинно ¬X. Докажем, что тогда истинно Y .“ Этому варианту”Γ, ¬X ` YΓ, ¬Y ` Xрассуждений соответствуют правилаи, которые можно получить и в исγ `X ∨YÔÍ-12Γ`X ∨YÔÍ-12Γ ` ¬¬(X ∨ Y )Γ, ¬(X ∨ Y ) ` XΓ, ¬(X ∨ Y ) ` ¬XΓ, ¬(X ∨ Y ) ` ¬¬XΓ, X ` X ∨ YΓ, ¬X ` X ∨ YΓ, X ` XÌÃÒÓΓ, ¬X ` YЭто правило назовем обобщенным правилом введения дизъюнкции.3.4. Глобальные свойства теории NОстановимся на описании множества выводимых формул в теории N . Нетрудно убедитьсяв том, что все аксиомы этой теории являются тавтологиями . Например, любая аксиома, полученная по схеме 1, может быть получена подстановкой формул в тавтологию x → (y → x), апотому сама является тавтологией (следствие 2.1).ÔÍ-12Выводимые формулы и тавтологии. Непротиворечивость теории N .

Полнота теории N .Разрешимость теории N . Независимость аксиом в теории N .ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓγ `X ∨Yчислении высказываний. Для этого достаточно использовать правило введения отрицания иправило доказательства от противного:ÌÃÒÓÌÃÒÓΓ, X, Y ` XÌÃÒÓÔÍ-12Γ`X ∧YÔÍ-12ÔÍ-12Γ, X ∧ Y ` XÌÃÒÓÌÃÒÓΓ, X ` YÌÃÒÓТеорема 3.5. Пусть Y — формула, построенная на переменных x1 , . . . , xn , f (ξ1 , . .

. , ξn ) —истинностная функция формулы Y , αi ∈ B, i = 1, n, — набор истинностных значений дляпеременных x1 , . . . , xn . Если f (α1 , . . . , αn ) = 1, то имеет место выводимость xα1 1 , . . . , xαnn ` Y .Если f (α1 , . . . , αn ) = 0, то имеет место выводимость xα1 1 , . . .

, xαnn ` ¬Y .Γ ` ¬(Z ∧ W )Γ, Z ∧ W ` ¬ZΓ, Z ∧ W ` ZΓ, Z, W ` ¬ZΓ, Z, W ` ZΓ, Z ∨ W ` UΓ, Z ` UΓ, Z ∨ W ` ¬UΓ, W ` UΓ, Z ` ¬UΓ, W ` ¬UÔÍ-12В результате получена выводимость Γ ` ¬Y , поскольку ¬Y = ¬(Z ∧ W ).Рассмотрим случай Y = Z ∨ W . Опять выберем набор значений α и введем, как и выше,обозначение Γ. Если одна из функций fZ fW на наборе α имеет значение 1, например fZ (α) = 1,то по индуктивному предположению имеет место выводимость Γ ` Z. Отсюда сразу получаемвыводимость Γ ` Z ∨ W = Y в силу правила введения дизъюнкции. Осталось рассмотретьвариант fZ (α) = fW (α) = 0. В этом варианте fY (α) = fZ (α) ∨ fW (α) = 0 и, значит, нужноустановить выводимость Γ ` ¬Y исходя из индуктивных предположений Γ ` ¬Z и Γ ` ¬W .Имеем:Γ ` ¬(Z ∨ W )ÌÃÒÓΓ ` ¬ZÔÍ-12J Доказательство строится индукцией по построению формулы.

В этом случае базис индукцииотносится к элементарным формулам, т.е. к переменным. Пусть Y = x и задано истинностноезначение α. При α = 1 имеем xα = x, Y = x, и севенция xα ` Y истинна, поскольку и левая,и правая части секвенции — одна и та же формула. При α = 0 имеем xα = ¬x, ¬Y = ¬x, иистинной является секвенция xα ` ¬Y .Чтобы доказать шаг индукции, необходимо в предположении, что утверждение верно дляформул Z и W , установить его истинность для формул (Z ∨ W ), (Z ∧ W ), (Z → W ) и (¬Z).Пусть z1 , . . . , zn — общий список переменных формул Z и W .Рассмотрим случай Y = Z ∧ W .

Для заданного набора α значений α1 , . . . , αn введемобозначение Γ = xα1 1 , . . . , xαnn . Предположим, что на наборе α истинностные функции fZ иfW принимают значение 1. Тогда по индуктивному предположению имеем Γ ` Z и Γ ` W ,откуда по правилу введения конъюнкции получаем выводимость Γ ` Y , так как Y = Z ∧ W .Пусть одна из истинностных функций, например fZ , принимает значение 0.

Тогда имеет местовыводимость Γ ` ¬Z. Используя правила естественного вывода, получаемÌÃÒÓÔÍ-12ÌÃÒÓИтак, множество формул, выводимых в теории N содержится в множестве всех тавтологий.На самом деле оба множества совпадают. Чтобы это доказать, установим одно вспомогательноеутверждение. Как и в случае булевых функций для произвольной пропозициональной переменной x введем обозначение xσ , σ ∈ B, полагая, что x1 = x и x0 = ¬x.ÔÍ-12ÔÍ-12Теорема 3.4.

Любая формула, выводимая в теории N , является тавтологией. #ÌÃÒÓÌÃÒÓЕсли формулы X и X → Y являются тавтологиями, то правило modus ponens приводит кформуле Y , также являющейся тавтологией (теорема 2.1). Это означает, что в любом выводевсе формулы являются тавтологиями, поскольку либо являются аксиомами, либо полученыиз тавтологий по правилу modus ponens (аккуратное доказательство может быть проведенометодом математической индукции по длине вывода). Можно также утверждать, что если всписке Γ все формулы — тавтологии, то и все формулы, выводимые из гипотез Γ, также будуттавтологиями.ÌÃÒÓÔÍ-12ÌÃÒÓ31ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123.

ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓÌÃÒÓΓ, Z → W ` ZΓ, Z → W ` ¬WΓ, Z → W ` Z → WΓ ` ¬WΓ`ZПусть fZ (α) = 0, fW (α) = 0. Тогда fY (α) = 1, и требуется установить Γ ` Z → W исходяиз Γ ` ¬Z и Γ ` ¬W . Из первой секвенции добавлением гипотезы получаем Γ, Z ` ¬Z, что сочевидной секвенцией Γ, Z ` Z по закону противоречия приводит к выводимости Γ, Z ` W идалее по правилу введения импликации к Γ ` Z → W .Рассмотрим случай Y = ¬Z. Если fZ (α) = 1, то fY (α) = 0 и Γ ` Z. Введением отрицания получаем Γ ` ¬¬Z = ¬Y .

Аналогично при fZ (α) = 0 имеем fY (α) = 1 и Γ ` ¬Z, чторавносильно Γ ` Y . IТеорема 3.6. Любая тавтология Y выводима в теории N .J Выводимыми в теории N являются только тавтологии. Если формула X выводима в теории N , то X — тавтология. Но тогда ¬X является противоречием и не относится к числувыводимых формул. IÔÍ-12Теорема 3.7. Теория N является непротиворечивой.ÌÃÒÓПолученное описание выводимых в теории N формул позволяет установить такие свойстваэтой теории, как непротиворечивость, полноту и разрешимость.

Установление этих свойств —цель, преследуемая при формализации любой теории.Под непротиворечивостью формальной теории понимают отсутствие в этой теории такойформулы X, для которой выводимыми являются и сама формула X, и ее отрицание ¬X. Иногда дают такое определение непротиворечивости теории: теория непротиворечива, если в нейсуществует невыводимая формула. Формально утверждение о выводимости любой формулысильнее, чем утверждение о выводимости какой либо пары X и ¬X (из первого утвержденияочевидно вытекает второе). Однако в данном случае оба подхода дают одно и то же: если втеории выводимы и X, и ¬X, то по закону противоречия выводима любая формула.ÔÍ-12J Пусть формула Y построена из переменных x1 , .

. . , xn . Поскольку Y — тавтология, ееистинностная функция на любом булевом векторе α принимает значение 1. Значит, для любыхзначений α1 , . . . , αn имеет место выводимость xα1 1 , . . . , xαnn ` Y .Обозначим Γ2 = xα2 1 , . . . , xαnn . Имеют место выводимости x1 , Γ2 ` Y и ¬x1 , Γ2 ` Y . Поправилу удаления конъюнкции находим x1 ∨ ¬x1 , Γ2 ` Y .

Используя выводимость ` x1 ∨ ¬x1 ,по правилу сечения получаем Γ2 ` Y .Повторяя рассуждения, последовательно убираем из списка гипотез переменные x2 , x3 и т.д.В конечном счете получим выводимость ` Y , что равносильно утверждению теоремы. IÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12Γ, Z → W ` WÌÃÒÓÌÃÒÓΓ ` ¬ZРассмотрим случай Y = Z → W . Выделим вариант fW (α) = 1. В этом варианте fY (α) = 1и нужно установить выводимость Γ ` Z → W исходя из Γ ` W .

Это верно в силу правилаприсоединения посылки. Пусть fZ (α) = 1, fW (α) = 0. Тогда fY (α) = 0, и нужно установитьвыводимость Γ ` ¬(Z → W ) исходя из Γ ` Z и Γ ` ¬W . Это можно сделать следующимобразом:Γ ` ¬(Z → W )ÔÍ-12ÔÍ-12Γ, Z ` ¬ZÌÃÒÓÌÃÒÓÌÃÒÓ32В результате требуемая секвенция оказадась сведена к четырем однотипным севенциям, в которых выбор формулы U (соответственно ¬U ) не имеет значения. Истинность всех четырехсевенций устанавливается по единому сценарию с помощью закона противоречия. Рассмотрим,например, первую из них:Γ, Z ` UΓ, Z ` ZÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-123.

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

Действительно, если, добавивв качестве аксиомы некоторую формулу X, мы найдем вывод формулы ¬X, то, с иной точкизрения, мы получим вывод ¬X из гипотезы X в теории N , т.е. X ` ¬X. Значит, согласно дереву (3.1), имеет место выводимость ` ¬X. Однако, как доказано, такое возможно только, еслиX — противоречие. Следовательно, добавление любой формулы, не являющейся тавтологиейили противоречием, дает непротиворечивую теорию.Впрочем, если в теорию ввести дополнительную схему аксиом, построенную на формуле, неявляющейся тавтологией, то подставляя в схему вместо символов подстановки определенныеформулы, можно получить противоречие. Это противоречие, с одной стороны, является аксиомой, поскольку получено из схемы аксиом, а с другой стороны, его отрицание есть тавтология,выводимая в теории N .

Пусть например, схема аксиом построена на формуле, представленнойистинностной функцией f (x1 , . . . , xn ). Так как формула — не тавтология, существует наборзначений α1 , . . . , αn аргументов функции, на котором она принимает значение 0. Каждуюпеременную xj заменим формулой xj ∨ ¬xj , если αj = 1, и формулой xj ∧ ¬xj . Полученнаяформула, построенная по схеме аксиом, будет противоречием.При построении исчисления высказываний (и далее исчисления предикатов) различают полноту в широком смысле, означающую сказанным выше, и полноту в узком смысле, означающую, что выводимыми являются все тавтологии. В узком смысле теория N полна.

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