yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Математика і інформатика->Содержание->3. 5. Правила введения я удаления связок.

Математическая логика

3. 5. Правила введения я удаления связок.

При доказательстве теорем и построении выводов можно использовать производные правила вывода, доказанные ранее, в том числе правила введения и удаления связок.

Связка

Введение

Удаления

Г,А|—ВГ|—АВ(МТД)

А,АВ|—В(МР)

Г1|—А, Г2|—АВГ12|—В

¬

 

Г,А|—В; Г,А|—¬ВГ|—¬А

(док-во от противного)

¬¬А|—А(удаление двойного отрицания)

А, ¬А|—В(слабое удаление отрицания)

&

 

Г1, Г2|—А&В

Г|— А&В Г |—А

Г|— А&В Г |—В

Г |—А Г |—AvB

 Г123 |—С

А В,В А |—АВ

АВ|—АВ, АВ|—ВС

 

В|—В-»А

п

Г2 Т7

Т7

МР(1,3)

МР(2,4)

Т9

МР(5,7)

МР(6,8)

=*-<А-4-В)(— А

Т5

Докажем некоторые из этих правил. В4. ¬ - введение

1.   АВ                                                                           Г1

2.    А¬В                                                                       Г2

3.   (АВ)  (¬В¬А)                                               Т7

4.   (А¬В)  (¬¬В¬А)                                           Т7

5. ¬В¬А                                                                        МР(1,3)

6. ¬¬В¬А                                                                      МР(2,4)

7.( ¬В¬А) ((¬¬В¬А) ¬А)                              Т9

8.( ¬¬В¬А) ¬А                                                        МР(5,7)

9. ¬А                                                                                  МР(6,8)

В5. & - удаление1

1. АВ                                                                             Г1

25

2.(А¬В)  ¬ ¬ (А¬В)                                            Т4

3.  (¬А¬¬(А¬В)) (¬(А¬В) А)                  Сл.1(1,2)

4.( ¬А¬¬(А¬В)) (¬(А¬В) А)                   Т6

5. ¬(А¬В) А                                                             МР(3,4)                                  

В6. & - удаление2             А&В|—В¬(А¬В) |—В|—¬(А¬В) В

В7. & - введение А,В|—А&В А,В|—¬(А¬В)

 

 

 

21