Теорема дедукции
(10) Следствие 1: если , то
и обратно
Доказательство:
Г:=0
Следствие 2: правило «транзитивности»
Доказательство:
1) A→B гипотеза.
2) B→C гипотеза
3) А гипотеза
4) A→B, B→C, A├С по теореме дедукции получаем
–
Следовательно, вывод верен.
5) Теорема Дедукции
Этот вывод эквивалентен новому производному правилу – правилу транзитивности
Следствие 3: правило «сечения»
Доказательство:
1) — гипотеза.
2) B – гипотеза
3) A – гипотеза
4)
5)
6) Вывод 1, 2, 3, 4, 5 верен иначе говоря:
Правило сечения!
(11) Теорема: В теории L выводимы следующие формулы
a.
b.
c.
d.
e.
f.
g.
ТеоремаА:
ТеоремаБ:
Теорема В:
(12) Множество теорем ИВ: доказательство леммы
Используя способ по индукции по структуре формулы
(1) А = аi, A` = a`
a`├ a` по дедукции ├ a`→ a` будет верна, так как она совпадает с теоремой или ├ А`→ А`
Теорема 1 то есть по обратной дедукции верно А`├ А` или a`├ a` добавление лишних гипотез не влияет на истинность теоремы
(2) А = ┐B т. е. по индукц. Предположению лемма верна для формулы В
Если I(B) = И тогда В`= B, I(A) = Л
А`= ┐A = ┐B на основании теоремы о добавлении двойного отрицания
├ В→┐┐В, по МР
то
I(B) = Л, В`= ┐B, I(A) = И, А`=А=┐B=B`
т. е. А`=B`
(3) А=В→С т. е. по инд. Предположению верны выводы
а)I(В) = Л тогда при любом значении I(С) имеем что I(A) = И т. е. А`=А=В→С
┐А→(А→В) {B//A, C//B}, ┐B→(B→C)=A по МР
Данный а) эквивалентен подпунктам I(С) = И и I(С) = Л
б) I(В) = И, I(С) = И тогда I(A) = И, т. е. А`=А=В→С, С`=C, B`=B
А1 {C//A} C→(B→C)=A=A`
в) I(В) = И, I(С) = Л, I(А) = Л, т. е.
С`=┐C, B`=B
Используя теорему подстановки вместо {B//A, C//B}
(13) Множество теорем ИВ (А — тавтология)
В теоремах теории L выводимыми формулами являются общ. формулами (тавтологией) и только они
1) Обратная Дано А – тавтология, Доказать
Доказательств: используя лемму
Аi` = {ai, I(ai) = И; ┐ai, I(ai) = Л}
Используя теорему дедукции
Используя теорему
и МР два раза получим
Аналогичным образом проделываем вышеописанную процедуру n-1 раз и в результате получим
3) Прямая теорема
Дано
Доказать что А – тавтология
А1,А2,А3 – аксиомы – тавтологии ()
Правило вывода из тавтологий А1-А3 МР сохраняет свойство тавтологичности, поэтому результирующие формулы в теоремах также будут тавтологиями.
Приведённая метатеорема указывает на свойство полноты теории L(ИВ).
Следствие из метатеоремы
Теория L формально непротиворечива
Доказательство:
Для формально непротиворечивой теории не могут быть верны теоремы и
(одновременно), так как на основании метатеоремы мы заключили что выводимой формулой является лишь тавтология, но непротиворечивая, поэтому не могут быть выводимы одновременно тавтология и противоречие, значит теория формально непротиворечива.
(14) Опр1: Исчисление предикатов (ИП) 1-ого порядка – это формальная теория К, в которой определены следующие компоненты:
1) Алфавит:
a. Логические связки (основные) ┐, →, (дополнительные) &, v
b. Служебные скобки (,).
c. Кванторы
2)
a. Предметные константы a, b, c
b. Предметные переменные x, y, z : x1, y1, z1 …
c. Предметные предикаты P, Q, R
d. Предметные функторы f, p, g
X2+X2=R2 – функтор
<, ≤, >, ≥, =, ≠ — предикаты
Опр2: Вхождение переменных в атомарные формулы A и B называется свободным, если они не связаны квантором. Это вхождение будет также свободным и в формулах ┐А, ┐B, A→B, и наоборот связанным если их объединяют кванторы.
Опр3: Формулы А и ┐А, где А – атомарная формула, называются контрарными литералами.
Опр4: Терм t(…x…) для переменной x, в формуле A(…x…t(x)…), называется свободным, если никакое свободное вхождение переменной x в формуле A не лежит в области действий по переменной y входящей в терм t.
Опр5: ИП – не содержащее предметных констант, функторов, предикатов, собственных (не логических) аксиом предметной области – называется ЧИСТЫМ (узким) ИП, в противном случае ПРИКЛАДНЫМ.
(15) Интерпретация ИП
В I(Приклад ИП) с областью интерпретации (носитель М) – это набор функций которые сопоставляют:
а) в каждой предметной константе а элемент носителя I(a) принадлежит М
б) каждому функтору f сопоставляет операцию I(f) на носителе
в) Каждому n-местному предикату Р сопоставляется отношения I(P), I(P) М
Свойство
1) Пусть х=(х1,х2,…,хn)
S=(s1,s2,…,sn)
T=(t1,t2,…,tn)
f(t1,t2,…,tn)
S из носителя M:
S*:{t} → M
a) S*(a) = I(a)
б) S*(xi)=Si
S*(f(t1,t2,…,tn))=I(f)(S*(t1),S*(t2),…,S*(tn))
S*(P) = I(P)= (S*(t1),S*(t2),…,S*(tn))
Всегда определ. истинностное значение для любой формулы для любого атом. формулы носителя
3) Если истинностное значение S*(P)=И, то формула P выполнима на наборе S
4) Формула ┐А выполнима на наборе S титтк формула А невыполнима на этом наборе S
5) A→B(Формула) выполнима на наборе S титтк формула А невыполнима на S или формула В выполнима на S
6) Формула выполнима на S титтк А выполнима на любом наборе S` отличающемся от набора S возможно только лишь i-ым компонентом
7) S` выполнима на S титтк A выполнима на каком либо наборе S` отличным от S возможно только лишь i-ым компонентом
8) Формула называется истин. На любой интерпретации I если она выполнима на любом наборе S из носителя M
9) Формула ложна в данной интерпретации I если она не выполнима на любом наборе S из носителя М
10) Интерпретация называется моделью множества Г если все формулы из Г истинны в данной интерпретации
11) Любая замкнутая формула истинна или ложна в данной интерпретации
Открытая(незамкнутая) формула А(x, y,z…) титтк её замыкание истинно в данной интерпретации
Вывод собствен. нелогич. аксиомы прикладной теории пишутся в открытой форме
(16) Опр1: Формула ИП общезначима (тавтология) если она истинна в любой интерпретации
Т11: Формула , где терм t свободен для переменной x формулы A, является тавтологией.
Т12: Формула , где терм t свободен для переменной x формулы A, является тавтологией.
Т1:Любая теорема ЧИП 1ого порядка в качестве выводимой формулы содержит общезначимую формулу
Т2: Любая общезначимая формула является выводимой формулой ПИП 1-ого порядка.
Свойство формальной непротиворечивости для ЧИП также выполняется
(17) Опр1: Формула B выполнимая на любом наборе в любой интерпретации, на которой выполнима формула A, называется логическим следствием форм. A.
Опр2: Формулы A и B логически эквивалентны AóB или A=B, если если они являются логическим следствием друг друга.
Следствия эквивалентности:
1)
2)
3)
4)
5)
6)
7)
8)
9) Для любой формулы A существует логически эквивалентная ей формула A’ в предваренной форме.
(18) Опр1: Теория равенства ε – это ПИП в котором кроме ЧИП дополнительно введены:
1) Собственный 2-х местный предикат «=» (x=y)
2) Собственные аксиомы:
a. E1:
b. E2:
Т 1, 2, 3:
1) , для любого терма (t)
(частный случай эквивалентности. Рефлексивность)
2)-симметричность
3) — транзитивность
Доказательство:
1)
Из P1 и E1 => => {x=x| |A(x)} =>t=t
2)
E2:{x=x|| A(x)}: (x=y)→((x=x)→(y=x))
2разадедукция назад:
E1 или теорема первая:
Применяем дедукцию вперед и получаем результат:
3)
E2:{x=z || A(x), y || x, x || y, x=z || A(x)}
(y=x)→((y=z)→(x=z)) – тавтология
Дедукция назад
по второй теореме:
Дедукция вперед и готов результат:
Предикат равенства (отношение равенства) на основе теорем 1, 2, 3 – обладает свойствами рефлексивности, симметричности, транзитивности, значит отношение равенства является отношением эквивалентности, но оно является его частным случаем, и является более сильным отношением эквивалентности чем другие. Элементы понимаются как абсолютно совпадающие.
(19) Опр1: Формальная арифметика – это ПИП в котором имеются:
1) предметные константы – 0
2) Двуместные функторы +,*
3) Одноместные функторы P,” ’ ”
4) Двуместный предикат «=»
5) Собственные (нелогические) Аксиомы:
A1:
A2: (t1’=t2’)→(t1=t2)
A3: ┐(t’=0)
A4: (t1=t2)→((t1=t3)→(t2=t3))
A5: (t1=t2)→(t1’=t2’)
A6: t+0=t
A7: t1+t2’=(t1+t2)’
A8: t*0=0
A9: t1*t2’=t1*t2+t1
Чтобы из этой формальной арифметики A получить обычную арифметику, надо одноместный функтор «’» интерпретировать как взятие следующего за текущим элементом t.
(20) Опр1: Группа G – это ПИП с равенством (теория равенств учтена) в которой имеется:
1) Предметная константа = «0»
2) Двуместный функтор «+»
3) Собственные (не логические) аксиомы:
G1: — ассоциативность
G2:
G3:
Замечание: В теорию G входит теория равенства со всеми аксиомами, и все следствия из этой теории.
G4:
Замечание: Если выполняется Аксиома G4, то такая группа называется Абелевой.
Опр2: Абелева группа называется группой конечного порядка n, если выполняется аксиома G5:
G5:
Опр3: Абелева группа называется полной, если выполняется G6
G6:
Опр4: Абелева группа называется периодической, если выполняется G7:
G7: Число k – должно существовать
Метатеорема 1: Во всякой достаточно богатой теории 1-ого порядка существует такая истинная формула f, что ни F и ни ┐F не являются выводами в этой теории.
Метатеорема 2: Во всякой достаточно богатой теории 1-ого порядка формула F, утверждающая непротиворечивость этой теории, не является выводимой в ней.
Интерпретация — пояснение – теорем Геделя не утверждает, что арифметика противоречива, а утверждает, что непротиворечивость собственными формулами теория установить не может.
(21) Постановка задачи:
Алгоритм АДТ в общем случае для любой теории Г, для любой формулы S в ней, не существует, т. е. алгоритм АДТ должен отвечать «Да», если вывод справедлив, и «нет» если такой вывод неверен.
В частности для теории L (ИВ), и для ПИП 1-ого порядка с одноместным предикатом алгоритмы АДТ известны:
А) (ИВ) – метод таблиц истинности (но не является методом автоматического поиска верных выводов)
Б) Для ПИП – таким методом может служить например метода «резолюций»
Этот метод MR выдает для ПИП 1-ого порядка ответ «Да», если вывод верен и выдает «нет» или зацикливается, если вывод неверен.
Доказательство от противного:
Т1: Если вывод — противоречие, то верен вывод
Доказательство:
1) по теореме Дедукции =>
— тавтология
— Обратная Дедукция и получаем:
(22)Опр1:Предложение – бескванторная дизъюнкция литералов (переменных).
Любая формула ИП преобразуется во множество предикат с помощью следующих операции:
1. Элиминация импликации
2. Протаскивание отрицаний:
3. Разделение связанных переменных:
4. Приведение к предваренной форме (изнутри вытаскиваются все кванторы):
5. Элиминация квантора :
6. Элиминация квантора :
7. Приведение формы к КНФ:
8. Элиминация конъюнкции (распад на отдельные предложения): A&B, A, B
В результате применения таких операций из 1-8 (в частном случае могут быть применены все 8 операций, и может быть не 1 раз), любая формула преобразуется во множество предложений.
Т1: Если Г – множество предложений полученных из формулы S, то S – является противоречием тогда и только тогда, когда множество Г – невыполнимо, т. е. Г не имеет модели.
Доказательство:
Для доказательства необходимо сначала доказать все 8 операций в отдельности, ранее доказанными теоремами и отдельные операции из 8-и операций имеют тривиальные доказательства, кроме сколемизации квантора существования (элиминации)
Положим, что наша формула F =Sесть противоречие.
Множество Г=F — в формуле А вместо i-ой переменной стоит
Пользуясь методом от противного, считаем, что множество Г, не является противоречием, тогда:
I(F’)=1
При этом