Математическая логика и теория алгоритмов. Галуев Г.А. - 25 стр.

UptoLike

ВУЗ: 

ТТИ ЮФУ | Таганрог

Составители: 

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 25 из 64
© 2003 Галуев Геннадий Анатольевич
Будем называть формулу
A
противоречием (в исчислении предикатов), если
формула
A⎤ является логически общезначимой (т.е. формула A ложна во всякой ин-
терпретации):
Говорят, что формула
A
является логическим следствием (в исчислении преди-
катов) множества формул Г, если во всякой интерпретации формула
A выполнена на
каждой последовательности, на которой выполнены все формулы из Г.
Формулы называются логически элементарными (в исчислении предикатов),
если каждая из них является логическим следствием другой.
С учетом введенных понятий и определений перейдем к изложению аксиомати-
ческого построения исчислений предикатов.
Аксиоматическое построение исчисления предикатов.
Теории первого порядка. Исчисление предикатов первого порядка.
В исчислении высказываний изучение таблиц истинности пропозиционных форм
дает эффективный метод проверки, является ли данная формула тавтологией (обще-
значимой, тождественно истинной – т.е. истинной при любых значениях пропозици-
онных букв). В исчислении предикатов, где предметные области могут быть беско-
нечны, аналогичный подход неприемлем. Здесь возникает необходимость в аксиома-
тизации и
построении соответствующей теории. Рассматриваемые далее теории отно-
сятся к так называемым теориям первого порядка, в которых не допускаются, напри-
мер, такие конструкции как предикаты, аргументы которых в свою очередь являются
предикатами.
Символами всякой теории К первого порядка служат: пропозиционные связ-
ки
→⎤, ; знаки ),(, ; предметные переменные ,...,....,,
21 n
xxx ; предикатные буквы
)1,( ≥jnA
n
j
; функциональные буквы )1,( ≥jnf
n
j
; предметные константы )1( ≥ia
i
.
Функциональные буквы и предметные константы в некоторых теориях могут и
отсутствовать.
Введенные ранее определения терма и формулы, а также определения связок
,,&, ↔V через →⎤, :
BA & есть
)( BA ¬→⎤
B
A∨ есть
BA →⎤
BA ↔ есть
)(&)( ABBA →→
остаются в силе.
Аксиомы каждой теории К первого порядка разбиваются на два класса: логиче-
ские аксиомы и собственные (нелогические) аксиомы.
К логическим аксиомам теории первого порядка относятся следующие:
1.
)( ABA →→
2.
))()(()(( CABACBA →→→→→→
3.
))(()( BABAB →→⎤→→⎤⎤
4.
)()( tAxAx
ii
→∀ ,
где
)(
i
xA - это формула теории
K
и t есть терм, свободный для
i
x в )(
i
xA .
5.
)()( BxABAx
ii
∀→→→∀ , если формула A не содержит
i
x свободно.
Здесь
CBA ,, - произвольные формулы.
Собственные аксиомы меняются от теории к теории и не могут быть сформули-
рованы в общем виде. Теория первого порядка, не содержащая собственных аксиом,
называется исчислением предикатов первого порядка
.
Правилами вывода во всякой теории являются правило
MP
B
BAA →,
,

Страницы