Основы математической логики и теории алгоритмов
Подождите немного. Документ загружается.
2. s(φψ)=s(φ)s(ψ)
3. s(φψ)=s(φ)s(ψ)
4. s(φ→ψ)=s(φ)→s(ψ)
П р и м е р . Если s(P
0
) = P
1
Р
2
, s(P
1
) = P
2
→Рз, φ = P
0
P
1
, то s(φ) =
( P
1
Р
2
)( P
2
→Рз).
Для любой секвенции (последовательности формул) R обозначим через s(R)
секвенцию (последовательность формул), получающуюся из R заменой всех
пропозициональных переменных Р, входящих в R, на формулы s(P), т.е.
s(φ
1
,
…,φ
n
├ψ)=s(φ
1
),…,s(φ
n
)├s(ψ).
Таким образом, отображение s естественным образом расширяется на
множество всех выражений исчисления ИС.
Следующая теорема утверждает, что подстановкой в доказуемую секвенцию
произвольных формул вместо пропозициональных переменных получается также
доказуемая секвенция.
Теорема (теорема о подстановке). Если s ― подстановка, R ― доказуемая
секвенция, то
)(RS
R
- допустимое правило.
Доказательство. Предположим, что секвенция R доказуема. Индукцией по
длине доказательства R покажем, что секвенция s(R) также доказуема. Если R ―
аксиома, равная φ├φ, то секвенция s(R) имеет вид s(R)├ s(R) и, значит, является
аксиомой. Предполагая, что R не является аксиомой, рассмотрим дерево D
доказательства секвенции R. Так как заключительный переход в дереве D к секвенции
R осуществляется по одному из двенадцати правил вывода, в силу индукционного
предположения достаточно установить, что переход по каждому из двенадцати правил
вывода с заключением R преобразуется подстановкой s к соответствующему правилу
вывода с заключением s(R). Покажем, как осуществляется такое преобразование на
примере правила 1. Пусть секвенция R равна Г├φψ и заключительный переход имеет
вид.
;
. Тогда подстановка s преобразует данный заключительный переход к
переходу
)(
)()();()(
Rs
ssss
, где s(R) равно s(Г)├(s()s())
.
В ИС обозначим через (φ ψ) формулу ИС ((φ→ψ ) (ψ→φ)). Напомним, что
11
таблица истинности последней формулы совпадает с таблицей истинности формулы
алгебры логики (φ ψ).
Лемма 1 Секвенция Г├(φψ) доказуема тогда и только тогда, когда
доказуемы секвенции Г,φ├ψ иГ, ψ├ φ.
Доказательство. Предположим, что секвенция Г├ (φψ) доказуема. Тогда
доказуемость секвенции Г, φ ├ψ устанавливается следующим деревом:
2
11,12
,
12
8
,
,
)(
)()(
Доказуемость секвенции Г,ψ├ φ показывается аналогично.
Установим теперь доказуемость секвенции Г├ (φ ψ), предполагая, что
секвенции Г,φ├ψ и Г,ψ├ φ доказуемы:
1
)()(
7
,
7
,
Формулы φ и ψ называются эквивалентными (обозначается φ
ψ), если в ИС
доказуемы секвенции φ ├ ψ и ψ├ φ.
В силу леммы 1.3.2 условие φ
ψ равносильно доказуемости секвенции
├(φ
ψ). Покажем, что отношение образует отношение эквивалентности на
множестве формул.
Лемма 2. Для любых формул φ, ψ и χ исчисления ИС справедливы следующие
утверждения:
(а) φ
φ;
(б) если φ
ψ, то ψ
φ;
(в) если φ
ψ и ψ
χ, то φ
χ.
Доказательство. В пункте (а) доказывать нечего, поскольку φ ├ φ ― аксиома.
Пункт (б) следует из симметричности в определении отношения
. Пункт (в) вытекает
из правила сечения (предложение 1.2.2, в) .
Установим, что эквивалентность формул сохраняется под действием операций
, , и →.
Лемма 3. Если φ
1
ψ
1,
и φ
2
ψ
2
, то
φ
1
ψ
1
, (φ
1
φ
2
)
(ψ
1
ψ
2
), (φ
1
φ
2
)
(ψ
1
ψ
2
) и
12
(φ
1
→φ
2
)
(ψ
1
→ψ
2
).
Доказательство. В силу симметричности отношения достаточно доказать
секвенции
φ
1
├
ψ
1
, (φ
1
φ
2
) ├ (ψ
1
ψ
2
), (φ
1
φ
2
) ├ (ψ
1
ψ
2
) и (φ
1
→φ
2
)├(ψ
1
→ψ
2
), а
доказуемость этих секвенций (на примере с ) устанавливается следующими
деревьями:
6,12
54
2121
2121
212
22
211
11
.
Формула ψ исчисления ИС называется подформулой формулы φ исчисления
ИС, если ψ является подсловом слова φ. Место, которое занимает подформула ψ в
формуле φ, называется вхождением ψ в формулу φ.
Теорема(теорема о замене). Пусть φ — формула исчисления ИС, ψ — ее
подформула, а формула φ' получается из φ заменой некоторого вхождения ψ на
формулу ψ'. Тогда если ψ
ψ', то φ
φ'.
Д о к а з а т е л ь с т в о . Если φ=ψ, то доказывать нечего. Если φ
ψ, то
используем индукцию по числу шагов построения формулы φ. Предполагая, что φ —
пропозициональная переменная, снова получаем φ = ψ. Индукционный переход
осуществляется рассмотрением четырех случаев: φ = φ
1
, φ =φ
1
φ
2
,, φ = φ
1
φ
2
, φ=
φ
1
→φ
2
- В каждом из этих случаев формула ψ входит в φ
1
или φ
2.
Поэтому
эквивалентность φ
φ' вытекает из индукционного предположения и леммы 1.3.3
1.4. Нормальные формы
Покажем, что преобразования формул алгебры логики, приводящие к
построению дизъюнктивных и конъюнктивных нормальных форм, имеют место и в
исчислении секвенций.
Лемма 1. Пусть ψ, φ и χ ― формулы ИС Тогда справедливы следующие
эквивалентности:
(а) (φ
ψ)
χ
φ
(ψ
χ), (φ ψ)
χ φ
(ψ
χ) (ассоциативность и );
(б) φ
ψ
ψ
φ, φ ψ
φ
ψ (коммутативность и );
(в) φ
φ
φ, φ
φ
φ (идемпотентность и );
(г) φ(ψχ)(φψ)(φχ), φ(ψχ)(φψ)(φχ)
(законы дистрибутивности);
13
(д) φ(φψ)φ, φ(φψ)φ (законы поглощения);
(е) (φψ)φψ, (φψ)φψ
(законы де Моргана);
(ж) φφ (закон двойного отрицания);
(з) φ→ψ
φ
ψ
Доказательство. Мы приведем доказательства эквивалентностей φ→ψ├
φ
ψ и
φ
ψ├φ→ψ, оставив остальные утверждения в качестве упражнения:
6
45
,
8
,
;
7
6,12
,
,
,
з
.
Литерой называется любая атомарная формула А, обозначаемая через А
1
,
или ее отрицание
А, которое обозначается через А
0
. Конъюнктом
(дизъюнктом) называется литера или конъюнкция (соответственно дизъюнкция)
литер.
Конъюнкт или дизъюнкция конъюнктов называется дизъюнктивной нормальной
формой (ДНФ), а дизъюнкт или конъюнкция дизъюнктов ― конъюнктивной
нормальной формой (КНФ). Следующая теорема является аналогом теоремы о
приведении формул алгебры логики к дизъюнктивным и конъюнктивным нормальным
формам.
Теорема 1. Любая формула ИС эквивалентна некоторой ДНФ.
2. Любая формула ИС эквивалентна некоторой КНФ.
Алгоритм приведения формулы ИС к ДНФ аналогичен алгоритму приведения
формул алгебры логики к ДНФ и опирается на лемму 1:
1) Выражаем согласно пункту (з) леммы 1.4.1 все импликации, участвующие
в построении формулы, через дизъюнкции и отрицания.
2) Используя законы де Моргана (лемма 1.4.1, п. (е)), переносим все
отрицания к переменным и сокращаем двойные отрицания по закону двойного
отрицания (лемма 1, п. (ж)).
3) Используя закон дистрибутивности φ(ψχ)(φψ)(φχ), преобразуем
14
формулу так, чтобы все конъюнкции выполнялись раньше дизъюнкций.
В результате применения пп. 1-3 получается ДНФ данной формулы.
Приведение формулы к КНФ производится аналогично приведению ее к ДНФ с
применением закона дистрибутивности φ(ψχ)(φψ)(φχ).
1.5. Семантика исчисления секвенций
Пусть X ― некоторое множество, fx ― отображение, которое каждой
пропозициональной переменной ставит в соответствие некоторое подмножество
множества X. Расширим по индукции отображение fx до отображения множества
формул ИС в булеан (т.е. множество всех подмножеств) P(X) множества X согласно
следующим соотношениям:
fx(
φ)=X\ fx(φ),
fx(φ
ψ)= fx(φ)
fx (ψ),
fx (φ
ψ)= fx(φ)
fx(ψ),
fx(φ→ψ)= fx(
φ)
fx(ψ).
Любое такое отображение fx, действующее на множестве формул ИС, называется
интерпретацией ИС в X.
Каждой секвенции S следующим образом ставится в соответствие некоторое
утверждение fx(S) о подмножествах X:
fx(φ
1
,…,φ
n
├ψ)
fx(φ
1
)
…
fx (φ
n
)
fx(ψ),
fx(├ψ)
fx(ψ)=X,
fx(φ
1
,…,φ
n
├)
fx(φ
1
)
…
fx (φ
n
)=
,
fx(├)
Х=
.
Теорема 1. Для любой интерпретации fx ИС и любой доказуемой в ИС секвенции
S справедливо утверждение fx(S).
Доказательство. Если S ― аксиома φ├ φ, то истинность утверждения fx(S),
имеющего вид f
Х
(φ)
f
Х
(φ), очевидна. В общем случае достаточно доказать, что при
переходе по любому из 12-ти правил вывода из справедливости утверждений fx от
секвенций над чертой следует истинность утверждения fx от секвенции под чертой.
Покажем, как проверяются указанные переходы на примере первого правила вывода
;
, где Г=
1
,…,
n
. То есть по условию имеем
n
i
XiX
ff
1
)()(
и
15
n
i
XiX
ff
1
)()(
. Тогда
n
i
XXiX
fff
1
)()()(
. Получаем
n
i
XiX
ff
1
)()(
, т.е. справедливо утверждение
))((
X
f
Проверка остальных переходов аналогична и предоставляется студентам.
Следствие 1. Исчисление ИС непротиворечиво.
Доказательство. Пусть X ― непустое множество, fx ― произвольная
интерпретация ИС, А ― некоторая атомарная формула. Покажем, что формула А
А
не доказуема в ИС. Действительно, f
x
(А А) = fx(A) (X \ fx(A)) = , откуда с учетом
непустоты множества X следует, что утверждение fx(А
А) ложно. Тогда по теореме 1
секвенция ├А
А не доказуема. .
Понятие интерпретации выходит за рамки самого исчисления
и относится к
семантике исчисления, устанавливающей соответствие действий в исчислении с
теоретико-множественными операциями. Сами же понятия формулы, секвенции,
правил вывода и доказательства, образующие исчисление, составляют синтаксис
исчисления.
Определим теперь так называемую главную интерпретацию ИС, которая
позволяет составлять таблицы истинности формул. Возьмем в качестве множества
X одноэлементное множество {}. Тогда для любой атомарной формулы А
значение f
X
(А) равно , т.е. fx(A)= 0, или fx(A) равно {}, т.е. fx(A) = 1
(напомним, что 0 = , а 1 = {}). Придавая переменным x и y значения f
{0}
(x) f
{0}
(y) из множества {0,1}, получаем таблицы истинности для логических операций
,, и (совпадающие с таблицами алгебры логики).
Пусть Α
1
,..., A
k
― пропозициональные переменные, f ― отображение множества
элементарных формул в {0,1}. С помощью таблиц истинности логических связок
функция f однозначно продолжается на множество формул φ(Α
1
,..., A
k
), которые
строятся из пропозициональных переменных Α
1
,..., A
k
и логических связок. При этом
для любой формулы φ, равной
(Α
1
,..., A
k
), значение f(φ) снова равно 0 или 1. Если
f()= 1 (f() = 0), то говорят, что формула φ истинна (ложна) на наборе (f(A
1
),...,f(A
k
)).
Функция f
: {0,l}
k
—> {0,1}, которая каждому набору (δ
1
,…,
k
) {0, l}
k
сопоставляет значение истинности формулы φ, называется истинностной функцией
формулы φ. Очевидно, что таблица истинности функции f
совпадает с таблицей
16
истинности формулы φ.
Напомним, что формула φ называется тождественно истинной
(тождественно ложной), если функция f
тождественно равна единице (тождественно
равна нулю).
Секвенция Г ├
называется истинной на наборе (δ
1
,…,
k
) {0, l}
k
, если на
этом наборе хотя бы одна формула из Г ложна или формула φ истинна. Секвенция Г├
называется истинной на наборе (δ
1
,…,
k
) {0, l}
k
, если на этом наборе некоторая
формула из Г ложна. Секвенция ├ по определению ложна на любом наборе, а
истинность секвенции ├ φ совпадает с истинностью формулы φ.
Секвенция S называется тождественно истинной, если S истинна на любом
наборе (δ
1
,…,
k
) значений истинности переменных A
1
,...,A
k
, среди которых
содержатся все переменные, входящие в формулы из S.
Покажем, что доказуемость секвенции (формулы) равносильна ее
тождественной истинности
Теорема 2. Если секвенция S доказуема в ИС, то S тождественно истинна.
Д о к а з а т е л ь с т в о . Пусть D — дерево доказательства секвенции S.
Применим индукцию по высоте дерева D. Если S — аксиома, то ее тождественная
истинность очевидна. Для завершения доказательства нужно проверить, что
правила вывода 1-12 сохраняют тождественную истинность. Покажем, как
происходит проверка, на примере правила 8, оставив проверку остальных
переходов студентам. Итак, рассмотрим правило
Г
ГГ )(;
и предположим, что на некотором наборе значений истинности пропозициональных
переменных все формулы из Г истинны. Тог да по индукционному предположению на
этом наборе истинны формулы
и
ψ. Следовательно, по определению операции
формула
также истинна.
Для произвольной формулы φ ИС положим
1
= φ,
о
=
. Сформулируем
лемму:
Лемма 1. Пусть φ(Α
1
,...,Α
k
) — формула ИС, построенная из
пропозициональных переменных Α
1
,...,Α
k
, (δ
1
,…,
k
) {0, l}
k
) — набор из {0,tl}
k
. Если
δ — f
((δ
1
,…,
k
), то секвенция
k
k
АА ,...,
1
1
доказуема.
17
Теорема 3. (теорема о полноте).
1. Формула
ИС доказуема в ИС тогда и только тогда, когда φ
тождественно истинна.
2. Секвенция S ИС доказуема в ИС тогда и только тогда, когда S
тождественно истинна.
Доказательство. Тождественная истинность доказуемых секвенций, а также
формул установлена в теореме 1.5.2. Утверждение 2 следует из утверждения 1, так как
доказуемость (тождественная истинность) секвенций
1
,…,
n
├
и
1
,…,
n
├ -
равносильна доказуемости (тождественной истинности) соответствующих формул
1
(
2
…
(
n
)…) и
1
(
2
…
(
n
А
0
А
0
)…).
Пусть φ(Α
1
,...,Α
k
) ― тождественно истинная формула. Индукцией по числу т
докажем, что для любых (δ
1
,…,
k-m
) {0, 1} доказуема секвенция
mk
mk
АА ,...,
1
1
. При
т=0 доказуемость секвенции
k
k
АА ,...,
1
1
вытекает из леммы 1.5.1 и тождественной
истинности формулы φ.
Установим индукционный переход. Предположим, что секвенции
mkmk
AАА
mk
,,...,
1
1
11
и
mkmk
AАА
mk
,,...,
1
1
11
доказуемы. Тогда из доказуемости
секвенции ├А
k-m
А
k-m
по правилу 6 следует доказуемость секвенции
1
1
11
,...,
mk
mk
АА
.
Доказуемость формулы φ вытекает из доказуемости секвенции
mk
mk
АА ,...,
1
1
при m=k.
Таким образом, по теореме о полноте для того чтобы установить, доказуема ли
секвенция
1
,…,
n
├
(или
1
,…,
n
├), достаточно составить таблицу истинности
формулы
1
(
2
…
(
n
)…)( или
1
(
2
…
(
n
А
0
А
0
)…)
)
и проверить ее
тождественную истинность. Как известно, существует единый алгоритм построения
таблиц истинности, и, значит, ИС разрешимо.
Следствие 1.. Тогда и только тогда выполняется ψ
φ, когда равны
истинностные функции f
и f
ψ
.
Из следствия 1.5.6 вытекает, что отношение эквивалентности, введенное в
курсе дискретной математике, и совпадают.
Схема аксиом называется независимой в исчислении, если хотя бы один ее
18
частный случай не доказуем в исчислении без этой схемы. Правило вывода называется
независимым в исчислении, если оно не является допустимым в исчислении,
полученном удалением этого правила.
Исчисление называется независимым, если все его схемы аксиом и правила
вывода независимы.
Теорема 1.5.8. Исчисление ИС независимо.
1.6. Исчисление высказываний гильбертовского типа
Теперь построим исчисление ИВ, в котором в отличие от ИС не используется
понятие секвенции, правило вывода одно, а схем аксиом — несколько.
Формулами ИВ называются формулы ИС.
Аксиомами ИВ являются следующие формулы для любых формул φ,
, χ:
1.
(
)
2. (
)
((
(
))
(
))
3. (
)
4. (
)
5. (
)
((
)
(
(
)))
6.
(
)
7.
(
)
8. (
)
((
)
((
)
))
9. (
)
((
)
)
10.
Указанные формулы называются схемами аксиом ИВ. При подстановке
конкретных формул в какую-либо схему получается частный случай схемы аксиом.
Единственным правилом вывода в ИВ является правило заключения (modus
ponens): если φ и φ
― выводимые формулы, то
― также выводимая формула.
Будем это записывать так:
;
.
Например, если высказывания А
В и А
В
(А
С) выводимы, то
высказывание АС также выводимо согласно правилу заключения.
19
Говорится, что формула φ выводима из формул φ
1
, ..., φ
n
(обозначается φ
1
, ...,
φ
n
├
φ), если существует последовательность формул
1
,...,
n
, φ, в которой любая
формула либо является аксиомой, либо принадлежит списку формул φ
1
, ..., φ
n
,
называемых гипотезами, либо получается из предыдущих по правилу вывода.
Выводимость формулы φ из (├ φ) равносильна тому, что φ ― теорема ИВ.
Пример 1. Покажем, что формула φ φ выводима в ИВ. Для этого построим
вывод данной формулы:
1) в схеме аксиом 2 формулу
заменим на φ φ, χ ― на φ. Получаем
аксиому (φ (()) ((φ ((
φ) )
(
))
2) в схеме аксиом 1 формулу
заменим на φ. Получаем ()
3) из 1 и 2 по правилу modus ponens заключаем ((()))()
4) в схеме аксиом 1 заменяем
на φ
φ. Получаем ((()))
5) из пп. 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. Покажем, что формула
(
(φ
)) доказуема в ИВ для любых
формул φ и
ИВ. По теореме о дедукции достаточно показать φ,
\- φ
. Построим
вывод формулы φ
из гипотез φ и
:
20