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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

/ Очевидно, что вторая часть теоремы вытекает из первой в силу
возможности применить допустимые правила вывода 5) и 6).
I. Пусть Γ ` A в ИВ. Докажем, что секвенция Γ ` A доказуема в
ИС, используя индукцию по длине вывода в ИВ.
Пусть вывод в ИВ состоит из единственной формулы A. Тогда
A — аксиома или гипотеза. В первом случае, согласно лемме 2 и до-
пустимому правилу 1), доказуемы секвенции ` A и Γ ` A. Во втором
случае применение того же допустимого правила к аксиоме ИС A ` A
доказывает секвенцию Γ ` A.
Рассмотрим теперь вывод в ИВ B
1
, . . . , B
n
(= A), имеющий произ-
вольную длину n > 1. Тогда формула A должна получаться по правилу
отделения из B
j
, B
k
, (j, k < n), причем по предположению индукции
секвенции Γ ` B
j
и Γ ` B
k
доказуемы, так как вывод каждой из фор-
мул B
j
, B
k
имеет длину, меньшую n . Формула B
k
должна иметь вид
B
j
⇒ A, и секвенция выводится по правилу удаления ⇒.
II. Пусть секвенция Γ ` A доказуема в ИС. Докажем, что суще-
ствует вывод формулы A из Γ в ИВ.
В силу свойств выводимости в ИВ (теорема 2 § 5, рефлексивность
и транзитивность), достаточно показать, что все правила вывода ИС
сохраняют выводимость в ИВ (при этом секвенцию Γ ` будем заменять
на Γ ` P ∧ ¬P ).
Сохранение выводимости для правил введения и удаления ∧, ∨ и
⇒ можно доказать, используя одноименные правила ИВ (теорема 2 § 6)
и транзитивность отношения выводимости в ИВ. Сохранение выводи-
мости для правила утончения имеет место в силу свойства утончения
(теорема 2(2) § 5).
Докажем сохранение выводимости правилом удаления противо-
речия, т.е. докажем в ИВ производное правило вывода
Γ, ¬A ` P ∧ ¬P
Γ ` A
:
1. Γ, ¬A ` P ∧ ¬P (исходная посылка).
2. Γ, ¬A ` P и Γ, ¬A ` ¬P (удаление ∧).
3. Γ ` ¬¬A (приведение к абсурду).
4. Γ ` A (удаление ¬¬).
Рассмотрим правило введения противоречия. Оно соответствует
производному правилу ИВ
Γ ` A; Γ ` ¬ A
Γ ` P ∧ ¬P
,
56

Страницы