КИВ-таблицы
[предыдущая глава]  [оглавление]  [следующая глава]

В булевой алгебре можно построить таблицу истинности для всякой формулы. В КИВ можно строить похожие таблицы. Будем называть таблицы истинности в булевой алгебре БА-таблицами, а аналогичные таблицы в КИВ - КИВ-таблицами. КИВ-таблица строится на основе БА-таблицы по такому принципу:

Например, из БА-таблицы:

AB~(A & B)
falsefalsetrue
falsetruetrue
truefalsetrue
truetruefalse

Получается КИВ-таблица:

~A, ~B ~(A & B)
~A, B ~(A & B)
A, ~B ~(A & B)
A, B ~~(A & B)

Будут ли верными формулы, из которых состоят КИВ-таблицы? Да, это так: все они будут истинными, но это следует доказать.

Докажем, что верна КИВ-таблица для формулы ~X. Напомним БА-таблицу для этой формулы:

X~X
truefalse
falsetrue

Соответствующая КИВ-таблица:
1.~X ~X
2. X ~(~X)

Докажем, что верна КИВ-таблица для формулы X Y. Напомним БА-таблицу для этой формулы:

X Y X Y
falsefalsetrue
falsetrue true
true falsefalse
true true true

Соответствующая КИВ-таблица:
3.~X, ~Y X Y
4.~X, Y X Y
5. X, ~Y ~(X Y)
6. X, Y X Y

Докажем, что верна КИВ-таблица для формулы X & Y. Напомним БА-таблицу для этой формулы:

X Y X & Y
falsefalsefalse
falsetrue false
true falsefalse
true true true

Соответствующая КИВ-таблица:
7.~X, ~Y ~(X & Y)
8.~X, Y ~(X & Y)
9. X, ~Y ~(X & Y)
10. X, Y X & Y

Докажем, что верна КИВ-таблица для формулы X Y. Напомним БА-таблицу для этой формулы:

X Y X Y
falsefalsefalse
falsetrue true
true falsetrue
true true true

Соответствующая КИВ-таблица:
11.~X, ~Y ~(X Y)
12.~X, Y X Y
13. X, ~Y X Y
14. X, Y X Y

Докажем, что верна КИВ-таблица для формулы X Y. Напомним БА-таблицу для этой формулы:

X Y X Y
falsefalsetrue
falsetrue false
true falsefalse
true true true

Соответствующая КИВ-таблица:
15.~X, ~Y X Y
16.~X, Y ~(X Y)
17. X, ~Y ~(X Y)
18. X, Y X Y

Докажем, что верна КИВ-таблица для формулы X Y. Напомним БА-таблицу для этой формулы:

X Y X Y
falsefalsefalse
falsetrue true
true falsetrue
true true false

Соответствующая КИВ-таблица:
19.~X, ~Y ~(X Y)
20.~X, Y X Y
21. X, ~Y X Y
22. X, Y ~(X Y)

Рассмотрим пример. Пусть у нас есть формула

~(A B) (B & ~A & C)

Для ее вычисления надо последовательно выполнить операции:


A B - результат R1
~R1 - результат R2
~A - результат R3
B & R3 - результат R4
R4 & C - результат R5
R2 R5 - результат R6

Теперь возьмем конкретные величины: A = true, B = false, C = false и начнем вычислять истинность формулы.

Параллельно будем выписывать доказательства КИВ, по одному на каждую операцию БА, составленные по следующим правилам (для ω-й по счету операции):

  • Написать Rω.
  • Добавить операнды булевой операции как гипотезы КИВ слева от .
  • Поставить "~" перед теми гипотезами, для которых соответствующий операнд в БА равен false.
  • Поставить "~" перед Rω в КИВ, если результат в БА равен false.

 БАКИВ
1 A B - результат R1 = true A, ~B R1
2 ~R1 - результат R2 = false R1 ~R2
3 ~A - результат R3 = false A ~R3
4 B & R3 - результат R4 = false ~B, ~R3 ~R4
5 R4 & C - результат R5 = false ~R4, ~C ~R5
6 R2 R5 - результат R6 = true ~R2, ~R5 R6

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

Тем самым каждый новый сегмент доказательства соблюдает требование дедуктивной системы: что новые формулы должны доказываться на основе ранее уже доказанных. Чтобы получить из правого столбца таблицы полноценное доказательство, нужно определить R1, R2,.... Это можно сделать по заготовленным выше КИВ-таблицам, в которых были как раз предусмотрены все возможные случаи:


A, ~B A B
A B ~~(A B)
A ~~A
~B, ~~A ~(B & ~A)
~(B & ~A), ~C ~(B & ~A & C)
~~(A B), ~(B & ~A & C) ~(A B) (B & ~A & C)

Следовательно мы можем написать метатеорему:

A, ~B, ~C ~(A B) (B & ~A & C)

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

Метатеорема о применении КИВ-таблиц.

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

Если формула Z булевой алгебры имеет β переменных z1, z2,... zβ и принимает значение истинности Ψ, когда переменные принимают значения истинности ψ1, ψ2,... ψβ соответственно, то в КИВ можно составить доказательство:

K1, K2,... Kβ K.

- где

Kω = ~zω, когда ψω = false, Kω = zω, когда ψω = true

K = ~Z, когда Ψ = false, K = Z, когда Ψ = true