Аксиоматические теории первого порядка

1. Аксиоматические теории первого порядка

2.

При
исследовании
конкретной
математической теории фиксируют некоторые
наборы исходных предикатных символов
P1 ,..., Pk
соответствующей арности n1 ,..., nk ,
исходных функциональных символов f1 ,..., f l
соответствующей арности m1 ,..., ml и исходных
предметных символов a,b,....
{P1 ,..., Pk ; f1 ,..., f l ; a, b,...}
Множество
называется
алгебраическим
типом
или
сигнатурой математической теории.

3.

Принципиальное отличие УИП от ИП
заключается в следующем.
1. Алфавит УИП состоит из предметных
переменных, логических и вспомогательных
символов, а также некоторых исходных
P1 ,..., Pk
предикатных
символов
соответствующей арности n1 ,..., nk , некоторых
исходных функциональных символов f1 ,..., f l
соответствующей арности m1 ,..., ml и некоторых
исходных предметных символов a,b,... .

4.

В результате элементы области интерпретации
такого языка будут описываться не только с
помощью предметных переменных, но и с
помощью
так
называемых
термов
–
специальных выражений языка, которые
индуктивно определяются следующим образом:
а) все предметные переменные и предметные
символы являются термами,
б)
если
f
–
сигнатурный
n-арный
функциональный символ и t1 ,...,t n – термы, то
выражение f (t1 ,...,t n ) является термом.

5.

2. Формулы УИП определяются по аналогии с
формулами ИП за исключением исходного шага
индукции – определения атомарных формул,
которые в данном случае имеют вид выражений
t1 t 2 , P (t1 ,..., t n ) для любых термов t1 , t 2 ,...,t n и
сигнатурных n-арных предикатных символов P.
Записывают ( x1 ,..., xn ) , если в формулу
входят предметные переменные x1 ,..., xn .
Формула без свободных вхождений переменных
называется
замкнутой
формулой
или
предложением.

6.

3. Множество аксиом УИП описывается пятью
определенными в предыдущем разделе схемами
аксиом A1 A5 , в которых , , i i 1,2,3 теперь
являются произвольными формулами УИП, и
дополнительной системой формул специальных
аксиом рассматриваемой математической теории.
Аксиомы первого вида называются логическими и
аксиомы второго вида – нелогическими аксиомами
УИП.
4. Правилами вывода УИП являются правило
modus ponens (MP) и правило обобщения (Gen).

7.

5. Формула называется теоремой УИП, если
найдется такая конечная последовательность
формул 1 ,..., n , в которой n = и каждая формула
i 1 i n либо является логической аксиомой из
схем A1 A5 , либо является нелогической
аксиомой из множества , либо получается из
некоторых
предыдущих
формул
этой
последовательности j 1 j i по одному из
правил вывода MP или Gen.
Последовательность формул 1 ,..., n называется
выводом или доказательством формулы .

8.

Вывод формулы сокращенно обозначают
символом | и говорят, что « есть теорема».
Множество всех таких теорем обозначается
символом Th ( ) и называется элементарной
теорией (или теорией первого порядка) узкого
исчисления предикатов сигнатуры с
множеством аксиом .

9. Интерпретация формул теории первого порядка

10.

При исследовании конкретной математической
теории фиксируют некоторые наборы исходных
предикатных символов P1 ,..., Pk соответствующей
арности n1 ,..., nk , исходных функциональных
символов f1 ,..., f l соответствующей арности m1 ,..., ml
и исходных предметных символов a,b,....
Множество {P1 ,..., Pk ; f1 ,..., f l ; a, b,...} называется
алгебраическим
типом
или
сигнатурой
математической теории.
Рассматривается язык формул узкого исчисления
предикатов (УИП) сигнатуры .

11.

Принципиальное отличие интерпретации
формул языка УИП от описанной ранее
интерпретации формул алгебры предикатов
заключается в том, что определение истинности
формул УИП сигнатуры вводится с помощью
интерпретации этого языка в конкретных
алгебраических системах с первоначально
фиксированными
предикатными,
функциональными и предметными символами
сигнатуры .

12.

Для придания содержательного смысла формулам
УИП сигнатуры задается:
область интерпретации – непустое множество
M, которое является областью возможных
значений всех предметных переменных,
на множестве M для каждого символа сигнатуры
фиксируется
соответствующий
математический
объект:
для
каждого
предикатного символа P арности n
фиксируется n -арное отношение PM M n , для
f
каждого функционального символа
арности n фиксируется n -арная алгебраическая
операция f M : M n M и для каждого предметного
символа a фиксируется элемент a M M .

13.

В результате получается алгебраическая
система с основным множеством M, которая
называется алгебраической -системой и
обозначается
или
просто M (M , ) . Такая система называется
также интерпретацией языка УИП сигнатуры
.
Конкретные
значения
предметным
переменным по-прежнему присваиваются с
помощью оценок предметных переменных, т.е.
отображений таких переменных в область
интерпретации M.

14. Выполнимость формул теории первого порядка

15.

Выполнимость формулы M | :
1) при оценке каждый терм t t ( x1 ,..., xn )
интерпретируется в M ( M , ) ее элементом
(t ) t ( ( x1 ),..., ( xn )) ,
который
получается
в
результате вычисления для элементов ( x1 ),..., ( xn )
значений соответствующих сигнатурных операций,
с помощью которых определяется терм t ;
2) если - атомарная формула t1 t 2 для термов
t1 ,t 2 , то M | равносильно (t1 ) (t 2 ) ;
3) если - атомарная формула вида P t1 ,...,tn для
n-местного предикатного символа P и термов
t1 ,...,tn ,
то M | равносильно тому, что
PM (t1 ),..., (tn ) истинно;

16.

Определение. В интерпретации M формула
называется:
общезначимой
(или
тождественно
истинной) и записывается M | , если
M | при любых оценках ;
выполнимой, если M | для некоторой
оценки ;
опровержимой, если для некоторой оценки
неверно, что M | ;
тождественно ложной, если для любой
оценки неверно, что M | .

17.

Определение. Интерпретация M языка УИП
сигнатуры называется моделью множества
формул , если в этой интерпретации M
тождественно истинны все формулы .
Определение.
Формула
называется
общезначимой формулой узкого исчисления
предикатов сигнатуры с множеством аксиом ,
если она тождественно истинна в любой модели
множества формул . Множество всех таких
общезначимых формул обозначим T ( ).
Главная цель - определение такой системы
нелогических аксиом , для которой Th ( )=T ( ).

18. Примеры теорий первого порядка

19.

Теория полугрупп. Пусть сигнатура
f
содержит
один
бинарный
функциональный символ f , для которого
используется инфиксная запись с помощью
символа : для любых предметных переменных
x,y терм f ( x, y) обозначается x y , или просто
xy . Тогда термамы сигнатуры : ( x1 x2 )...xk и
атомарные формулы: ( x1 x2 )...xk ( y1 y2 )...ym (для
x1 ,..., xk , y1 ,..., y m
некоторых
и правильно
расставленных скобок).
Рассмотрим систему аксиом : ( xy) z x( yz ) ,
выражающую
свойство
ассоциативности
операции умножения.
1.

20.

Моделями множества формул языка УИП
сигнатуры являются алгебры с одной
ассоциативной бинарной операцией, которые
называются полугруппами.
Примеры полугрупп дают основные
числовые множества с операциями сложения
или умножения, а также множества всех
преобразований любого непустого множества с
операцией композиции.
Элементарная теория Th ( ) называется
теорией полугрупп.

21.

2. Теория упорядоченных множеств. Пусть
сигнатура P содержит один бинарный
предикатный символ P , для которого используется
инфиксная запись с помощью символа : формула
P( x, y) обозначается x y .
Система аксиом :
x x, x y y x x y,
x y y z x z.
В этом случае моделями множества формул
языка УИП сигнатуры являются множества с
отношением
порядка,
которые
называются
упорядоченными множествами.
Элементарная теория Th ( ) называется теорией
упорядоченных множеств.

22.

3. Теория арифметики. Сигнатура , , S ,0
содержит два бинарных функциональных символа
+, (для которых используется инфиксная запись),
один унарных функциональный символ S и один
предметный символ 0.
Система аксиом : S ( x) S ( y) x y , S ( x) 0 ,
x 0 x , x 0 0 , x S ( y) S ( x y) , x S ( y) xy x ,
(0) x ( ( x) S ( x) ) x ( x) ,
где (x) – произвольная формула языка УИП
рассматриваемой
сигнатуры
Ω,
содержащая
единственную свободную переменную x.
Элементарная теория Th ( ) называется теорией
арифметики и обозначается Ar.

23.

Моделью такой теории является, например,
множество неотрицательных целых чисел N0 с
бинарными операциями сложения + и умножения
чисел, унарной операцией S ( x) x 1 и выделенным
числом 0. Такая модель N0=(N0;+, ,S,0) называется
стандартной моделью арифметики.
С другой стороны, известно, что теория Ar имеет
также модели, которые существенно отличаются от
стандартной модели N0 и которые называются
нестандартными моделями теории арифметики.
Отметим, что теория Ar принято называть также
арифметикой Пеано в честь итальянского
математика Дж.Пеано, который в 1891 году впервые
рассмотрел аксиоматику множества натуральных
чисел.

24.

Эта аксиоматика принципиально отличалась от
описанной выше системы только последней
аксиомой,
которая
Дж.Пеано
была
сформулирована в форме следующего принципа
математической индукции:
если P(n) – такое свойство натуральных чисел,
что P(0) (т.е. 0 обладает этим свойством P ) и
P(n) P S (n) (т.е. вместе с любым натуральным
числом n этим свойством P обладает
следующее за ним число n+1), то данным
свойством P обладает каждое натуральное
число.

25.

С одной стороны, аксиоматика Пеано имеет
единственную модель – множество натуральных
чисел N0=(N0;+, ,S,0), но, с другой стороны,
последняя аксиома Пеано не может быть
выражена на языке УИП рассматриваемой
сигнатуры , , S ,0 .
Известная теорема Геделя о неполноте
формальной арифметики показывает, что
множество всех формул языка УИП сигнатуры
, , S ,0 , тождественно истинных на алгебре
N0=(N0;+, ,S,0), существенно шире элементарной
теории арифметики Ar.

26. Свойства теорий первого порядка

27.

Теория первого порядка Th ( ) называется:
непротиворечивой, если в ней нельзя
доказать никакое предложение вместе с
его отрицанием ;
полной, если она содержит любое
предложение или его отрицание ;
разрешимой, если есть эффективная
процедура, позволяющая для любой
формулы определить, является она
теоремой этой теории или нет.

28.

Теорема Геделя о существовании модели. Теория
первого порядка непротиворечива в том и только
том случае, если она имеет модель.
В частности, все перечисленные выше теории
непротиворечивы.
Теорема Геделя о полноте. Для любого множества
формул языка УИП сигнатуры теория первого
порядка Th ( ) состоит из тех и только тех формул
этого языка, которые общезначимы на всех моделях
множества аксиом .

29.

Для алгебраической -системы A обозначим
Th (A)
множество всех формул сигнатуры ,
которые общезначимы на A.
Лемма. Для любой алгебраической -системы A
множество формул
Th (A)
удовлетворяет
следующим свойствам:
1) множество
первого порядка;
Th (A)
является теорией
2) теория Th (A) непротиворечивая;
3) теория Th (A) полная.
В частности, для алгебры неотрицательных целых
чисел N0=(N0;+, ,S,0) множество формул Th (N0)
языка УИП сигнатуры , , S ,0 является полной
теорией.

30.

В частности, для алгебры неотрицательных
целых чисел N0=(N0;+, ,S,0) множество формул
Th (N0) языка УИП сигнатуры , , S ,0
является полной теорией.
С другой стороны, теория полугрупп не
является полной, так как, например, ни
x, y ( xy yx) ,
предложение
ни
его
отрицание не принадлежат этой теории в
силу того, что есть как коммутативные, так и
некоммутативные полугруппы.

31.

Теорема Геделя о неполноте арифметики.
Теория
Ar
является
собственным
подмножеством теории Th (N0).
Доказано также, что теория Th (N0) в
принципе не имеет разрешимой системы аксиом
(для которой есть алгоритм, распознающий по
любой формуле языка УИП сигнатуры
, , S ,0 , является ли она аксиомой или нет).