1632
правки
Изменения
м
rollbackEdits.php mass rollback
{{Определение
|definition=
Пусть <tex>\Gamma</tex> - некоторые некоторый список высказываний, <tex>\alpha</tex> - некоторое высказывание в исчислении <tex>\langle L, A, R \rangle</tex>. Тогда будем говорить, что <tex>\alpha</tex> '''выводится''' из <tex>\Gamma</tex> (запись: <tex>\Gamma \vdash \alpha</tex>), если существует доказательство <tex>\alpha</tex> в исчислении <tex>\langle L, A_1, R \rangle</tex>, где <tex>A_1</tex> - это <tex>A</tex> с добавленными формулами из <tex>\Gamma</tex>. Элементы <tex>\Gamma</tex> называются допущениями, предположениями, или гипотезами.
}}
# <tex>\delta_i</tex> --- аксиома или предположение, входящее в <tex>\Gamma</tex>. Тогда вставим перед этой формулой <tex>\delta_i</tex> и <tex>\delta_i \rightarrow (\alpha \rightarrow \delta_i)</tex>, формула верна по M.P.
# <tex>\delta_i = \alpha</tex>. Тогда вставляем перед формулой 4 формулы из леммы.
# <tex>\delta_i</tex> выводится по M.P. из <tex>\delta_j</tex> и <tex>\delta_k</tex>, где <tex>j, k < i</tex>. Выведем <tex>\alpha \rightarrow \delta_i</tex>, добавив <tex>(\alpha \rightarrow \delta_j) \rightarrow ((\alpha \rightarrow (\delta_j \rightarrow \delta_i)) \rightarrow (\alpha \rightarrow \delta_i))</tex> (сх. акс. 2) и <tex>((\alpha \rightarrow (\delta_j \rightarrow \delta_i)) \rightarrow (\alpha \rightarrow \delta_i))</tex> (M.P. из <tex>j</tex> и предыдущей)
}}
