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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Математическая Логика и Теория Алгоритмов стр. 26 из 64
© 2003 Галуев Геннадий Анатольевич
и правило обобщения (сокращенно Gen от английского слова Generalization)
Ax
A
i
∀
.
Моделью теории первого порядка называется всякая интерпретация, в которой
истинны все аксиомы этой теории. Нетрудно показать, что если правила
MP
и Gen
применяются к истинным в данной интерпретации формулам, то результатом являют-
ся формулы, также истинные в этой интерпретации. Следовательно, всякая теорема
теории истинна во всякой ее модели.
Существует также доказательство того, что множество логических следствий
выбранных аксиом теории K в точности совпадает с множеством теорем теории К. В
частности, для исчисления предикатов
первого порядка множество его теорем совпа-
дает с множеством всех логически общезначимых формул (тождественно истинных
формул, тавтологий).
Отметим необходимость ограничений в схемах аксиом 4 и 5.
Если отказаться от ограничения из схемы 4, то можно получить следующее:
Пусть
)(
1
xA
есть ),(
21
2
12
xxAx⎤∀ и t есть
2
x
. Видно, что при этом терм t не свободен для
1
x в )(
1
xA .
Тогда частный случай схемы 4 таков:
)())((
21
2
1221
2
121
xxAxxxAxx →⎤∀⎤∀∀ )(
∗
В качестве интерпретации взамен, например, множество целых чисел и
2
1
A - от-
ношение равенства т.е.
,1)(
21
2
1
=xxA если
21
xx
=
. Тогда посылкав )(∗ (т.е. выражение
перед знаком
→) истина, а заключение (выражение после знака → в )(∗ ложно, по-
этому вся импликация
)(∗ имеет значение ложь (0).
В случае схемы 5 отказ от ограничений также приводит к неприятным послед-
ствиям. Если
A
и
B
есть
11
1
1
)(( xxA входит свободно), то частный случай схемы аксиом 5
таков
))()(())()((
1
1
111
1
11
1
11
1
11
xAxxAxAxAx ∀→→→∀ )(
∗
∗
Нетрудно убедиться, что (**) имеет значение 0 (ложь), если
)(
1
1
1
xA выполнено
для некоторых, но не для всех
1
x из предметной области.
Предваренные нормальные формы в исчислении предикатов.
В исчислении предикатов аналогично исчислению высказываний применяются
нормальные формы. Предваренные нормальные формы используются в исчислении
предикатов для упрощения процедур доказательств.
Говорит, что формула
A
исчисления предикатов находится в предваренной
нормальной форме тогда и только тогда, когда формула имеет вид
MxQxQxQ
nn
...
2211
, )(
∗
где каждое
ii
xQ есть или
i
x∀ или
i
x
∃
;,...,1 ni
=
M
- формула не содержащая кванторов.
nn
xQxQ ....
11
- называют префиксом, а
M
- матрицей формулы
A
Приводятся формулы к виду (*) с помощью эквивалентных преобразований,
в результате чего получаются новые формулы, логически эквивалентные первона-
чальным.
Для эквивалентных преобразований используются законы, установленные
теоремой (см. 2.1 – 2.10) для пропозиционных связок, а также следующие, специ-
фические для исчисления предикатов, соотношения:

Страницы