Рефлексивность

z => z - вот уж формула достойная того, чтобы называться "аксиомой" в том смысле, что она кажется простой и очевидной. Так почему она не входит в список аксиом? Просто потому, что аксиом должно быть как можно меньше, а эту формулу можно доказать на основе Imp1 и Imp2 (или Imp1 и Imp2'). С другой стороны, не получится доказать, скажем, Imp1 на основе Imp2 и формулы z => z; или Imp2 на основе Imp1 и формулы z => z. Так что минимальный вариант - это две первые аксиомы Imp1 и Imp2 (или Imp1 и Imp2').

Некоторая несуразность ощущается в том, что со школьной геометрии мы привыкли: аксиомы проще, чем теоремы, которые из этих аксиом получаются. Данный пример демонстрирует нам, что это вовсе необязательно. В школе вообще рекомендуется двигаться от простого к сложному из чисто дидактических соображений - так легче усваивается материал. Здесь же цель была в том, чтобы минимизировать число аксиом. Итак, докажем формулу z => z, которую еще называют "законом рефлексивности". Для наглядности напомню три первые аксиомы, которые нам понадобятся.

Imp1:

a(ba)

Imp2:

ab (a(bc)(ac))

Imp2':

a(bc) (ab(ac))

Доказательство закона рефлексивности:

1) Imp1 |-> z(bz) // a ~> z

2) Imp1 |-> z(bzz) // a ~> z, b ~> bz

3) Imp2' |-> z(bzz) (z(bz)(zz)) // a ~> z, b ~> bz, c ~> z

4) №2, №3 |-> z(bz)(zz) // MP

5) №1, №4 |-> zz // MP

Здесь мы доказали формулу на основании аксиом Imp1 и Imp2'. На шагах 1-3 мы сначала сделали серию замен, исходя из аксиом Imp1 и Imp2'. Далее было дважды применено правило MP, чтобы упростить формулу до получения нужного результата.

Теперь доказательство того же самого на основании аксиом Imp1 и Imp2:

1) Imp1 |-> z(bz) // a ~> z

2) Imp1 |-> z(bzz) // a ~> z, b ~> bz

3) Imp2 |-> z(bz) (z(bzz)(zz)) // a ~> z, b ~> bz, c ~> z

4) №1, №3 |-> z(bzz)(zz) // MP

5) №2, №4 |-> zz // MP

В доказательстве виден полезный прием. Если в левой части некоторой формулы стоит что-то похожее на простейший вариант аксиомы - например, фрагмент z(bzz) похож на аксиому a(ba),- то с помощью правила подстановки пытаемся получить этот фрагмент из аксиомы. Затем применяем MP, чтобы оставить только правую часть формулы.

Тем же способом можно доказать не только формулу z z, но вообще любую формулу вида X X, где X - некоторая формула КИВ. Потребуется лишь заменить повсюду в доказательстве переменную z на формулу X. В качестве упражнения докажите формулу (a b) (a b).

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

1) Imp1 |-> X(b X) // a ~> X

2) Imp1 |-> X(b X X) // a ~> X, b ~> b X

3) Imp2' |-> X(b X X) (X(b X)(X X)) // a ~> X, b ~> b X, c ~> X

4) №2, №3 |-> X(b X)(X X) // MP

5) №1, №4 |-> X X // MP