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

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

∀xA(x)⊃∃yA(y)
общезначима (здесь существенно, что универсум любой интерпретации не пуст).
Некоторые свойства теорий первого порядка
Для теорий первого порядка можно уточнить некоторые понятия, введенные в 4.1.
Формула 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;
∃x(A(x)&C) = ∃xA(x)&C, ∃x
(A(x)∨C) = ∃xA(x)∨C;
C⊃∀xA(x) = ∀x(C⊃A(x)), C⊃∃xA(x) = ∃x(C⊃A(x));
∀xA(x)⊃C ⇒ ∃x(A(x)⊃C).
Имеет место следующее утверждение:
Теорема 14. Если теория первого порядка (формально) противоречива, то в ней
выводима любая формула.
Доказательство. В самом деле, пусть формулы A и ¬A выводимы в теории.
Формула ¬A⊃(A⊃B) является тавтологией в исчислении высказываний, следовательно,
она выводима. Её вывод, поскольку он содержит только MP, остается выводом и в любой
теории первого порядка. Поэтому формула ¬A⊃(A⊃B) выводима в теории первого
порядка. Дважды применяя MP, мы получаем вывод произвольной формулы B.
Таким образом, для доказательства непротиворечивости какой-либо теории
первого порядка достаточно установить невыводимость в этой теории хотя бы одной
формулы.
Теорема 15. (Гёдель, 1930). Всякая общезначимая формула теории T первого
порядка является теоремой теории T.
Значительная часть теорем логики состоит в доказательстве утверждений
вида
«Γ|–P» или «не Γ|–P» для разных теорий первого порядка, множеств Γ и разных (классов)
формул P.
Результат «Γ|–P» может доказываться посредством предъявления описания вывода
формулы P из Γ. Однако в мало-мальски сложных случаях оно оказывается настолько
длинным, что заменяется инструкцией по составлению такого описания, более
или менее
полной. Наконец, доказательство «Γ|–P» может вообще не сопровождаться предъявлением

Страницы