Другие аксиоматизации исчисления высказываний

Другие аксиоматизации исчисления высказываний

Выше мы построили формальную систему, в которой выводимы тавтологии и только они. Такая система, разумеется, не единственна. Можно изменять наборы пропозициональных связок, входящих в формулы, наборы аксиом или правила вывода.
Если, например, не заботиться о независимости аксиом, то можно включить в схемы аксиом все формулы, которые использовались для доказательства корректности и полноты ИВ (их конечное число). Получим формальную систему, в которой выводимы тавтологии и только они, причём доказательство полноты значительно упрощается, а в доказательстве корректности нужно будет проверить тавто- логичность всех этих формул.
В рассмотренной нами формальной системе ИВ представлены только две пропозициональные связки 1 и —Чтобы записать высказывание, которое является дизъюнкцией высказываний А и В, в такой формальной системе нужно написать формулу Л А—>В. Поскольку 1 и -> образуют полную систему функций, то остальные связки также реализуются формулами ИВ. Такой подход несколько сокращает доказательства, но в других отношениях неудобен.
Наиболее естественным набором пропозициональных связок является набор {1, Л, V, —»} (мы перечислили связки в порядке убывания старшинства). Приведём формальную систему КИВ (классическое исчисление высказываний), в которой используется этот набор, причём выводимы в точности тавтологии. Алфавит КИВ состоит из счётного множества переменных, пропозициональных связок 1,A,V, —» и скобок. Определение формулы для КИВ почти дословно повторяет данное для ИВ, только добавляются ещё две возможности построения формул (А V В) и (А А В). Правило вывода остаётся прежним: modus ponens. А вот список схем аксиом изменяется и становится намного длиннее:

Несмотря на большое количество аксиом, проверка корректности КИВ не вызывает затруднений. Оба подхода к доказательству теоремы о полноте по прежнему применимы.
Рассуждения становятся, конечно, длиннее, но их суть не меняется.
Вернёмся к формулам, в которые входят только связки 1, —к Можно ли построить формальную систему, в которой выводимы в точности тавтологии и в которую входит лишь конечное число аксиом? (В системе ИВ аксиом бесконечно много.) Легко понять, что это невозможно, если ограничиться только правилом вывода modus ponens: в конечное число аксиом будет входить лишь конечное число переменных, поэтому выводимыми будут лишь формулы, использующие эти переменные, а тавтология может содержать сколь угодно большое число переменных.
Добавим ещё одно правило вывода - правило подстановки. Оно состоит в том, что если выводима формула А, то выводимы также формулы, которые получаются из А подстановкой вместо переменных произвольных формул (разумеется, каждое вхождение переменной нужно заменять на одну и ту же формулу).
Выберем в качестве аксиом три формулы (А1 АЗ). Полученную формальную систему назовём исчислением высказываний с подстановкой. В этой системе по-прежнему выводимы в точности тавтологии.
Корректность исчисления высказываний с подстановкой вытекает из того, что подстановка сохраняет тавтологичность формул.
Любой вывод в ИВ можно преобразовать в вывод в исчислении высказываний с подстановкой, заменяя каждое использование схемы аксиом на использование соответствующей аксиомы и последующую подстановку. Отсюда следует полнота исчисления высказываний с подстановкой.
Непосредственный анализ исчисления высказываний с подстановкой оказывается менее удобным. В частности, здесь не выполняется теорема дедукции. Действительно, из формулы х можно получить подстановкой любую формулу
А, поэтому х Ь А. Однако не любая формула вида х—>А является тавтологией, например, х—>у — не тавтология.
Задачи
1.24. Проверьте корректность (выводимы только тавтологии) и полноту (все тавтологии выводимы) формальных систем, в которых множество формул совпадает с множеством формул ИВ, правило вывода modus ponens, а схемы аксиом имеют вид

1.25. Найдите конечный набор А схем аксиом такой, что в формальной системе с тем же множеством формул, что и в ИВ, со схемами аксиом А и правилом вывода

выводимы тавтологии и только они.
1.26. Изменится ли множество выводимых формул, если к ИВ добавить ещё одно правило вывода