Математическая логика и теория алгоритмов. Стенюшкина В.А. - 22 стр.

UptoLike

ВУЗ: 

ОГУ | Оренбург

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

Рубрика: 

Теорема 5.4 Имеет место выводимость: А
→
(В
→
С), В |−
L
А
→
С.
Доказательство Сначала доказываем выводимость
А
→
(В
→
С), В,А|−
L
С:
1)
A
→
(В
→
С); гипотеза;
2)
А; гипотеза;
3)
В
→
С; МР: 2,1;
4)
В; гипотеза;
5)
С; МР: 4,3.
Вывод для
С построен. Теперь по теореме дедукции заключаем, что
имеет место выводимость
А
→
(В
→
С), В|−
L
А → С. Теорема доказана. Теорема
дает производное правило
Sec
CA
B),CB(A
→
→→
─ правило сечения. 
       Теорема 5.4 Имеет место выводимость: А → (В → С), В |−L А → С.
       Доказательство Сначала доказываем выводимость А→(В→С), В,А|−LС:
       1) A → (В → С); гипотеза;
       2) А; гипотеза;
       3) В→ С; МР: 2,1;
       4) В; гипотеза;
       5) С; МР: 4,3.
       Вывод для С построен. Теперь по теореме дедукции заключаем, что
имеет место выводимость А → (В → С), В|−L А → С. Теорема доказана. Теорема
                          A → ( B → C ), B
дает производное правило                   Sec ─ правило сечения.
                               A→C

Страницы