Основные правила вывода исчисления высказываний.

4. Правила вывода

1)Правило подстановки: если α – выводимая формула, содержащая букву А(т.е. α (А)), то выводима и формула α (β), получающаяся из α заменой всех вхождений на произвольную формулу β: α (А)/α (β)

2)Правило заключения(Modus Ponens – MP):

Если α и α → β – выводимые формулы, то β тоже выводимая: (α, α → β)/β

Замечание:

В этом описании исчисления высказываний аксиомы явл-ся формулами исчисления, а в правилах вывода исп-ся метаформулы (схемы ф-л)

Схема фор-л α → β обозначает мн-во всех тех формул исчисления кот получаются если ее метапеременные заменить формулами исчисления:

α зам на А, β на А& В, то из α → β получим А→ (А& В).

5. Производные правила вывода в исчислении высказываний: правило введения импликации, теорема дедукции, правило силлогизма, правило введения отрицания.

2. Т. в теории L: А│ ₋ В→ А. Док-во:

1) А – гипотеза по условию.

2) из (1) и аксиомы (Ⅱ.1) по правилу MP получим выводимость В→ А при гипотенузе А.

Полученную выводимость можно вместе с правилом подстановки рассматривать как новое произв. Правило вывода – правило введения импликации: α ⁄ β → α для β.

1.Теорема дедукции: Если Г, α │ ⁻ β, то Г│ ₋ α → β, и наоборот.

2.следствие из т. Дедукции – правило силлогизма: А→ В, В→ С, │ ₋ А→ С(в теории L).

Док-во: построим вывод из этих гипотез:

1) А→ В- гипотеза по условию,

2) В→ С – гипотеза по условию

3) А- гипотеза

4) Из (3) и (1) по правилу МР получим: А, А→ В │ ₋ В

5) Применим МР для (4) и (2): В, В→ С │ ₋ С

6) Из (1), (3) и (5) имеем: А→ В, В→ С, А │ ₋ С

7) Из (6) по теореме дедукции: А→ В, В→ С │ ₋ А→ С.

3. Правило введения отрицания (метод док-ва от противного): Если Г, А│ ₋ В и Г, А│ ₋ , то Г|-

1) по т. Дедукции, если Г, А │ ₋ В и Г, А│ ₋ , то Г│ ₋ А→ В и Г│ → А→

2)из (1) и (Ⅰ.9) двойным применением МП получим Г│ ₋ .