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

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

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

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

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

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

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

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

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

Если у нас β переменных, то всего получится 2^β метатеорем. Например, для трех переменных z₁, z₂, z₃ получим метатеоремы:

~z₁, ~z₂, ~z₃ Z
~z₁, ~z₂, z₃ Z
~z₁, z₂, ~z₃ Z
~z₁, z₂, z₃ Z
z₁, ~z₂, ~z₃ Z
z₁, ~z₂, z₃ Z
z₁, z₂, ~z₃ Z
z₁, z₂, z₃ Z

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

~z₁, ~z₂ Z
~z₁, z₂ Z
z₁, ~z₂ Z
z₁, z₂ Z

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

~z₁ Z
z₁ Z

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