Математическое введение в декларативное программирование. Зюзысов В.М. - 24 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

4 Теории первого порядка
4.1 Синтаксические свойства истинности теорий с языком
первого порядка
Нам понадобится следующее понятие языка первого порядка. Пусть дана формула
P, свободное вхождение переменной x в P и терм t. Мы говорим, что данное вхождение x
не связывает t в P, если оно не лежит в области действия ни одного квантора вида ∀y и ∃y,
где y - переменная, входящая в t.
Иными словами, после подстановки t вместо данного вхождения x все переменные,
входящие в t, останутся свободными в P.
Чаще всего приходится подставлять терм вместо каждого из свободных вхождений
данной переменной. Важно, что такая операция переводит термы в термы и формулы в
формулы. Если каждое свободное вхождение x в P не связывает t, мы будем говорить про-
сто, что терм t свободный для x в P.
Пример
1. Терм y свободен для переменной x в формуле P(x), но тот же терм y не свободен для
переменной x в формуле ∀y P(x).
2. Терм f(x,z) свободен для переменной x в формуле ∀yP(x, y)⊃Q(x), но тот же терм f(x,z)
не свободен для переменной x в формуле ∃z∀y P(x, y)⊃Q(x).
Пусть нам даны некоторая формальная теория T с языком первого порядка и задана
интерпретация этой теории. Обозначим через F множество всех формул теории T, истин-
ных в данной интерпретации. Перечислим те свойства F, которые отражают заложенные в
языки первого порядка логику, независящую от конкретных особенностей интерпретации.
Для любой замкнутой формулы P, либо P∈F, либо ¬P∈F. •
•
•
•
•
Множество F не содержит противоречия, т. е. ни для какой формулы P не может быть,
чтобы одновременно выполнялось P∈F и ¬P∈F.
Множество F содержит все тавтологии.
Множество F содержит следующие общезначимые формулы (называемые «логические
аксиомы с кванторами»):
∀x A(x) ⊃A(t),
где A(t) есть формула теории T и t есть терм теории T, свободный для x в A(x). Заме-
тим, что t может совпадать с x, и тогда мы получаем аксиому ∀xA(x) ⊃A(x).
∀x (A ⊃ B(x)) ⊃ (A⊃∀x B(x)),
где A не содержит свободных вхождений переменной x.
Множество F замкнуто относительно правил вывода modus ponens и обобщения. По
определению это означает, что если A∈F и A⊃B ∈F, то также B∈F; если A∈F, то
∀xA∈F для любой переменной x.
4.2 Определение теории первого порядка
Аксиоматическая формальная теория с языком первого порядка называется теори-
ей первого порядка, если она имеет следущие аксиомы и правила вывода..
Аксиомы теории первого порядка T разбиваются на два класса: логические аксио-
мы и собственные (или нелогические) аксиомы.
Логические аксиомы: каковы бы ни были формулы A, B и C теории T, следующие
формулы являются логическими аксиомами теории T.
A
1
. A⊃(B⊃A);
A
2
. (A⊃(B⊃C)) ⊃ ((A⊃B) ⊃ (A⊃C));
A
3
. (¬B⊃¬A) ⊃ ((¬B⊃A) ⊃B);
24

Страницы