Интерпретация формальных теорий
Интерпретацией формальной теории в область интерпретации М называется функция
, которая каждой формуле формальной теории ставит в соответствие некоторое содержательное высказывание относительно объектов множества М. Если соответствующее высказывание истинно, то говорят, что формула выполняется в интерпретации I.
Интерпретация называется моделью множества формул Г, если все формулы выполняются в данной интерпретации.
Если формула истинна в любой интерпретации, то это тавтология, если формула ложна в любой интерпретации, то это противоречие.
Формальная теория называется семантически непротиворечивой, если ни одна ее теорема не является противоречием.
Модель для формальной теории существует тогда и только тогда, когда она семантически непротиворечива.
Формальная теория формально непротиворечива, если в ней нельзя одновременно вывести формулу F и ее отрицание.
Формальная теория называется полной, если каждому истинному высказыванию модели М соответствует теорема теории
.
Если для множества М существует формально полная непротиворечивая теория , то множество М называется аксиоматизируемым или формализуемым.
Формальная теория называется разрешимой, если существует алгоритм, который определяет, является ли формула теоремой теории.
Исчисление высказываний.
Опишем формальную теорию исчисления высказываний.
Исчисление высказываний – это формальная теория £, которой:
1. Алфавит:
· - буквы (A,B,…Z);
· - специальные символы ⌐ → ( ).
2. Формулы:
· любая буква A, B,…Z – формула;
· если А, В – формулы, то (А), (⌐А), (А→ В) – формулы.
3. Аксиомы:
1. А1:
2. А2:
3. А3:
Выражения А1-А3 называются схемами аксиом, т. к. каждая из них порождает бесконечное множество формул. Вместо А, В и С можно подставлять любые формулы.
4. Правило вывода: правило modus ponens (m.p.):
A и B- любые формулы. Т. о. множество аксиом теории £ - бесконечно. Множество правил вывода также бесконечно.
Производные правила вывода
Исчисление высказываний £ достаточно богатая формальная теория, в которой можно вывести многие правила вывода.
Теорема 1.
- закон тождества.
Доказательство.
1. А1: . Выполним замену {
}. Получим:
.
2. А1: . Выполним замену {
}. Получим:
.
3. Из 1 и 2 по правилу m.p. получим:
.
4. A1: {A/B}. Получим:
.
5. Из 3 и 4 по правилу m.p. получим .
Теорема 2
А - добавление антцедента.
Доказательство.
1. А - гипотеза
2. А1:
3. Из 1 и 3 по правилу m.p. получаем
Всякую доказанную выводимость можно использовать как новое производное правило вывода.
Если имеется множество общезначимых формул, то из него можно вывести только общезначимые формулы.
Дедукция
В теории £ импликация тесно связана с выводимостью. Теорема дедукции используется при доказательстве теорем, т. к. дает нам новое правило вывода.
Теорема (дедукции). Если Г – множество формул, А и B Î Г и A|-£B, то Г|-А→В.
В частности A|-B, то А→В.
Доказательство. Пусть E1,E2,….En вывод B из Г, A. En = B. Покажем, что Г|-£А→ Ei, .
Пусть i=1.
Возможны 3 случая.
1) Пусть Е1 – аксиома. Тогда рассмотрим вывод:
1. Е1
2. А1: . Выполним замену {А/Е1, В/А}. Получим:
3. Из 1 и 2 по правилу m.p. получаем |-£А→ E1.
2) Пусть Е1 Г. Доказательство аналогично 1).
3) Пусть Е1 А. Тогда по закону тождества (теорема1)
, следовательно,
Таким образом Г .
Пусть i<k. Рассмотрим вывод Ek. Возможны 4 случая:
1) Ek – аксиома.
2) Е1 Г.
3) Е1 А.
4) Ek получена из формул Ei и Ej по правилу m.p., причем i,j<k и Ei=Ej® Ek.
Для 1), 2), 3) доказательство аналогично доказательству при i=1.
Для 4) случая:
1. (i)
2. (j)
3. А2: . Выполним подстановку {Ei/B, Ek/C}, получим
(n)
4. По правилу m.p. из (j) и (n) получаем (n+1)
5. По правилу m.p. из (j) и (n+1) получаем (n+2) ч.т.д.
Таким образом, для любого k, в том числе при k=n. Но En=B Þ
.
Схема аксиом A3 теории £ в доказательстве не использовалась, поэтому теорема дедукции имеет место для более широкого класса теорий, чем £.
Следствие 1. Если , то
и обратно.
Доказательство. По теореме дедукции, если , то
. Пусть Г={0}. Тогда имеем Следствие 1.
Следствие 2. (правило транзитивности).
Доказательство.
1. Гипотеза .
2. Гипотеза с.
3. Гипотеза А.
4. По правилу m.p. из 1 и 3 получаем B.
5. По правилу m.p. из 2 и 4 получаем C
6. Из 1-5 получаем: если ,
- гипотезы Г, то
.
7. По теореме дедукции .
Следствие 3. (правило сечения).
Доказательство.
1. Гипотеза .
2. Гипотеза A.
3. По правилу m.p. из 1 и 2 получим .
4. В – гипотеза.
5. По правилу m.p. из 3 и 4 получим С.
6. Из 1-5 получаем:
7. по теореме дедукции .
2.9. Некоторые теоремы теории £
Множество теорем теории £ бесконечно. Рассмотрим некоторые из них.
1. (закон двойного отрицания).
2. (закон двойного отрицания).
3. (из ложного что угодно).
4. (закон де Моргана)
5. (закон де Моргана)
и т. д.
(Вывод законов см. Ф.А. Новиков “Дискретная математика для программистов”, стр.114).
Теорема. Теоремами теории £ являются только общезначимые формулы.
Следствие. Теория £ формально непротиворечива.
Выводы.
1. Можно задать некоторые правила преобразования формул, которые обладают свойством: при применении к общезначимым формулам они дают в результате общезначимые формулы. Такими правилами являются правила вывода.
2. Можно задать конечное число общезначимых формул таких, что любая общезначимая формула может быть получена из них с помощью правил вывода.