Теория алгоритмов. Зюзысов В.М. - 35 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

связывает 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 разбиваются на два класса: логические
аксиомы и собственные (или нелогические) аксиомы.
Логические аксиомы: каковы бы ни были формулы 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);
A
4
. ∀x A(x) ⊃A(t), где A(t) есть формула теории T и t есть терм теории T, свободный для x в
A(x). Заметим, что t может совпадать с x, и тогда мы получаем аксиому ∀xA(x) ⊃A(x).
A
5
. ∀x (A ⊃ B(x)) ⊃ (A⊃∀x B(x)), где A не содержит свободных вхождений переменной x.
Собственные аксиомы: таковые не могут быть сформулированы в общем случае,
ибо меняются от теории к теории. Правилами вывода во всякой теории первого порядка
являются
1. Modus ponens:
MP
B
BAA ⊃,
2. Правило обобщения:
)(
)(
xxA
xA
∀
Gen
Теория первого порядка, которая не содержит собственных аксиом, называется
исчислением предикатов первого порядка. Чистым исчислением предикатов
называется исчисление предикатов первого порядка, не содержащее предметных констант
и функторов.
Как мы увидим позже, логические аксиомы выбраны таким образом, что
множество логических следствий аксиом теории в точности совпадает
с множеством
теорем теории. В частности, для исчисления предикатов первого порядка множество его
теорем совпадает с множеством логически общезначимых формул.
Общезначимые формулы в теории первого порядка играют ту же роль, что
тавтологии в логике высказываний. Между ними есть и формальная связь: если взять
любую тавтологию и вместо входящих в нее
пропозициональных переменных подставить
произвольные формулы языка первого порядка, то получится общезначимая формула. В
самом деле, пусть есть некоторая интерпретация теории, при которой как-то
зафиксированы значения предметных переменных. Тогда каждая из подставленных
формул станет истинной или ложной, а значение всей формулы определяется с помощью
таблиц истинности для логических связок, то есть
по тем же правилам, что и в логике
высказываний.
Конечно, бывают и другие общезначимые формулы, не являющиеся частным
случаем пропозициональных тавтологий. Например, формула

Страницы