Теорема о дедукции [ править ]
Будем обозначать буквами [math]Gamma, Delta, Sigma[/math] списки формул (возможно, пустые).
| Определение: |
| Пусть [math]Gamma[/math] — некоторый список высказываний, [math]alpha[/math] — некоторое высказывание в исчислении [math]langle L, A, R angle[/math] . Тогда будем говорить, что [math]alpha[/math] выводится из [math]Gamma[/math] (запись: [math]Gamma vdash alpha[/math] ), если существует доказательство [math]alpha[/math] в исчислении [math]langle L, A_1, R angle[/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] .
| Теорема: |
ightarrow eta[/math] . В ней [math]delta_m = alpha
ightarrow eta[/math] . Добавим [math]delta_ = alpha[/math] — это добавленная аксиома, и [math]delta_ = eta[/math] , получим вывод [math]eta[/math] как М.Р. [math]delta_m[/math] и [math]delta_[/math] .
| Лемма: |
| [math]vdash alpha ightarrow alpha[/math] |
| Доказательство: |
| [math] riangleright[/math] |
|
| [math] riangleleft[/math] |
| Теорема (о дедукции): |
Имеется вывод [math]delta_1, . delta_, eta[/math] . Набросаем план вывода, формулы в нем занумеруем через 10 (Ну да, логика же):
[math](10)[/math] [math]Gamma vdash alpha
ightarrow delta_1[/math]
[math](10m — 10)[/math] [math]Gamma vdash alpha
ightarrow delta_[/math]
[math](10m)[/math] [math]Gamma vdash alpha
ightarrow eta[/math]
Дополним план до полноценного вывода. Рассмотрим формулу номер [math]i[/math] . Возможны следующие варианты:
Для того, чтобы оценить ресурс, необходимо авторизоваться.
Математическая логика и теория алгоритмов являются основой курса дискретной математики, что нашло отражение в данном учебном пособии. Учебное пособие адресовано студентам, обучающимся по направлениям 210300 — радиотехника, 230000 — информатика и вычислительная техника, и по специальностям: 210401 — физика и техника оптической связи, 210402 — средства связи с подвижными объектами, 210403 — защищенные системы связи, 210404 — многоканальные телекоммуникационные системы, 210405 — радиосвязь, радиовещание и телевидение, 210406 — сети связи и системы коммутации, и полностью соответствует действующему Государственному образовательному стандарту высшего профессионального образования и требованиям квалификационной характеристики выпускника. Теоретическая часть пособия основана на лекциях, читанных автором в Поволжской государственной академии телекоммуникаций и информатики.
Эта теорема позволяет устанавливать выводимость различных формул гораздо более простым способом, чем непосредственный вывод этих формул.
Формула β выводима из формул α1, α2, . αn, если формулу β можно вывести путем правила заключения, приняв за исходные формулы α1, α2, . αn и все истинные в исчислении высказываний формулы.
1) каждая формула αi(1≤i≤n) выводима из формул α1, α2, . αn;
2) каждая выводимая в исчислении высказываний формула выводима из формул α1, α2, . αn;
3) если формула α и α→β выводима из формул α1, α2, . αn, то формула β также выводима из α1, α2, . αn.
β выводима из α1, α2, . αn будем обозначать α1, α2, . αn├β, если αi нет, то ├β (просто выводимая формула).
Если α1, α2, . αn является аксиомами или другими выводимыми формулами, то класс выводимых формул совпадает с классом всех выводимых в исчислении высказываний формул, так как всякая выводимая формула считается выводимой из любой системы формул.
Если формула β выводима из формул α1, α2, . αn, то α1→(α2→(. (αn→β). )) – выводимая формула.
.
Доказательство этого утверждения проведем по индукции следующим образом. Сначала докажем, что оно верно, если β является одной из формул αi. Затем покажем, что если утверждение верно для формул β′ и β′→β″, то оно верно и для β″.
Итак, если β одна из формул αi, то либо i=n, либо i
Во втором случае αn→αi – выводимая формула:
1. 
— подстановка в аксиому А1;
2. ├αi – по определению;
3. ├αn→αi – по правилу заключения к шагам 1 и 2.
1. 
(A→(B→C))→((A→B)→(A→C))≡(αn→(β′→β″))→((αn→β′)→(αn→β′′));
3. ├ αn→β′′ — по правилу заключения к шагам 1 и 2.
Таким образом мы доказали, что если
Теперь установим справедливость теоремы дедукции. Допустим, что имеет место
В таком случае будем иметь
Применив то же самое вторично, получим
Рассуждая так же и далее, наконец, получим
Применив то же рассуждение еще раз, получим
