Эквивалентные
системы аксиом
[предыдущая глава]  [оглавление]  [следующая глава]

В доказательстве метатеоремы дедукции мы рассмотрели два варианта: когда среди наших аксиом есть аксиомы Imp1 и Imp2 и когда среди наших аксиом есть аксиомы Imp1 и Imp2'. То есть, эта метатеорема верна и при том, и при другом выборе аксиом. Помимо них в доказательстве используются только те аксиомы, которые пришли вместе с исходным доказательством G1, G2,..., Gβ-1, Gβ R. Поэтому метатеорема дедукции будет верна для любого варианта КИВ, в котором есть либо аксиомы Imp1 и Imp2, либо аксиомы Imp1 и Imp2'. Остальные аксиомы не имеют значения для теоремы дедукции.

Более того, в последующих главах будут использоваться не аксиомы Imp1, Imp2, Imp2', а теорема дедукции, которая из них получается. Поэтому, в принципе, можно саму теорему дедукции считать аксиомой (или правилом вывода), а аксиомы Imp1/Imp2 исключить.

До сих пор мы не определились с выбором, какую из аксиом использовать: Imp2 или Imp2'. Во всех рассуждениях мы рассматривали оба варианта. Теперь мы докажем, что это не имеет значения. А точнее так: если принять за аксиомы Imp1 и Imp2, то можно будет доказать Imp2' как теорему. А если, наоборот, принять за аксиомы Imp1 и Imp2', то можно будет доказать как теорему Imp2. Получается, что эти два варианта КИВ в конечном счете приведут к одним и тем же доказанным формулам. Вот вам один из примеров, когда есть два взаимозаменяемых варианта КИВ.

Еще раз напомню аксиомы:

Imp2:

ab ((a(bc))(ac))

Imp2':

a(bc) ((ab)(ac))

Возьмем в качестве аксиомы Imp2. Поскольку аксиома - формула доказанная, то можно написать:

ab ((a(bc))(ac))

Теперь передвинем значок слева направо, используя MP:

ab ((a(bc))(ac))

ab (a(bc))(ac)

ab, a(bc) ac

Переставим местами гипотезы

a(bc), ab ac

Теперь передвинем значок обратно, используя МТД:

a(bc) (ab)(ac)

a(bc) (ab)(ac)

- получилась Imp2' как теорема.

Аналогично можно получить Imp2 из Imp2'. Достаточно выписать все те же самые формулы, только в обратном порядке.

Далее для ясности будем считать Imp2 аксиомой, а Imp2' - теоремой.