Элементы математической логики. Фролов И.С. - 69 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

выполняется следующее структурное условие: если формула ∀xA по-
лучена из формулы A по правилу обобщения, то переменная x не яв-
ляется свободной в гипотезах, предшествующих формуле ∀xA в этой
последовательности.
Выводимость и доказуемость в исчислении предикатов определя-
ется так же, как и в исчислении высказываний.
Пример 1. Построим доказательство формулы ∀xA(x) ⇒
⇒ ∀yA(y):
1. ∀xA(x) ⇒ A(y) (аксиома Q1).
2. ∀y(∀xA(x) ⇒ A(y)) (Gen, 1).
3. ∀y(∀xA(x) ⇒ A(y)) ⇒ (∀xA(x) ⇒ ∀yA(y)) (аксиома Q3).
4. ∀xA(x) ⇒ ∀yA(y) (MP, 2, 3).
Здесь структурное условие выполнено, так как правило обобщения при-
меняется на шаге 2, а перед ним стоит только аксиома (гипотез нет
вообще).
Так же, как в исчислении высказываний, выводы даже простых
формул получаются очень громоздкими. Поэтому практически для по-
строения доказательств пользуются производными правилами вывода,
среди которых ключевую роль играет теорема дедукции.
Теорема 1. Если Γ, A ` B, то Γ ` A ⇒ B.
В доказательстве разберем только случай применения правила
обобщения, так как все остальное дословно повторяет доказательство
аналогичной теоремы исчисления высказываний (теорема 4 § 5).
Пусть формула B
i
получена из формулы B
j
(j < i) по прави-
лу обобщения, и, таким образом, имеет вид ∀xB
j
. Без ограничения
общности можно предполагать, что формула B
i
в выводе непосред-
ственно следует за B
j
, т.е. i = j + 1. Предположим, что имеется вывод
Γ ` A ⇒ B
j
и построим вывод Γ ` A ⇒ ∀xB
j
.
Если в последовательности формул B
1
, . . . , B
j
встречается A, то
в силу структурного условия переменная x не является свободной в
A. Тогда допустима аксиома Q3: ∀x(A ⇒ B
j
) ⇒ (A ⇒ ∀xB
j
) и воз-
можно применение правила обобщения к формуле A ⇒ B
j
, что дает
∀x(A ⇒ B
j
) и, после применения правила MP, A ⇒ ∀xB
j
.
Если среди формул B
1
, . . . , B
j
нет A, то вывод формулы B
j
и сле-
дующей за ней формулы ∀xB
j
не зависит от A, т.е. существует вывод
формулы ∀xB
j
только из гипотез Γ. Остается воспользоваться аксио-
мой 1 в виде ∀xB
j
⇒ (A ⇒ ∀ xB
j
) и правилом MP, чтобы вновь полу-
чить A ⇒ ∀xB
j
.
68

Страницы