Полнота КИВ

КИВ - не имеет сильной полноты, поскольку в ней нельзя ни доказать, ни опровергннуть нейтральную формулу булевой алгебры.

КИВ обладает слабой полнотой в том смысле, что всякую тавтологию БА (булевой алгебры) можно доказать в КИВ (если в КИВ такая формула допустима). Это утверждение требует обоснования в соответствующей метатеореме (Эрбрана), которую мы сейчас и рассмотрим.

Формулировка теоремы Эрбрана:

Всякая тавтология БА, выглядящая как формула КИВ, может быть доказана в КИВ как теорема.

Доказательство

Оговорка "выглядящая как формула КИВ" подразумевает, что некоторые тавтологии БА все-таки не могут быть доказаны в КИВ, если определение понятия "формулы" сделать разным в КИВ и в БА.

Так например, если в алфавите КИВ не предусмотреть символа true, то нельзя будет доказать тавтологию БА: (X ó X) ó true.

Рассмотрим произвольную формулу Z, которая является тавтологией БА и формулой КИВ. Покажем, как в КИВ можно построить доказательство, которое даст этой формуле звание "теорема".

Используем метод, описанный в "метатеореме о применении КИВ-таблиц". Составим с помощью этой теоремы по одному доказательству для каждой возможной комбинации значений переменных. Поскольку формула Z у нас - тавтология, то во всех этих доказательствах справа от знака будет стоять Z (что соответствует значению формулы true), и ни в одном не будет стоять ~Z (что соответствовало бы false).

Если у нас β переменных, то всего получится 2β метатеорем. Например, для трех переменных z1, z2, z3 получим метатеоремы:

~z1, ~z2, ~z3 |— Z

~z1, ~z2, z3 |— Z

~z1, z2, ~z3 |— Z

~z1, z2, z3 |— Z

z1, ~z2, ~z3 |— Z

z1, ~z2, z3 |— Z

z1, z2, ~z3 |— Z

z1, z2, z3 |— Z

Возьмем эти метатеоремы и сгруппируем их попарно так, чтобы отличие между парными метатеоремами было только в последней гипотезе. С помощью метатеоремы MT_Not_6 мы из каждой пары сможем составить новую метатеорему, которая во всем совпадает с исходными гипотезами пары, но из нее исключена последняя гипотеза. В рассмотренном примере это будут метатеоремы:

~z1, ~z2 |— Z

~z1, z2 |— Z

z1, ~z2 |— Z

z1, z2 |— Z

Эти метатеоремы тоже объединим попарно, получим еще несколько метатеорем, где гипотез будет меньше на одну. Продолжая в том же духе в конце-концов придем к двум метатеоремам, содержащим всего по одной гипотезе:

~z1 |— Z

z1 |— Z

Последний раз применив MT_Not_6, получим Z, то есть, искомое доказательство формулы Z.

Заключение

Помимо многочисленных вариантов КИВ, есть и другие похожие (но не эквивалентные) дедуктивные системы. Самая известная из них - интуиционистская логика. В ней эксперимента ради была выброшена одна из аксиом (~~a => a) и заменена на (~a => (b => b)). В результате получилась вполне развитая дедуктивная система, в чем-то похожая на КИВ, но где-то дающая другие результаты. Тем самым было показано, что вполне может быть логика, отличающаяся от "классической", но вполне развитая.

Булева алгебра и КИВ во многом взаимозаменяемы. Теоремам КИВ соответствуют тавтологии булевой алгебры. Невыполнимые формулы булевой алгебры могут быть опровергнуты в КИВ. Нейтральные формулы булевой алгебры не могут быть ни доказаны, ни опровергнуты в КИВ (т.е. может быть доказано их отрицание). В рассмотренном нами варианте КИВ нет символов true и false, но это не принципиально, поскольку есть варианты КИВ и с этими символами. Если интересно, можете добавить две простые дополнительные аксиомы: true и ~false - и посмотреть, что получится.

Некоторая взаимозаменяемость вовсе не означает равноценность - эти две системы имеют много важных различий.

Когда речь заходит об определении истинности или доказанности некоторой формулы, булева алгебра удобнее. Проще составить таблицу истинности (тем более, с помощью компьютера), чем долго угадывать подходящую теорему или метатеорему КИВ. А во что разворачиваются все эти бесчисленные стрелки и скобки, когда их начинаешь применять к формулам хотя бы в 5-6 переменных - просто страшно смотреть.

Полезность КИВ заключается прежде всего в том, что на ее примере можно освоиться с такими понятиями, как аксиома, теорема, доказательство, гипотеза, полнота и непротиворечивость и т.д. В булевой алгебре всего этого нет в таком явном, подчеркнутом виде. Также на примере КИВ можно понять принципы, по которым проводят грань между языком и метаязыком.

Формулы булевой алгебры, когда их переносят в естественный язык, по большей части работают безупречно - за исключением материальной импликации, которая в этом случае, напротив, ведет к опасным парадоксам. Пока рассмотрение материальной импликации ограничивается математикой - все хорошо, но как только ее начинают применять в естественном языке - возникают кое-какие проблемы (так называемые парадоксы материальной импликации). Что касается КИВ - в ней все крутится именно вокруг материальной импликации, поэтому применение КИВ в естественном языке проблематично. Даже некоторые аксиомы КИВ (например, Imp1) в естественном языке не выполняются.