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

. . , αn ) = 1, то имеет место выводимость xα1 1 , . . . , xαnn ` Y .Если f (α1 , . . . , αn ) = 0, то имеет место выводимость xα1 1 , . . . , xαnn ` ¬Y .ÔÍ-12Остановимся на описании множества выводимых формул в теории N . Нетрудно убедитьсяв том, что все аксиомы этой теории являются тавтологиями . Например, любая аксиома, полученная по схеме 1, может быть получена подстановкой формул в тавтологию x → (y → x), апотому сама является тавтологией (следствие 1.1).Если формулы X и X → Y являются тавтологиями, то правило modus ponens приводит кформуле Y , также являющейся тавтологией (теорема 1.1). Это означает, что в любом выводевсе формулы являются тавтологиями, поскольку либо являются аксиомами, либо полученыиз тавтологий по правилу modus ponens (аккуратное доказательство может быть проведенометодом математической индукции по длине вывода).

Можно также утверждать, что если всписке Γ все формулы — тавтологии, то и все формулы, выводимые из гипотез Γ, также будуттавтологиями.ÌÃÒÓÔÍ-12ÌÃÒÓΓ ` ¬¬(X ∨ Y )ÔÍ-12ÔÍ-12Γ`X ∨YÌÃÒÓÌÃÒÓправило доказательства от противного:ÌÃÒÓÔÍ-12ÌÃÒÓ21ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-122. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓÔÍ-12Γ ` ¬(Z ∧ W )Γ, Z ∧ W ` ZΓ, Z, W ` ¬ZΓ, Z, W ` ZΓ ` ¬ZВ результате получена выводимость Γ ` ¬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 )Γ, W ` ¬UВ результате требуемая секвенция оказадась сведена к четырем однотипным севенциям, в которых выбор формулы U (соответственно ¬U ) не имеет значения. Истинность всех четырехсевенций устанавливается по единому сценарию с помощью закона противоречия. Рассмотрим,например, первую из них:Γ, Z ` UΓ, Z ` ZΓ, Z ` ¬ZΓ, Z → W ` WΓ, Z → W ` ZΓ, Z → W ` Z → WΓ, Z → W ` ¬WΓ ` ¬WÔÍ-12Γ`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ÌÃÒÓΓ ` ¬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 ` ¬UÔÍ-12ÔÍ-12Γ, W ` UÌÃÒÓΓ, Z ` UΓ, Z ∨ W ` ¬UÌÃÒÓÔÍ-12Γ, Z ∧ W ` ¬ZÔÍ-12ÌÃÒÓÌÃÒÓ22fW принимают значение 1. Тогда по индуктивному предположению имеем Γ ` Z и Γ ` W ,откуда по правилу введения конъюнкции получаем выводимость Γ ` Y , так как Y = Z ∧ W .Пусть одна из истинностных функций, например fZ , принимает значение 0.

Тогда имеет местовыводимость Γ ` ¬Z. Используя правила естественного вывода, получаемΓ, Z ∨ W ` UÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-122. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ23Теорема 2.6. Любая тавтология Y выводима в теории N .J Пусть формула 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Полученное описание выводимых в теории N формул позволяет установить такие свойстваэтой теории, как непротиворечивость, полноту и разрешимость. Установление этих свойств —цель, преследуемая при формализации любой теории.Под непротиворечивостью формальной теории понимают отсутствие в этой теории такойформулы X, для которой выводимыми являются и сама формула X, и ее отрицание ¬X. Иногда дают такое определение непротиворечивости теории: теория непротиворечива, если в нейсуществует невыводимая формула.

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

Другими словами, в такой теории Для каждой формулы X выводима либо сама формула, либо ее отрицание. Наша теория не полна в этом смысле. Действительно, если, добавивв качестве аксиомы некоторую формулу X, мы найдем вывод формулы ¬X, то, с иной точкизрения, мы получим вывод ¬X из гипотезы X в теории N , т.е.

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

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

В узком смысле теория N полна. Впрочем, отсутствие полноты в широком смысле легко устраняется простой модификацией формальнойтеории: достаточно вместо каждой схемы аксиом записать обычную аксиому, заменив местаподстановки переменными и добавить еще одно правило вывода, заключающееся в подстановкевместо переменных произвольных формул. Отметим, что свойством полноты обладают оченьÔÍ-12ÔÍ-12J Выводимыми в теории N являются только тавтологии.

Если формула X выводима в теории N , то X — тавтология. Но тогда ¬X является противоречием и не относится к числувыводимых формул. IÌÃÒÓÌÃÒÓТеорема 2.7. Теория N является непротиворечивой.ÌÃÒÓТеорема 2.8. Схемы аксиом исчисления N не зависят друг от друга.ÌÃÒÓJ Наиболее просто доказать независимость схем, начиная с 3-й, так как все эти схемы используют, кроме импликации, еще одну операцию, которая участвует лишь в двух других схемахаксиом.

Можно ограничиться двухэлементной областью изменения переменных и стандартнойинтепретацией операций, кроме одной. В табл. 2.1 приведены схемы аксиом и новая интерпретация одной из операций. При этой интерпретации указанная схема аксиом при некоторыхзначениях входящих в нее формул принимает значение 0, в то время как остальные аксиомыÔÍ-12ÌÃÒÓÔÍ-12простые математические теории: согласно теореме Геделя о неполноте любая достаточно содержательная теория не является полной, поскольку в рамках такой теории удается построитьтакую формулу Z, что ни эта формула, ни ее отрицание не являются выводимыми.Под разрешимостью теории понимают наличие алгоритма, который для любой формулыпозволяет установить за конечное число элементарных операций, выводима эта формула илинет. В данном случае в качестве такого алгоритма может рассматривать процедуру построения истинностной функции и проверки ее на наличие значений 0. Отсутствие таких значенийозначает, что функция является постоянной, а формула — тавтологией, т.е.