Применение логiки предикатiв

Главная - Логика - Применение логiки предикатiв

Применение логiки предикатiв

Исчисление предикатiв, не какое мiстить функцiональних букв i предметных констант, называется чистым исчислением предикатiв. Досi речь шла преимущественно именно о чистом исчислении предикатiв. Такi исчисления мiстять тiльки означенi выше так званi логiчнi аксiоми (или схемы аксiом).

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

Найтиповiшi примеры iндивiдуальних предикатних букв - предикаты = (рiвностi) i  (порядку)а функцiональних букв - знаки арифметических операцiй +, , , / и тому подобное и iнших популярных математических функцiй. Как предметнi областi найчастiше выступают множество N натуральных чисел, множество Z цiлих чисел, множество R дiйсних чисел, булеан (A) некоторого множества A и iн.

Бiльшiсть прикладных исчислений мiстить предикат рiвностi = i аксiоми, что его определяют. Например, аксiомами для рiвностi могут быть такi:

E1. x(x = x)

E2. (x = y)(F(x, x)F(x, y)),

где F(x, y) получено из F(x, x) путем замiни некоторых (не обязательно всiх) вõоджень x на y при условии, что y в этих вхождениях также остается вiльним.

Любая теорiя, в якiй E1 i E2 есть аксiомами или теоремами, называется теорiею (или исчислением) из рiвнiстю.

Из аксiом E1 i E2 нетрудно вывести теоремы, которые описывают основнi властивостi рiвностi, - рефлексивнiсть, симетричнiсть i транзитивнiсть:

t (t = t)

(x = y)(y = x)

(x = y)((y = z)(x = z)).

Аналогiчно могут быть введенi три аксiоми, что задают бiльш общий предикат - предикат еквiвалентностi E(x, y) :

Q1. xE(x, x)

Q2. xy(E(x, y)E(y, x))

Q3. xyz((E(x, y)E(y, z))E(x, y)).

Iншим прикладным исчислением является теорiя частичного порядка, какая мiстить три конкретнi аксiоми для предиката :

O1. x(xx)

O2. xy(((xy)(yx))(x = y))

O3. xyz((xy)((yz)(xz))).

Присоединив к этих аксiом аксiому

O4. xy((xy)(yx)(x = y)),