Лемма о дедукции, полнота исчисления высказываний — различия между версиями
Proshev (обсуждение | вклад) |
м (rollbackEdits.php mass rollback) |
||
| (не показано 10 промежуточных версий 6 участников) | |||
| Строка 1: | Строка 1: | ||
| + | [[Категория: Математическая логика]] | ||
| + | |||
[[Лекция 2 | <<]][[Лекция 4 | >>]] | [[Лекция 2 | <<]][[Лекция 4 | >>]] | ||
| − | |||
| − | |||
==Теорема о дедукции== | ==Теорема о дедукции== | ||
| Строка 9: | Строка 9: | ||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
| − | Пусть <tex>\Gamma</tex> - | + | Пусть <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>\Gamma = \varnothing</tex>, то <tex>\Gamma \vdash \alpha</tex> соответствует <tex>\vdash \alpha</tex>. | Замечание: в этом определении появляются дополнительные предположения, поэтому речь идет именно о ''выводе'', а не о ''доказательстве''. Очевидно, что, если <tex>\Gamma = \varnothing</tex>, то <tex>\Gamma \vdash \alpha</tex> соответствует <tex>\vdash \alpha</tex>. | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
{{Теорема | {{Теорема | ||
| Строка 39: | Строка 32: | ||
}} | }} | ||
| − | + | ||
| + | {{Теорема | ||
| + | |about= о дедукции | ||
| + | |statement= | ||
| + | Пусть справедливо <tex>\Gamma \cup \{\alpha\} \vdash \beta</tex>. Тогда справедливо <tex>\Gamma \vdash \alpha \rightarrow \beta</tex>. | ||
| + | |proof= | ||
| + | Имеется вывод <tex>\delta_1, ..., \delta_{m-1}, \beta</tex>. Набросаем план вывода, формулы в нем занумеруем через 10 ('''<s>Ну да, логика же</s>'''): | ||
| + | |||
| + | <tex>(10)</tex> <tex>\Gamma \vdash \alpha \rightarrow \delta_1</tex> | ||
| + | |||
| + | ... | ||
| + | |||
| + | <tex>(10m - 10)</tex> <tex>\Gamma \vdash \alpha \rightarrow \delta_{m-1}</tex> | ||
| + | |||
| + | <tex>(10m)</tex> <tex>\Gamma \vdash \alpha \rightarrow \beta</tex> | ||
| + | |||
| + | Дополним план до полноценного вывода. Рассмотрим формулу номер <tex>i</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> и предыдущей) | ||
| + | }} | ||
| + | |||
| + | {{Определение | ||
| + | |definition= | ||
| + | Высказывание <tex>\alpha</tex> следует из высказываний <tex>\Gamma</tex>, если при любой оценке пропозициональных переменных, входящих в высказывания, на которых все высказывания из <tex>\Gamma</tex> истинны, <tex>\alpha</tex> также истинно. Запись: <tex>\Gamma \models \alpha</tex>. | ||
| + | }} | ||
| + | |||
| + | ==Теорема о полноте исчисления высказываний== | ||
| + | |||
| + | {{Лемма | ||
| + | |statement= | ||
| + | Если <tex>\Gamma \vdash \alpha</tex>, то <tex>\Gamma, \gamma \vdash \alpha</tex>. Если <tex>\Gamma_1, \Gamma_2 \vdash \alpha</tex>, то <tex>\Gamma_2, \Gamma_1 \vdash \alpha</tex>. Аналогично для следствия. | ||
| + | |proof= | ||
| + | |||
| + | '''КТО МОЖЕТ НАПИСАТЬ ЭТО ФОРМАЛЬНО?''' | ||
| + | }} | ||
Текущая версия на 19:25, 4 сентября 2022
Теорема о дедукции
Будем обозначать буквами списки формул (возможно, пустые).
| Определение: |
| Пусть - некоторый список высказываний, - некоторое высказывание в исчислении . Тогда будем говорить, что выводится из (запись: ), если существует доказательство в исчислении , где - это с добавленными формулами из . Элементы называются допущениями, предположениями, или гипотезами. |
Замечание: в этом определении появляются дополнительные предположения, поэтому речь идет именно о выводе, а не о доказательстве. Очевидно, что, если , то соответствует .
| Теорема: |
Пусть справедливо . Тогда справедливо |
| Доказательство: |
| Возьмем --- вывод формулы . В ней . Добавим --- это добавленная аксиома, и , получим вывод как М.Р. и . |
| Лемма: |
| Доказательство: |
|
| Теорема (о дедукции): |
Пусть справедливо . Тогда справедливо . |
| Доказательство: |
|
Имеется вывод . Набросаем план вывода, формулы в нем занумеруем через 10 (
...
Дополним план до полноценного вывода. Рассмотрим формулу номер . Возможны следующие варианты:
|
| Определение: |
| Высказывание следует из высказываний , если при любой оценке пропозициональных переменных, входящих в высказывания, на которых все высказывания из истинны, также истинно. Запись: . |
Теорема о полноте исчисления высказываний
| Лемма: |
Если , то . Если , то . Аналогично для следствия. |
| Доказательство: |
| КТО МОЖЕТ НАПИСАТЬ ЭТО ФОРМАЛЬНО? |