Исчисление высказываний гильбертовского типа
Теперь построим исчисление ИВ, в котором в отличие от ИС не используется понятие секвенции, правило вывода одно, а схем аксиом — несколько.
Формулами ИВ называются формулы ИС.
Аксиомами ИВ являются следующие формулы для любых формул φ, , χ:
()
()((())())
()
()
()(()(()))
()
()
()(()(()))
()(())
Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.
Единственным правилом вывода в ИВ является правило заключения (modus ponens): если φ и φ ― выводимые формулы, то ― также выводимая формула. Будем это записывать так:
.
Например, если высказывания АВ и АВ (А С) выводимы, то высказывание АС также выводимо согласно правилу заключения.
Говорится, что формула φ выводима из формул φ1, ..., φn (обозначается φ1, ..., φn├φ), если существует последовательность формул 1,...,n, φ, в которой любая формула либо является аксиомой, либо принадлежит списку формул φ1, ..., φn, называемых гипотезами, либо получается из предыдущих по правилу вывода. Выводимость формулы φ из (├ φ) равносильна тому, что φ ― теорема ИВ.
Пример 1. Покажем, что формула φ φ выводима в ИВ. Для этого построим вывод данной формулы:
в схеме аксиом 2 формулу заменим на φ φ, χ ― на φ. Получаем аксиому (φ (()) ((φ (( φ) )())
в схеме аксиом 1 формулу заменим на φ. Получаем ()
из 1 и 2 по правилу modus ponens заключаем ((()))()
в схеме аксиом 1 заменяем на φ φ. Получаем ((()))
из пп. 3 и 4 по правилу вывода справедливо ├
Теорема 1. (теорема о дедукции). Если Γ,φ ├, то Г ├, где Г ― набор некоторых формул φ1, ..., φn..
Доказательство. Рассмотрим минимальный вывод 1,…,k формулы = к из формул 1,…,n и . Если к = 1, то =φ, или ― аксиома, или входит в Г. В первом случае в силу примера 1.6.1 формула выводима в ИВ из Г. Во втором и третьем случаях последовательность , (), будет выводом в ИВ из Г.
Предположим, что к > 1 и формула получается из формул i и j=i (где i, j < к) по правилу заключения. Поскольку i < к и j < к по индукции можно считать, что Г├i и Г├φ (i). Используя аксиому 2, получим (i)(((i))())и дважды применяя к этой формуле правило заключения с формулами i и (i) получаем сначала формулу ((i))(), а затем формулу . Тем самым, выводимость формулы из Г доказана.
Применение теоремы о дедукции позволяет во многих случаях сокращать доказательство формул.
Пример
2.
Покажем, что формула
(
(φ
))
доказуема
в ИВ для любых формул φ
и
ИВ.
По теореме о дедукции достаточно показать
φ,
\- φ
.
Построим
вывод формулы φ
из
гипотез φ
и
:
из аксиомы 1 () и гипотезы получаем формулу ;
из аксиомы 1 () и гипотезы получаем формулу ;
из заключения п. 1 и аксиомы ()(()(())) получаем ()(());
из заключения пп. 2 и 3 выводится формула ();
из гипотезы и заключения п. 4 получаем формулу .
Следствие. Тогда и только тогда 1,... ,n ├, когда ├(1(2…(n)…))
Доказательство. Пусть 1,... ,n ├. Тогда, применяя теорему о дедукции, имеем 1,... ,n-1 ├n. Аналогично, продолжая процесс необходимое число раз, получаем ├(1(2…(n)…)). Для доказательства достаточности предположим, что ├, где = (1(2…(n)…)). Очевидно, 1├. По правилу заключения получаем 1├(2…(n)…). Далее через n шагов имеем 1,... ,n ├.
Следующая теорема устанавливает эквивалентность доказуемости в ИС и доказуемости в ИВ.
Теорема 2. (теорема об эквивалентности ИС и ИВ)
Секвенция 1,... ,n ├ доказуема в ИС тогда и только тогда, когда формула выводима в ИВ из формул 1,... ,n .
Секвенция 1,... ,n ├ доказуема в ИС тогда и только тогда, когда формула А А выводима в ИВ из формул 1,... ,n .
Доказательство. Так как доказуемость (тождественная истинность) секвенций 1,... ,n ├·и 1,... ,n ├ равносильна доказуемости (соответственно тождественной истинности) формул (1(2…(n)…))) и (1(2…(nАА)…)) соответственно, в силу следствия достаточно показать, что доказуемость формулы φ в ИС равносильна доказуемости формулы φ в ИВ. Непосредственно проверяется, что все аксиомы ИВ тождественно истинны, а правило заключения сохраняет тождественную истинность. Поэтому по теореме о полноте из выводимости формулы φ в ИВ следует ее доказуемость в ИС.
Для доказательства выводимости в ИВ доказуемой в ИС формулы φ достаточно проследить сохранение истинности утверждений ИВ, соответствующих секвенциям, при переходе по любому из 12 правил вывода ИС. Сохранение выводимости в ИВ для правил 1-5 устанавливается с помощью примера 2 и аксиом 3-7. Если в ИВ справедливо 1,... ,k ,├ и 1,... ,k ,├, 1,... ,k ├, то по теореме о дедукции 1,... ,k ├ и 1,... ,k ├. Применяя три раза правило заключения к аксиоме 8, получаем 1,... ,k ├. Следовательно, правило 6 сохраняет выводимость. Правило 7 соответствует теореме о дедукции, а правило 8 — правилу заключения. Для доказательства сохранения выводимости правилом 9 рассмотрим справедливое в ИВ соотношение 1,... ,k ,├AA. Из аксиом 3 и 4 получаем 1,... ,k ,├A и 1,... ,k ,├A. По теореме о дедукции имеем 1,... ,k ├A и 1,... ,k ├A. Из аксиом 9 и 10 заключаем 1,... ,k ├. Рассмотрим правило 10. Если 1,... ,k ├ и 1,... ,k ├, то из аксиомы 1 получаем 1,... ,k ├(AA) и 1,... ,k ├(AA). Из аксиом 9 и 10 заключаем 1,... ,k ├(AA),. Сохранение выводимости по правилам 11 и 12 следует из определения вывода в ИВ.
Из теоремы 1.6.3. вытекает непротиворечивость и разрешимость ИВ. Непосредственно проверяется независимость схем аксиом ИВ.
Множество формул Г называется противоречивым, если в ИВ справедливо Г├ΑА. Если Г ― противоречивое множество формул, будем обозначать этот факт через Г├.
На основании теоремы 2 справедливо следующее
Утверждение. Формула φ выводима в ИВ из множества формул Г тогда и только тогда, когда множество Г{} ― противоречиво: Г├ Г{}├ .