Для каждой из следующих формул найдите вывод из пустого множества посылок.
3.27 x = y Й f(x, y) = f(y, x).
3.28 " x $ y (y = f(x)).
3.29 $ y (x = y & y = z) Й x = z.
3.30 $ x (x = a & P (x)) є P (a).
Теории первого порядка
Теория первого порядка сигнатуры s определяется с помощью аксиом. Интерпретация, при которой истинны все аксиомы теории первого порядка G, называется моделью G. Если теория первого порядка G выполнима, мы также говорим что она непротиворечива. Логические следствия теории первого порядка называется её теоремами. Доказательство предложения F в теории первого порядка G есть вывод F из подмножества аксиом из G.
Теоремы корректности и полноты выполняются для логик предикатов с функциональными символами и равенством и могут быть сформулированы в рамках теорий первого порядка следующим образом. В соответствие с теоремой корректности, если существует доказательство предложения F в теории первого порядка G, тогда F является теоремой G. В соответствие с теоремой полноты Гёделя, обратное также верно: для любой теоремы F теории первого порядка G, существует доказательство F в G. Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.
Арифметика первого порядка
Мы будем упрощать запись формул сигнатуры арифметики первого порядка (6) введением следующего обозначения: a будет записываться как 0, s(t) как t' , f(t1, t2) как t1+t2, и g(t1, t2) как t1 · t2. Аксиомы арифметики первого порядка являются универсальным замыканием следующих формул:
8. x' № 0.
9. x'= y'Й x = y.
10. (F(0) & " v (F(v) Й F(v'))) Й " v F(v) для любой формулы F(v).
11. x + 0 = x.
12. x + y'= (x + y)'.
13. x · 0 = 0.
14. x · y'= x · y + x.
Интерпретация (7) является моделью этой теории. Арифметика первого порядка имеет также другие модели, и некоторые из них совсем не похожи на систему натуральных чисел (задача 3.40).
В следующих формулах 1 обозначает терм 0', 2 – 0'', и 4 – 0''''. Через t1 Ј t2 мы обозначаем формулу $ v(t2 = t1 + v), где v – первая объектная переменная, которая не встречается в t1, t2.
Дата добавления: 2015-10-05; просмотров: 717;