Правила вывода КИВ

Самое знаменитое из всех правил вывода имеет собственное звучное латинское название: modus ponens. Далее обозначается как MP.

DEF[modus ponens]: Правило вывода modus ponens:

X, X => Y |-> Y // MP,

где X и Y - формулы КИВ (а следовательно и X => Y - тоже формула КИВ, согласно одному из правил построения формул). В комментарии к дедуктивному шагу будем писать аббревиатуру правила вывода "MP".

Формула X, участвующая в MP, немудрено называется "малой посылкой", а формула X => Y - "большой посылкой". Формула Y в результате будет доказана, если малая и большая посылка доказаны.

Пример:

a => (b => a), (a => (b => a)) => (a => a) |-> a => a // MP,

Или сокращенно:

a(ba), (a(ba)) (aa) |-> aa // MP,

С точки зрения оформления слева от значка |-> лучше писать не сами формулы, а номера шагов, на которых они были получены. Так получится и короче, и понятнее: для проверки доказательства не придется просматривать все предшествующие шаги дедукции в поисках места, где формула была доказана. Если одна из формул является аксиомой, то вместо номера шага будет ее краткое обозначение (Imp1, Imp2,...).

Второе правило вывода КИВ - это правило подстановки:

X(a, b, c) |-> X(A, B, C) // a ~> A, b ~> B, c ~> C,

где X(a, b, c) - некоторая аксиома; a, b, c - переменные, которые встречаются в этой аксиоме КИВ; A, B, C - любые формулы КИВ. X(A, B, C) - формула КИВ, которая получается при замене в аксиоме переменных a, b, c на соответствующие формулы A, B, C. В комментарии будем писать, что на что заменяется через значок "~>". В общем случае могут быть заменены все переменные, в некоторых случаях может хватить замены только некоторых их них. Например:

a => (b => a) |-> a => ((b => z) => a) // b ~> (b => z),

Или коротко:

a(ba) |-> a(bza) // b ~> bz,

С точки зрения оформления слева от значка |-> можно писать не саму аксиому, а ее краткое обозначение: Imp1, Imp2,...

Скажем несколько слов о других вариантах.

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

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