<< На главную >>
Теорема о дедукции
Будем обозначать буквами [math]\Gamma, \Delta, \Sigma[/math] списки формул (возможно, пустые).
| Определение: |
| Пусть [math]\Gamma[/math] - некоторые список высказываний, [math]\alpha[/math] - некоторое высказывание в исчислении [math]\langle L, A, R \rangle[/math]. Тогда будем говорить, что [math]\alpha[/math] выводится из [math]\Gamma[/math] (запись: [math]\Gamma \vdash \alpha[/math]), если существует доказательство [math]\alpha[/math] в исчислении [math]\langle L, A_1, R \rangle[/math], где [math]A_1[/math] - это [math]A[/math] с добавленными формулами из [math]\Gamma[/math]. Элементы [math]\Gamma[/math] называются допущениями, предположениями, или гипотезами. |
Замечание: в этом определении появляются дополнительные предположения, поэтому речь идет именно о выводе, а не о доказательстве. Очевидно, что, если [math]\Gamma = \varnothing[/math], то [math]\Gamma \vdash \alpha[/math] соответствует [math]\vdash \alpha[/math].
| Теорема (Modus Ponens(M.P.)): |
Пусть справедливо [math]\alpha \rightarrow \beta[/math], так же справедливо [math]\alpha[/math]. Тогда по правилу M.P. справедливо [math]\beta[/math] |
| Теорема: |
Пусть справедливо [math]\Gamma \vdash \alpha \rightarrow \beta[/math]. Тогда справедливо [math]\Gamma \cup \{\alpha\} \vdash \beta[/math] |
| Доказательство: |
| [math]\triangleright[/math] |
|
Возьмем [math]\delta_1, ..., \delta_m[/math] --- вывод формулы [math]\alpha \rightarrow \beta[/math]. В ней [math]\delta_m = \alpha \rightarrow \beta[/math]. Добавим [math]\delta_{m+1} = \alpha[/math] --- это добавленная аксиома, и [math]\delta_{m+2} = \beta[/math], получим вывод [math]\beta[/math] как М.Р. [math]\delta_m[/math] и [math]\delta_{m+1}[/math]. |
| [math]\triangleleft[/math] |
| Лемма: |
[math]\vdash \alpha \rightarrow \alpha[/math] |
| Доказательство: |
| [math]\triangleright[/math] |
- [math]\alpha \rightarrow (\alpha \rightarrow \alpha)[/math] (Сх. акс. 1)
- [math](\alpha \rightarrow (\alpha \rightarrow \alpha)) \rightarrow (\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha)) \rightarrow (\alpha \rightarrow \alpha)[/math] (Сх. акс. 2)
- [math](\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha)) \rightarrow (\alpha \rightarrow \alpha)[/math] (М.Р. 1, 2)
- [math](\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha))[/math] (Сх. акс. 1)
- [math]\alpha \rightarrow \alpha[/math] (М.Р. 4, 3)
|
| [math]\triangleleft[/math] |
