Понятие об элементарных теориях

Понятие об элементарных теориях.

Элементарные теории (теории первого порядка) служат примерами формальных аксиоматических теорий. Каждая из теорий первого порядка является расширением формализованного исчисления предикатов.

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

Например: Исходя из определения понятия группы, можно предложить следующее ее описание в виде аксиоматической теории первого порядка. К логическим символам добавляются один символ бинарной операции * и одна нелогическая предметная константа e.

К аксиомам формализованного исчисления предикатов с равенством добавляются следующие нелогические (собственные) аксиомы:

("x) ("y) ("z) (x*(y*z)=(x*y)*z),

("x) (e *x=x* e =x),

("x) ($y) (x*y=y*x= e)

Можно дать и другую формализацию этой теории, если выбрать лишь один символ бинарной операции * и следующие собственные аксиомы:

("x) ("y) ("z) (x*(y*z)=(x*y)*z),

("x) ("y) ($z) (y*z=x),

("x) ("z) ($y) (y*z=x).

Обе предложенные формулировки суть элементарной теории групп, т.е. формальной теории, в основе которой лежит исчисление предикатов первого порядка.

Термин «теория первого порядка» означает, что в теории кванторы применяются лишь по предметным переменным и не допускаются кванторы по предикатам или кванторы по функциям, т.е. в теории первого порядка не допускаются предикаты, имеющие в качестве возможных значений своих аргументов другие предикаты и функции.

Относительно тех или иных формальных теорий первого порядка могут быть поставлены вопросы об их непротеворичивости, полноте, категоричности, разрешимости. Например, для всех теорий первого порядка справедлива теорема К. Гёделя (1930г), являющаяся продолжением теоремы о полноте: Всякая непротиворечивая теория первого порядка с равенством имеет счетную нормальную модель (т.е. модель на счетном множестве).

Теорема Гёделя (о полноте): Во всяком исчислении предикатов первого порядка теоремами являются те, и только те формулы, которые логически общезначемы.

Синтаксическое определение элементарных теорий.

Опр. Формула называется замкнутой или предложением, если эта формула не содержит свободных переменных.

Опр. Пусть S - список предложений данной сигнатуры. Элементарной теорией, определяемой множеством S называется множество предложений, выводимых из S. Обозначается: Th(S). Th(S)={F|S|–F, F - предложение}.

Пример: S - это аксиоматика элементарной теории.

s=<×,=, e >

С1: "x (x=x)

С2: (x=y&y=z®x=z)

С3: "x, "y (x=y®y=x)

С4: "x, "y (x=y®(A(x)«A(y))

С5: "x, "y, "z (x(yz)=(xy)z)

С6: "x (x× e =x, &× e x=x)

С7: "x $y (x×y= e & y×x= e)

Семантическое определение элементарных теорий (с помощью модели)

Пусть K – класс моделей одной и той же сигнатуры.

Опр. Элементарной теорией Th(K) называется множество предложений, истинных на любой модели этого класса. Обозначение: Th(K)={F| " M ÎK, M╞ F, F - предложение}.

Опр. Элементарная теория называется разрешимой, если существует алгоритм, позволяющий по любому предложению данной сигнатуры определить, принадлежит ли оно данной теории или нет. Если такого алгоритма нет, то теория называется неразрешимой.