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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

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
Теория первого порядка, которая не содержит собственных аксиом называется ис-
числением предикатов первого порядка. Чистым исчислением предикатов называется ис-
числение предикатов первого порядка, не содержащее предметных констант и функторов.
Как мы увидим позже, логические аксиомы выбраны таким образом, что множест-
во логических следствий аксиом теории в точности совпадает с множеством теорем тео-
рии. В частности, для исчисления предикатов первого порядка множество его теорем сов-
падает с множеством логически общезначимых формул.
Общезначимые формулы в теории первого порядка играют ту же роль, что тавтоло-
гии в логике высказываний. Между ними есть и формальная связь: если взять любую тав-
тологию и вместо входящих в нее пропозициональных переменных подставить произ-
вольные формулы языка первого порядка, то получится общезначимая формула. В самом
деле, пусть есть некоторая интерпретация теории, при которой как-то зафиксированы зна-
чения предметных переменных. Тогда каждая из подставленных формул станет истинной
или ложной, а значение всей формулы определяется с помощью таблиц истинности для
логических связок, то есть по тем же правилам, что и в логике высказываний.
Конечно, бывают и другие общезначимые формулы, не являющиеся частным слу-
чаем пропозициональных тавтологий. Например, формула
∀xA(x)⊃∃yA(y)
общезначима (здесь существенно, что универсум любой интерпретации непуст).
4.3 Некоторые свойства теорий первого порядка
Для теорий первого порядка можно уточнить некоторые понятия, введенные ранее.
Формула P является противоречием, тогда и только тогда, когда формула ¬P яв-
ляется общезначимой.
Формальная теория T называется (формально) непротиворечивой, если в ней не
являются выводимыми одновременно формулы P и ¬P.
Имеет место метатеорема:
Теория T формально непротиворечива тогда и только тогда, когда она семантиче-
ски непротиворечива.
Из определений логического следования и эквивалентности непосредственно выте-
кают следующие утверждения:
A ⇒ B тогда и только тогда, когда |= A ⊃ B;
A = B тогда и только тогда, когда |= A ~ B.
Имеют место также следующие логические следования и эквивалентности (форму-
лы A и B − произвольны, формула C не содержит никаких вхождений переменной x):
¬∀xA(x) = ∃x¬A(x), ¬∃xA(x) = ∀x¬A(x);
∀x(A(x)&B(x)) = ∀x A(x)&∀xB(x), ∃x(A(x)∨B(x)) = ∃xA(x)∨∃xB(x);
∃x(A(x)&B(x)) ⇒ ∃xA(x)&∃xB(x), ∀xA(x)∨∀xB(x) ⇒ ∀x(A(x)∨B(x));
∀x∀yA(x,y) = ∀y∀xA(x,y), ∃x∃yA(x,y) = ∃y∃xA(x,y);
∀x(A(x)&C) = ∀xA(x)&C, ∀x(A(x)∨C) = ∀xA(x)∨C;
25

Страницы