Главная страница Случайная страница
КАТЕГОРИИ:
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника
Непрямые правила.
|
|
За правилами сохраняются обозначения, данные при формулировке натурального исчисления высказываний. То есть правила первого вида позволяют из одних выражений выводить новые, а правила второго вида регламентируют выведение из утверждений о логическом следовании новых утверждений о логическом следовании.
Прямые правила вывода в S6:
А, В_ (ВК); А & В (УК, 1); А & В (УК, 2);
А & В А В
Ø 
(А & В) (ОК ); А___ (ВД, 1); В _ (ВД, 2);
Ø А Ú Ø В А Ú В А Ú В
А Ú В, Ø А (УД, 1); А Ú В, Ø В (УД, 2); Ø (А Ú В) (ОД);
В А Ø А & Ø B
А É В, А (УИ, 1 ); А É В, Ø В (УИ, 2); Ø (А É В) (ОИ);
В Ø А А & Ø В
А É В, В É А (ВЕ); Аº В (УЕ, 1); А º В ( УЕ, 2 );
А º В А É В В É А
__А__ (ВО); Ø Ø А_ (УО) ;
Ø Ø А А
Ø " х А(х) (О"); Ø \x А(х) (О$) ;
$х Ø А(х) " х Ø А(х)
G |- A(x) __, G не содержит x свободно (В");
G |- [x А(x)
G, A(x) |- C__, G, \y A(y), A(x) |- C__, G, C не содержат x свободно (У\);
G, \x А(x) |- C G, |- C
[x А(x), t свободнодля x в А(x) (У" );
А (x / t)
А (x / t), t свободнодля x в А(x) (В$).
$ x A(x)
Непрямые правила вывода в S6:
а) правило введения импликации (ВИ):
G, A |- B_
G |- А É В
б) правило введения отрицания, или правило опровержения «путем сведения к абсурду» (ВО) или (Св.А):
G, А |- В, Ø В
G |- Ø А
в) правило доказательства «от противного» (ДОП):
G, Ø А |- В, Ø В
G |- A
На применение правила (ВИ) накладывается следующее ограничение: все свободные переменные гипотез должны быть фиксированными, то есть к ним в процессе дедукции не применяются по этим переменным ни правило (В[), ни правило (В\). Понятие вывода такое же, как для натурального исчисления высказываний[28], но разумеется, добавляются соответствующие правила вывода для кванторов с теми ограничениями на их использование, которые были оговорены.
Рассмотрим, для примера, несколько доказательств в S6.
Метатеорема: если G |- A(x) É B(x), то |- [x A(x) É [x B(x)
Доказательство.
1) G |- A(x) É B(x) допущение, G не содержит x свободно
2) G, A(x)|- B(x) 1), MP
3) G, [x A(x) |- B(x) 2), (У[), транзитивность |-
4) G, [x A(x) |- [xB(x) 3), (В[)
5) G |- [x A(x) É [x B(x) 4), (ВИ).
Метатеорема: $х " у Р(х, у) |- " у $х Р(х, у)
1) $х " у Р(х, у) допущение
2) " у Р(z, у) 1), (У$)
3) Р(z, w) 2), (У")
4) $x Р(x, w) 3), (В$)
5) " у $х Р(х, у) 4), (В"), п/п к w/y.
Данные примеры иллюстрируют специфику натурального исчисления предикатов в сравнении с его аксиоматической формулировкой.
Контрольные вопросы и упражнения.
1. Общая характеристика исчислений логики предикатов.
2. Понятие аксиоматического исчисления логики предикатов.
3. Структура аксиоматического исчисления логики предикатов S5.
4. Характеристика списка аксиом S5..
5. Общая характеристика правил вывода в S5..
6. Понятие правильной подстановки.
7. Правило удаления квантора общности.
8. Правило введения квантора общности
9. Правило введения квантора существования.
10. Правило удаления кантоа существования.
11. Правило переименования свободных переменных.
12. Правило переименования связанных переменных.
13. Характеристика определения доказательства.
14. Определение доказуемой формулы.
15. Определение вывода.
16. Теория дедукции.
17. Доказательство теоремы о дедукции.
18. Общая характеристика металогических принципов в S5.
19. Принцип непротиворечивости аксиом.
20. Принцип независимости аксиом.
21. Принцип полноты.
22. Общая характеристика натурального исчисления предикатов S6.
23. Типология правил вывода в S6.
24. Характеристика кванторных правил в S6.
25. Определение вывода в S6.
26. Определение доказательства в S6..
27. Процедура построения выводов и доказательств в S6.
28. Построить выводы в S6:
a) " x (A(x) & B(x)) |- " x A(x) & " x B(x)
б) $x (S(x) É P(x)) |- " x (S(x) É $x P(x))
в) " x (M(x) É P(x)); " x (S(x) É M(x)) |- " x (S(x) É P(x))
г) " x (M(x) É Ø P(x)), (S(x) É M(x)) |- " x (S(x) É Ø P(x))