Теории первого порядка

В теориях первого порядка (К) допускаются кванторы и предикаты по предметным переменным. Они позволяют описывать логику достаточно содержательных математи-

ческих дисциплин - например, арифметики. Теории, в кото-рых эти ограничения сняты, имеют более высокий порядок. Рассмотрим аксиоматическое построение теорий первого порядка.

1.Определения терма и формулы остаются в силе.

2. Все множество аксиом делится на две части:

а) логические, отражающие общие свойства логических рассуждений и поэтому верные, независимо от содержания теории К, и

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

3. В качестве правил вывода в любой теории К достаточно принять правила вывода, применяемые в ИП, поскольку вы-вод формул является чисто логическим действием и пра-вильность его определяется тождественной истинностью тавтологий, используемых в них.

Простейшие примеры теорий первого порядка можно построить на основании отношений эквивалентности и по-рядка, применяемых в теории множеств.

I. Теории первого порядка с равенством. Пусть на некото-ром предметном множестве М задано некоторое множество предметных переменных Х, предметных констант A , функ-циональных переменных F.

Множество предикатных переменных содержит логи-ческую функцию Р = Р(х,у) = ‘ х эквивалентно у ’ (либо ‘x=y’). В общем случае отношение эквивалентности удов-летворяет аксиомам:

1) рефлексивности: "хÎ Х (х r x) ,

2) симметичности: "х,"у Î Х (если (х r у),то (у r x ) ,

3) транзитивности: "х,"у,"z Î Х (если хr у и уr z, то xr z).

Для того, чтобы обеспечить выполнение данных свойств в теориях с равенствами, их можно было бы непо-

средственно добавить в качестве аксиом к логическим ак-сиомам. Однако обычно вместо них используют упрощён-ный набор аксиом следующего вида:

1) "x (x = x) - рефлексивность равенства,

2) (x = y)® (A(x,x) ® A(x,y)) - подстановочность равенства.

Справедливость обычных аксиом симметричности и транзитивности можно вывести из 1)- 2) с использованием тавтологий ИВ.

II.Теория частичной упорядоченности.

Пусть М - некоторое множество объектов, Х – мно-жество предметных переменных на М.

Предметных констант нет: A =Æ .

Функциональных переменных нет: F =Æ .

Множество предикатных переменных Р = Р(х,у)=‘х строго предшествует у ’ = ‘ х < у ’.

Бинарное отношение строгого порядка удовлетворяет аксиомам:

1) антирефлексивности: "хÎ Х (х Ør x) ,

2) асимметичности: "х,"у Î Х (если (х r у),то (уØ r x ) ,

3) транзитивности: "х,"у,"z Î Х (если хr у и уr z, то xr z).

Подход к аксиоматическому заданию теории частич-ной упорядоченности, включающей данное отношение, ана-логичен включению отношения эквивалентности. Вместо полного добавления к аксиомам ИП аксиом 1)-3) присое-диняются только аксиомы 1) антирефлексивность и 3) тран-зитивность. Асимметричность можно вывести из получив-шегося набора аксиом. В теориях частичной упорядочен-ности отношение строгого порядка на элементах пред-метного множества всегда вводит строгий частичный поря-док (строгий полный - не всегда).