Лемма о дедукции, полнота исчисления высказываний — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
(не показано 8 промежуточных версий 5 участников)
Строка 9: Строка 9:
 
{{Определение  
 
{{Определение  
 
|definition=
 
|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>\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>.
 
{{Теорема
 
|author=
 
Modus Ponens(M.P.)
 
|statement=
 
Пусть справедливо <tex>\alpha \rightarrow \beta</tex>, так же справедливо <tex>\alpha</tex>. Тогда по правилу M.P. справедливо <tex>\beta</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

<< >>

Теорема о дедукции

Будем обозначать буквами [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].

Теорема:
Пусть справедливо [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]
  1. [math]\alpha \rightarrow (\alpha \rightarrow \alpha)[/math] (Сх. акс. 1)
  2. [math](\alpha \rightarrow (\alpha \rightarrow \alpha)) \rightarrow (\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha)) \rightarrow (\alpha \rightarrow \alpha)[/math] (Сх. акс. 2)
  3. [math](\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha)) \rightarrow (\alpha \rightarrow \alpha)[/math] (М.Р. 1, 2)
  4. [math](\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha))[/math] (Сх. акс. 1)
  5. [math]\alpha \rightarrow \alpha[/math] (М.Р. 4, 3)
[math]\triangleleft[/math]


Теорема (о дедукции):
Пусть справедливо [math]\Gamma \cup \{\alpha\} \vdash \beta[/math]. Тогда справедливо [math]\Gamma \vdash \alpha \rightarrow \beta[/math].
Доказательство:
[math]\triangleright[/math]

Имеется вывод [math]\delta_1, ..., \delta_{m-1}, \beta[/math]. Набросаем план вывода, формулы в нем занумеруем через 10 (Ну да, логика же):

[math](10)[/math] [math]\Gamma \vdash \alpha \rightarrow \delta_1[/math]

...

[math](10m - 10)[/math] [math]\Gamma \vdash \alpha \rightarrow \delta_{m-1}[/math]

[math](10m)[/math] [math]\Gamma \vdash \alpha \rightarrow \beta[/math]

Дополним план до полноценного вывода. Рассмотрим формулу номер [math]i[/math]. Возможны следующие варианты:

  1. [math]\delta_i[/math] --- аксиома или предположение, входящее в [math]\Gamma[/math]. Тогда вставим перед этой формулой [math]\delta_i[/math] и [math]\delta_i \rightarrow (\alpha \rightarrow \delta_i)[/math], формула верна по M.P.
  2. [math]\delta_i = \alpha[/math]. Тогда вставляем перед формулой 4 формулы из леммы.
  3. [math]\delta_i[/math] выводится по M.P. из [math]\delta_j[/math] и [math]\delta_k[/math], где [math]j, k \lt i[/math]. Выведем [math]\alpha \rightarrow \delta_i[/math], добавив [math](\alpha \rightarrow \delta_j) \rightarrow ((\alpha \rightarrow (\delta_j \rightarrow \delta_i)) \rightarrow (\alpha \rightarrow \delta_i))[/math] (сх. акс. 2) и [math](\alpha \rightarrow (\delta_j \rightarrow \delta_i)) \rightarrow (\alpha \rightarrow \delta_i)[/math] (M.P. из [math]j[/math] и предыдущей)
[math]\triangleleft[/math]


Определение:
Высказывание [math]\alpha[/math] следует из высказываний [math]\Gamma[/math], если при любой оценке пропозициональных переменных, входящих в высказывания, на которых все высказывания из [math]\Gamma[/math] истинны, [math]\alpha[/math] также истинно. Запись: [math]\Gamma \models \alpha[/math].


Теорема о полноте исчисления высказываний

Лемма:
Если [math]\Gamma \vdash \alpha[/math], то [math]\Gamma, \gamma \vdash \alpha[/math]. Если [math]\Gamma_1, \Gamma_2 \vdash \alpha[/math], то [math]\Gamma_2, \Gamma_1 \vdash \alpha[/math]. Аналогично для следствия.
Доказательство:
[math]\triangleright[/math]
КТО МОЖЕТ НАПИСАТЬ ЭТО ФОРМАЛЬНО?
[math]\triangleleft[/math]