![]() |
Главная Случайная страница Контакты | Мы поможем в написании вашей работы! | |
|
Узкое исчисление предикатов непротиворечиво, если ни для какой его формулы недоказуемы одновременно ни она сама, ни ее отрицание.
Построим соответствие h, согласно которому каждой формуле УИП сопоставим некоторую формулу исчисления высказываний следующим образом.
1. Если А - элементарная формула Р(х1,...,хn), то h(А) = Р.
2. Если формулам А и В из УИП сопоставлены формулы h(А) и h(В) в ИВ, то h(ù А) = ù h(А), h(А * В) = h(А) * h(В), где * есть один из знаков: &, V, ®.
3. Если формуле А(х) сопоставлена формула h(А), то h(($х)А(х)) = h(А); h(("х)А(х)) = h(А), т.е. кванторы вместе с их переменными стираются.
Если А - формула в УИП, то h(А) получается из А стиранием в А всех кванторов и всех предметных переменных.
Лемма. Если формула А доказуема в УИП, то формула h(А) доказуема в ИВ.
Доказательство. Индукция по длине k доказательства.
БАЗИС. k = 1. Возможны следующие случаи.
1. ├ С в УИП, причем формула С - аксиома, полученная по одной из схем аксиом А1-А11. Тогда h(С) есть формула в ИВ, построенная по той же схеме аксиом.
2. ├ С, причем С есть ("x)A(x) ® А(у) - аксиома Бернайса. Тогда h(С) = h(("х)А(х) ® А(y)) = h(А) ® h(А). Поэтому h(С) доказуема в ИВ. Если С есть А(у) ® ($х)А(х) - вторая аксиома Бернайса, то доказуемость А(С) в ИВ следует из тех же соображений.
ПРЕДПОЛОЖЕНИЕ ИНДУКЦИИ. Допустим, что лемма справедлива для всех доказуемых в УИП формул с длиной доказательства меньше k.
ШАГ ИНДУКЦИИ. Покажем, что лемма справедлива для всех доказуемых в УИП формул с длиной доказательства k. Пусть ├ А в УИП и A1,A2,…,Ak (=А) есть доказательство формулы А в УИП длины k. Возможны следующие случаи.
1. А - аксиома. Тогда это рассмотренный выше случай базиса.
2. ├ А в УИП и А1,А2,…,Аi,...,Аi ® Ak,...,Ak(=A) есть доказательство форму-лы А в УИП длины k, причем Аk получено из Аi и Аi ® Аk по правилу заключения. Так как длины доказательств A1,A2,...,Аi и A1,A2,…,Ai,…,Ai ®Ak формул Аi и Аi ® Аk меньше k, то по предположению индукции
(1) ├ h(Аi) в ИВ; (2) ├ h(Аi ® Аk) в ИВ.
Так как h(Аi ® Аk) = h(Аi) ® h(Аk), то
(3) ├ h(Аi) ® h(Ak)в ИВ; (4) h(Аk), П3(1,3).
3. ├ А в УИП и А1,А2,...,Аi,...,Аk (=А) есть доказательство формулы А в УИП длины k, причем формула Аk, равная С ® ("x)B(x) получена из формулы
Аi = С ® В(х) с помощью "-правила. Так как длина доказательства A1,A2,…,Ai формулы Аi меньше k, то по предположению индукции ├ h(Аi). Так как h(Аi) = h(С ® В(х)) = h(С ® ("x)B(x)) = h(Аk), то ├ h(Ak) в ИВ.
4. ├ А в УИП и А1,А2,...,Аi,...,Аk (=А) есть доказательство формулы А в УИП длины k, причем формула Аk, равная ($х)В(х) ® С получена из формулы
Аi = В(х) ® С с помощью $-правила. Далее аналогично предыдущему случаю.
Теорема. УИП непротиворечиво.
Доказательство. Если ├ А и ├ ù А в УИП, то ├ h(А) и ├ ù h(А) в ИВ. Проти-воречие с непротиворечивостью ИВ.
Дата публикования: 2015-01-23; Прочитано: 211 | Нарушение авторского права страницы | Мы поможем в написании вашей работы!