Альтернативные системы аксиом
Методическое пособие - Философия
Другие методички по предмету Философия
° t при оценке переменных ? (последнее правило оценки не применяется, так как все вхождения переменных втерм t свободны).
В точности те же оценки получат эти вершины, когда вычисляется оценка формулы A при оценке переменных ??.
В остальных вершинах оценки формул A и A(x:=t) и подавно совпадают (там записано одно и то же).
Итак, при оценке переменных ?? оценкой формулы A является ложь. То же самое верно для формулы A(x:=t) при оценке ?. Тогда по последнему правилу оценки формула ?xA имеет оценку ложь при оценке ?. Значит, в этом случае оценка формулы ?xA>A(x:=t) - истина.
Итак, при обеих возможных оценках формулы A(x:=t) формула ?xA>A(x:=t) имеет оценку истина. Поэтому она общезначимая.
Корректность ИП и следствия из нее
Теорема. В ИП выводимы только общезначимые формулы.
Доказательство. Нужно проверить общезначимость аксиом и то, что правила вывода сохраняют общезначимость. Мы уже доказали общезначимость аксиом: аксиомы (A1-A3) общезначимы по утв. 3.38 (Пусть A - тавтология, x1,. . . , xn - набор пропозициональных переменных, которые входят в A, а F1, . . . , Fn - формулы ИП. Тогда формула A(F1, . . . , Fn) - общезначима), а общезначимость аксиом (A4-A5) доказана в утверждениях3.48, 3.45 (Если терм t свободен для переменной x в формуле A, то формула ?xA>A(x:=t)-общезначима и Если в формуле A нет свободных вхождений переменной x, то формула ? x(A>B)>(A>?xB) - общезначима).
(A1)
(A2)
(A3)
(A4)в условиях 3.48
(A5) в условиях 3.45
Если при некоторой оценке переменных формулыA, A>B истинны, то и формула B также истинна при этой оценке переменных. Поэтому правило modusponens из общезначимых формул выводит только общезначимые.
Остаётся проверить, что правило обобщения сохраняет общезначимость. Действительно, из общезначимости A следует, что в любой интерпретации при любой оценке переменных она истинна. Но тогда по определению интерпретации квантора формула ?x A также истинна в любой интерпретации при любой оценке переменных.
Как следствие получаем непротиворечивость исчисления предикатов. Поскольку в исчислении предикатов выводятся только общезначимые формулы, то из формул A и -|A выводимой может быть только одна.
Буквально так же, как в исчислении высказываний, определяется вывод из множества формул (гипотез). Формулы, выводимые из аксиом исчисления предикатов и аксиом некоторой теории T , называются выводимыми в T или (формальными) теоремами теории T. Так как аксиомы исчисления предикатов содержат аксиомы исчисления высказываний, а правило modus ponens является одним из правил вывода, то любая тавтология выводима в исчислении предикатов. Мы сформулируем это утверждение в виде леммы.
Лемма 3.53. Пусть A1, A2, . . . , An- формулы исчисления предикатов, а ?(x1, . . . , xn) - тавтология, в которую входят переменные x1, . . . , xn. Тогда формула ?(A1, . . . ,An) выводима в исчислении предикатов.
Доказательство этой леммы очевидно: нужно подставить в вывод формулы ? в исчислении высказываний вместо переменных xi формулы Ai. Полученная последовательность формул будет выводом в исчислении предикатов.
Ослабленная и слабая теорема дедукции
Теорема 3.54 (ослабленная теорема дедукции).Если ?,A ? B и существует вывод B из ?,A, в котором не применяется правило обобщения к свободным переменным формулы A, то ? ? A>B.
Доказательство. Следуем схеме доказательства теоремы дедукции для исчисления высказываний: вывод ?1, . . . ,?n формулы B из гипотез ?,A, который существует по условию теоремы, заменяется на последовательность формул A>?1, . . . ,A>?n и индукцией по n доказывается, что эту последовательность можно дополнить до вывода. Для этого надо разобрать два случая.
. Формула ?i является аксиомой (A1-A5) или формула ?i получена по правилу modusponens из предыдущих формул ?j , ?k, j, k < i. В этих случаях построение вывода A>?i в предположении, что уже выведены формулы A>?k, k < i, в точности повторяет доказательство теоремы дедукции для исчисления высказываний.
. Формула ?i является выводом по правилу Gen из формулы ?k, k < i. Это означает, что ?i = ?x?k. Добавим следующие формулы перед формулой A>?i:
? x(A>?k) (Gen)
? x(A>?k)>(A>?x?k) (A5)
В первой строке правило обобщения применяется к формуле A>?k, которая встречается раньше формулы A>?i в последовательности формул, которую мы пополняем. Вторая строка - это аксиома (A5). Условия утверждения 3.45 (Если в формуле A нет свободных вхождений переменной x, то формула
? x(A>B)>(A>?xB)
общезначима) в данном случае выполнены, потому что по условию x не является свободной переменной формулы A.
Следствие 3.55 (слабая теорема дедукции).
Если ?,A ? B иформула A замкнутая, то?? A>B.
Доказательство. Замкнутая формула вообще не содержит свободных переменных, поэтому любой вывод B из ?,A удовлетворяет условию теоремы 3.54.
Теорема о полноте ИП
Теорема о полноте для ИП:
В любом ИП 1-го порядка формула является тавт-ей она общезначимой.
Док-во:
Покажем, что если - теорема, то она общезначима.
Проверяем непосредственно, что схемы аксиом явл. общезначимы: (A1) - (A5)
MP и G из из общезначимых формул дают общезначимые формулы => любая теорема - общезначима.
Утв.: (Гёдель)
Любой раздел математики может быть описан как теория 1-го порядка.
Пример теории 1-го порядка, аксиоматическая арифметика. Теорема Гёделя о неполноте
Пусть задана произвольная теория 1-го порядка. Если к ее алфавиту добавить предикат "равенство": P(x, y) = (по опр.) "x = y" и в число собствен?/p>