Лекция №8

Вид материалаЛекция

Содержание


Использование равносильностей для упрощения формул.
По предположению индукции
A->a)->((a->b)->(a->ab)) (ii
A->b, b->c├─ a->c.
Ab->c ├─ a ->(b->c).
R->a)->(a->r) (iv
Подобный материал:
1   2   3   4
§ 9.3. Равносильность формул. Основные отношения равносильности.


Определение 9.3.1. Формулы А, В алгебры предикатов сигнатуры σ называются равносильными на алгебраической системе М(σ), если они принимают на М(σ) одинаковые значения при любом наборе значений предметных переменных, имеющих свободные вхождения переменных в А или В.

Из определения 9.3.1 видно, что равносильность тех или иных формул сигнатуры σ зависит от свойств алгебраической системы М(σ). Например, формулы xA и xA равносильны на любой одноэлементной системе, однако не равносильны в общем случае. Можно привести и менее тривиальные примеры. Изучение равносильностей, имеющих место для отдельных конкретных алгебраических систем, не отвечает целям и задачам математической логики как науки об общих закономерностях в рассуждениях. В связи с этим более ценным является следующее понятие равносильности.

Определение 9.3.2. Формулы алгебры предикатов сигнатуры σ называются равносильными, если они равносильны на любой алгебраической системе сигнатуры σ.

Равносильность формул А, В, как и равносильность высказываний будем обозначать в виде АВ.

Отметим следующие очевидные свойства равносильности формул.

1.Отношение равносильности формул является отношением эквивалентности на множестве всех формул сигнатуры σ, и, следовательно, все указанные формулы разбиваются на классы равносильных формул.

2.Если формула A’ получена из А заменой некоторой подформулы В равносильной ей формулой В’, то А’=А.

Приведем примеры равносильностей, называемых иногда основными равносильностями алгебры предикатов.

1. ABBA

2. AvBBvA 1, 2 – законы коммутативности
  1. (AB)CA(BC)
  2. (AvB)vCAv(BvC) 3, 4 – законы ассоциативности
  3. A(BvC)ABvAC
  4. AvBC(AvB)(AvC) 5, 6 - законы дистрибутивности
  5. A(AvB)A
  6. AvABA 7,8 – законы поглощения
  7. AAA
  8. AvA A 9, 10 – законы идемпотентности

__ _ _
  1. ABAvB

____ _ _

12. AvB A B 11, 12 – законы де Моргана

_ _
  1. A->BB->A закон контрапозиции


  1. AA закон двойного отрицания


15.A v Aи закон исключенного третьего


16.AAл закон противоречия


17.(A->B)(B->C)->(A->C)и правило силлогизма


18. хуАухА 18, 19 – правила перестановки


19. хуАухА одноименных кванторов

___ _

20. хАxA 20, 21 – правила отрицания кванторов

___ _

21. xAxA


22. x(AB)xAxB 22, 23 – законы дистрибутивности


23. x(AvB)xAvxB кванторов ,  относительно


операций  и v (соответственно);

24. A->BA->B;


25. δxA*Bδx(A*B), где δ – квантор  или , *-операция  или v и формула В не содержит вхождений х;


26. δхА(х)δуА(у), где δ – квантор  или , А(х) – формула, не содержащая вхождений буквы у, а А(у) – формула, полученная из А(х) заменой всех свободных вхождений х на у.


Перечисленные равносильности являются следствиями свойств логических операций, а потому имеют место для любых систем. В связи с этим их называют основными законами логики предикатов. Они постоянно (явно или неявно) используются при доказательствах утверждений во всех разделах математики.

Так, зачастую вместо теоремы вида А -> В доказывается равносильное утверждение А ->В. При этом используется закон контрапозиции 13. Закон исключенного третьего 15 обычно используется при доказательствах от противного, когда для доказательства теоремы А опровергают утверждение А и отсюда на основании равносильности A v A  и делают вывод об истинности А. Правило силлогизма 17 позволяет сводить доказательства теоремы вида А->С к доказательству цепочек более простых утверждений, например, А->В, В->С.

С другой стороны, в доказательствах иногда допускаются ошибки, состоящие в замене утверждения на равносильным ему предложением. Так по аналогии с равносильностями 18-19, разрешающими переставлять одноименные кванторы, иногда переставляют и разноименные кванторы. Этого делать нельзя, поскольку и в общем случае формулы вида


хуА и ухА (1)


не равносильны. Например формула ху(x < y) истинна на N, а формула ху(x < y) ложна.

Аналогичные ошибки допускаются с использованием правила дистрибутивности кванторов  и  относительно операций v и  (соответственно). Покажите в качестве упражнения, что формулы

х(A v B) и хА v xB,

a также формулы

х (A  B) и хА  xB

в общем случае не равносильны.

Заметим, что равносильность формул А, В эквивалентна истинности формулы

(A->B)  (B->A)

или двух формул

A->B, B->A.


Однако практически зачастую бывает так, что из двух последних формул истинна только одна. Так, приведенные выше формулы (1) в общем случае не равносильны, но формула


ухА -> хуА


истинна на любой алгебраической системе.

Если формула А->В истинна на системе М(σ), то при любом наборе значений предметных переменных, имеющих свободные вхождения в формулу А->В, формула В принимает истинное значение всякий раз, когда истинным является значение А. В связи с этим говорят, что формула В является следствием формулы А.

Свойства отношения логического следования формулы из формул также широко используются при доказательствах. В рассуждениях при доказательствах иногда используется также известный в математической логике принцип двойственности.

Определение 9.3.3. Пусть А – формула алгебры предикатов, не содержащая операции ->. Формула, полученная из А заменой всех вхождений  на ,  на ,  на ,  на , называется двойственной к А и обозначается через А*.

Очевидно, что (А*)*= А, и потому формулы А и А* называются двойственными. Двойственными называются и взаимозаменяемые операции  и , а также кванторы  и .


Теорема 9.3.4. Пусть А – формула алгебры предикатов p1, …, ps суть все различные элементарные формулы в А, т. е.:


A = A(p1, …, ps)


Тогда имеет место равносильность формул:

A*( p1, …, ps ) = A(p1, …, ps ).


Доказательство. Докажем теорему индукцией по рангу r формулы А. При r = 0 ее утверждение верно. Допустим, что оно верно для любой формулы ранга r < n и пусть r(A) = n+1.

Возможны 5 случаев:


A = A1  A2, A = A1 v A2, A = xA1, A = xA1, A =A1.

  1. A = A1  A2. Тогда, используя предположение индукции, закон де Моргана 11 и общие свойства равносильности, получим:



A*( p1, …, ps ) = A1*( p1, …, ps ) v A2*( p1, …, ps ) 

 A1 ( p1, …, ps ) v A2( p1, …, ps )  A ( p1, …, ps ).


В трех следующих случаях рассуждения аналогичны. Вместо равносильности 11 в них используются соответственно равносильности 12, 20, 21. В последнем случае утверждение теоремы следует непосредственно из предположения индукции. Теорема доказана.


Следствие 9.3.5. (Принцип двойственности.) Для любых формул А, В алгебры предикатов:

A  B  A*  B*

Принцип двойственности позволяет вместо двух равносильностей A  B и A*  B* доказывать лишь любую одну из них.


§ 9.4. ^ Использование равносильностей для упрощения формул.


Равносильности 1-26 зачастую используются также для преобразования формул к равносильным им формулам нужного вида.

В качестве примеров рассмотрим преобразование формул алгебры предикатов к так называемым приведённым и предваренным формулам.

Определение 9.4.1. Формула алгебры предикатов называется приведенной, если в ней не используется операция ->, а отрицание или не используется совсем, или относится лишь к элементарным формулам.

Определение 9.4.2. Предваренной (или нормальной, или пренексной) формулой алгебры предикатов называется любая формула вида


δ1xi1δ2xi2…δkxik A, (1)


где δ1, …, δk – кванторы, а А приведенная формула, не содержащая кванторов.


Теорема 9.4.3. Для всякой формулы А алгебры предикатов существует равносильная ей приведенная формула. Докажем теорему индукцией по рангу r(А) формулы А. Если r(А) = 0, то утверждение верно. Пусть r(А) > 0. Тогда по определению формулы А совпадает с одной из формул вида


A1  A2, A1 v A2, δxA1, A1 -> A2, A1 (2)


^ По предположению индукции формулы А1, А2 равносильны приведенным формулам. Заменив ими в (2) формулы А1, А2, мы в трех первых случаях сразу получим приведенные формулы. А так как A1->A2А12 (см. равносильность 24), то остается рассмотреть случай, когда A =A1. Если А1 – элементарна, то А – приведенная формула. Если же А1 не элементарна, то она может иметь вид


B1  B2, B1 v B2, δxB1, B1 -> B2, B1,


где r(Bi) < r(A) - 2. Тогда по свойствам равносильности 11, 12, 20, 21, 24, 14 формула А равносильна одной из формул:


B1 v B2, B1 B2, δ*xB1, B1 vB2, B1 (3)


Остается применить предположение индукции к формулам B1,B1,B2 и заменить их в (3) приведенными формулами.


Теорема 9.4.4. Для всякой формулы а алгебры предикатов существует равносильная ей предваренная формула.


Доказательство. По теореме 9.4.3, не теряя общности, можно считать, что А – приведенная формула. Снова применим индукцию по r(А). Для r(А) =0 утверждение верно. Пусть r(А) > 0. Тогда формула А может иметь вид


1) A1  A2, 2) A1 v A2, 3) δxA1, 4) A1


Причем в случае 4 А1 – элементарная формула и для нее утверждение теоремы верно. Рассмотрим случаи 1-3.


1. A = A1  A2. По предположению индукции Аi равносильна предваренной формуле Bi, i = 1,2, причем согласно равносильности 26 связанные переменные любой из формул В1, В2 можно считать отличными от всех переменных другой формулы. Таким образом, A = B1  B2, где можно считать


B1 = δ1x1…δkxkC1, B2k+1xk+1…δnxnC2


x1, …, xk не входят в С2, xk+1,…,xn не входят в С1, и формулы С1, С2 не содержат кванторов. Отсюда, используя равносильность 25, получим


Aδ1x1…δkxkδk+1xk+1…δnxn(C1  C2).


2. A = A1 v A2, рассуждения двойственны.


3. A = δxA1. По предположению индукции А1 равносильна приведенной формуле


A  δ1x1…δkxkB (4)


причем можно считать, что x  x1, …, xk. Возможны два подслучая:

а) В содержит свободные вхождения х. Тогда А равносильна предваренной формуле


δxδ1x1…δkxkB;

б) В не содержит свободных вхождений х. Тогда из равносильности 4 следует, что значения формулы А1 не зависят от значений переменной х, а потому АА1 и теорема доказана.


§9.5. Построение исчисления предикатов.


1. Язык исчисления предикатов.


В качестве алфавита исчисления предикатов возьмем то же самое множество

Ҩ = σ U X U O

которое служило алфавитом при определении формул алгебры предикатов. За элементами множества σ, Х и О сохраним те же самые обозначения и названия, хотя здесь на все буквы алфавита Ҩ мы должны пока смотреть просто как на символы, не имеющие какого-либо содержательного смысла. Например, символ операции f здесь не обозначает какую-либо конкретную операцию, определенную на каком-либо конкретном множестве. То же относится и к символам предикатов. Термины же «символ операции» и «символ предиката» объясняются тем, что в приложениях исчисления предикатов к конкретным математическим теориям мы будем трактовать их (интерпретировать) как операции и предикаты на конкретном множестве. Аналогично, предметным переменным будут придаваться значения из этого множества.

Понятия терма и формулы сигнатуры σ в исчислении предикатов определяются буквально так же, как в алгебре предикатов.

Равенство формул, как и в алгебре предикатов, будем обозначать знаком =.

Из множества всех формул ниже особую роль будут играть формулы, не содержащие свободных вхождений предметных переменных. Они называются замкнутыми формулами, или предложениями.

Таким образом, нами полностью определен язык исчисления предикатов 1-й ступени сигнатуры σ. Обозначим его буквой α. При формул языка α будут использоваться те же правила сокращения скобок, что и в алгебре предикатов.

Заметим, что кроме исчисления предикатов 1-й ступени в математической логике и в теории моделей рассматриваются исчисления предикатов и логические языки 2-й ступени. В их алфавиты кроме перечисленных выше символов вводятся также символы функциональных и предикатных переменных и кванторы ,  могут навешиваться не только на предметные переменные, но и на функциональные переменные и предикатные переменные.


2.Аксиомы и правила вывода исчисления предикатов.


При построении исчисления предикатов с определенным выше языком α аксиомы и правила вывода могут выбираться по-разному. Мы выберем следующую систему аксиом. Аксиомы этой системы по используемым в них логическим операциям делятся на 5 подсистем, которые мы занумеруем римскими цифрами. В подсистемах l - lV под буквами А, В, С понимаются произвольные формулы языка α, ограничения на формулы системы V указываются в формулировках соответствующих аксиом.

  1. 1) A->(B->A)

2) (A->(B->C))->((A->B)->(A->C))

  1. 1) AB->A
  1. 2) AB->B
  2. 3) (A->B)->((A->C)->(A->BC))


lll. 1) A->AvB

2) B->AvB

3) (A->C)->((B->C)->(AvB->C))



IV. 1) A->A



2) A->A

3)(A->B)->(B->A)


V. 1)x A(x)->A(t)

2) A(t)->x A(x).


где A(x) – формула, содержащая свободные вхождения переменной х, A(t) – формула, полученная заменой в A(x) всех свободных вхождений x термом t, удовлетворяющим условию: ни одно свободное вхождение х в A(x) не находится в области действия квантора по какой-либо переменной, содержащейся в t (при этом условии говорят, что терм t свободен для х в формуле A(x)) (далее аксиомы будут обозначаться римскими цифрами с индексами. Например, ll3 – аксиома 3 из подсистемы ll).

Сформулируем теперь правила вывода. Каждое такое правило позволяет из некоторого множества исходных формул получать новую формулы. Поэтому правило вывода записывают обычно в виде «дроби», у которой в «числителе» находятся исходные формулы, а в «знаменателе» – вновь получаемая формула.


l. Правило заключения:

A, A ->B ,

B

где А, В – любые формулы языка α.

ll. Правило -введения:

B -> A ,

B->xA

где А содержит , а В не содержит свободные вхождения переменной х.

lll. Правило -удаления:

A -> B ,

x A->B

где А, В – формулы, удовлетворяющие тем же условиям, что и в правиле ll.

Формула, находящаяся в «знаменателе» правила вывода, называется непосредственным следствием формул «числителя».

Заметим, что, подставляя в аксиому l1 вместо А, В произвольные формулы, мы получим бесконечное множество формул. Таким образом, запись аксиомы l1 является, по существу, схемой, по которой можно получать формулы. То же можно сказать об остальных аксиомах и о формулах из правил вывода.

Определив язык α и аксиомы с правилами вывода, мы определили тем самым логическое исчисление, называемое исчислением предикатов 1-й ступени сигнатуры σ. Меняя σ, т. е. меняя множество формул и сохраняя схемы аксиом и правил вывода, мы будем получать другие исчисления предикатов. В дальнейшем язык α будем считать фиксированным и соответствующее логическое исчисление будем обозначать той же буквой α.


§ 9.6. Выводимость и доказуемость формул.


Определение 9.6.1. Выводом формулы А из конечного или бесконечного множества формул Т в исчислении α называется конечная последовательность формул

А1, А2, …, An, ___

в которой An = A и каждая из формул Ai, i 1, n является или аксиомой, или формулой из Т (исходной формулой), или получается по некоторому правилу вывода из предыдущих формул последовательности (1).

Если существует вывод формулы А из множества формул Т исчисления α, то говорят, что в α А выводима из Т и пишут


Т ├─ А, или В1, В2, …, ВК ├─ А,

α α

если Т = {В1, В2, …, ВК}. При этом формулы из Т называют посылками вывода.

Особо важным является случай, когда Т – пустое множество.


Определение 9.6.2. Формула из А языка α , выводимая в исчислении α из пустого множества формул, называется доказуемой формулой, или теоремой исчисления α, а сам вывод формулы А из пустого множества формул называется ее доказательством. Если формула А доказуема в исчислении α, то пишут

├─ А.

α

Так как у нас исчисление α фиксировано, то букву α будем опускать и писать просто


Т ├─ А; В1, В2, …, ВК ├─ А; ├─ А.


Очевидно, что при выводах и доказательствах формул можно использовать не только аксиомы и исходные формулы, но и любые доказанные ранее формулы.

Дальше нас будут интересовать вопросы о характеризации доказуемых формул и формул, выводимых из заданного множества, вопросы о непротиворечивости и полноте исчисления α. Предварительно приведем доказательства некоторых формул и вспомогательных правил вывода. При этом последовательности формул, являющиеся доказательствами или выводами, будем записывать в столбик, указывая справа их происхождение (номер аксиомы, номер правила вывода, порядковые номера исходных формул и т. п.).


Теорема 9.6.3. ├─ А -> А для любой формулы А.

Доказательство.

1) (А->((В->А)->А))->((А->(В->А))->(А->А)), (l2)

2) А ->((В->А)->А) , (l1)

3) (А->(В->А))->(А->А), (l, 1, 2)

4) А-> (В->А), (l1)

5) А->А. (1, 3, 4)


Теорема 9.6.4. Если А – любая формула и В – доказуемая формула, то ├─ А->В.

Доказательство получается и добавлением к доказательству формулы В аксиомы l1 и формулы А->В, получаемой из В и аксиомы l1 по правилу l.


Теорема 9.6.5. ├─ АВ -> ВА для любых формул А, В.

Доказательство.

1) (АВ->В)->((АВ->А)->(АВ->ВА)), (ll3)
  1. АВ->В, (ll3)
  2. (АВ->А)->(АВ->ВА), (l, 1, 2)

4) АВ->А, (ll1)

5) АВ->ВА.


Заменяя в доказательстве теоремы 9.6.5 ll1 ll3 соответственно аксиомами lll1-lll3, получим доказательство следующей формулы.


Теорема 9.6.6. ├─ АВ -> ВА для любых формул А, В.

______ ___

Теорема 9.6.7. ├─ x A(x) ->-x A(x) для любой формулы А(х), содержащей свободные вхождения переменной х.

Доказательство.

  1. А(х)-> х А(х), (V2)

______ ___

2) (А(х)->х А(х))->(х А(х)->А(х)) (lV3)

______ ___

3) x А(x) ->А(x) (l, 1, 2)

______ ___

4) x А(x) -> x А(x) (l, 1, 3)


Даже из приведенных простейших примеров видно, что задача построения доказательств формул является сложной и зачастую весьма искусственной. То же относится и к построению выводов. Попытайтесь, для примера построить вывод


AC ->D ├─ A -> (C->D).


Для облегчения этой работы сначала доказывают ряд вспомогательных правил вывода, которыми затем можно заменять целые куски выводов или доказательств.

Ряд наиболее распространенных вспомогательных правил вывода можно получить из так называемой теоремы дедукции. Однако и ее формулировка и доказательство в общем случае сложны. Мы пока один ее ослабленный вариант.

Теорема об ограниченной дедукции. Пусть Т – произвольное множество формул, и А, В – произвольные формулы. Если

T, A├─ B (2)

и существует вывод формулы В из T U {A}, в котором не используются правила -введения и -удаления, то


T ├─ A -> B. (3)

Доказательство. Пусть

В1, В2, …, Вm = B

есть вывод формулы В из T U {A}, в котором не используются правила -введения и -удаления. Докажем утверждение (3) индукцией по длине вывода m.

Пусть m=1. Тогда В является или аксиомой, или посылкой. Если В – аксиома, то она, очевидно, доказуема, и по теореме 9.6.4 имеем ├─ A -> B для любой формулы А. Отсюда и следует (3). Пусть В – посылка. Если В=А, то (3) следует из теоремы 9.6.3. Если же ВТ, то можно указать следующий вывод формулы А->В из Т:
  1. В->(А->В), (l1)
  2. В, (посылка)

3) А->В (l, 1,2)


Допустим, что теорема верна при m < n, и докажем ее для m = n + 1. В этом случае по условию формула В будет или аксиомой, или посылкой, или непосредственным следствием двух предыдущих формул Bi, BJ по правилу заключения. Если В – аксиома или посылка, то (3) устанавливается точно так же, как и при m=1. Пусть В получается из Bi, BJ по правилу заключения, т. е. BJ = Bi -> B. Так как i<n, j<n, то по предположению индукции имеем:

T├─ A -> Bi, T├─ A -> (Bi ->B).

Применяя теперь к формулам

A->( Bi ->B), A-> Bi

и к аксиоме l2

(A->( Bi ->B))->((A-> Bi)->(A->B))

дважды правило заключения, получим формулу А->В. Теорема доказана.

Докажем теперь ряд вспомогательных правил вывода, обозначая в них буквами А, В, С произвольные формулы α.

Правило умножения формул:

A, B ├─ AB.

Вывод.
  1. ^ (A->A)->((A->B)->(A->AB)) (II3)
  2. A->A (теорема 1)
  3. (A->B)->(A->AB) (I, 1, 2)
  4. B->(A->B) (I1)
  5. B (посылка)
  6. A->B (I, 4, 5)
  7. A->AB (I, 3, 6)
  8. A (посылка)
  9. AB . (I, 7, 8)

Правило силлогизма:

^ A->B, B->C├─ A->C.

Согласно теореме дедукции достаточно показать, что

A->B, B->C, A├─ C,

причем существует вывод С, не использующий правил -введения и -удаления. Таким выводом может служить последовательность формул:

А, А->В, В, В->С, С.

Для ее получения дважды применяется правило заключения к посылкам. Аналогично доказываются следующие правила.

Правило умножения посылок:

A->(B->C)├─ AB ->C.

Правило разделения посылок:

^ AB->C ├─ A ->(B->C).

Правило перестановки посылок:

A->(B->C)├─ B->(A->C).

Правило умножения заключений:

A->B, A->C├─ A->BC.

Правило сложения посылок:

A->C, B->C├─ A v B->C.

Правило введения посылки:

A├─ B->A.

Правило контрапозиции:

A->B├─ B->A.

Правило де Моргана:

_ _ __ ___ _ _

a) A v B ├─ AB, б) АВ ├─ A v B


а) Вывод:

  1. AB->A (ll1)



  1. AB->B (ll2)

_ __
  1. A->AB (правило контрапозиции, 1)

_ __
  1. B->AB (правило контрапозиции, 2)

_ _ __
  1. A v B->AB (правило сложения посылок, 3, 4)

_ _
  1. A v B (посылка)

__
  1. AB (1, 5, 6)


б) Вывод:

_ _ _
  1. A->A v B (lll1)

_ _ _
  1. B->A v B (lll2)

─── ─
  1. A v B ->A (правило контрапозиции, 1)

─── ─
  1. A v B ->B (правило контрапозиции, 2)


  1. A->A (IV2)


  1. B->B (IV2)

──
  1. A v B->A (правило силлогизма, 3, 5)

──
  1. A v B->B (правило силлогизма, 4, 6)

──
  1. A v B->AB (правило умножения заключений, 7, 8)

__ ────
  1. AB->A vB (правило контрапозиции, 9)


───── ­_ _
  1. A v B -> A v B (IV2)

__ _ _
  1. AB->A v B (правило силлогизма, 10, 11)


Правило -отрицания:

_____ ___

а) x A(x)├─ x A(x)

(следует непосредственно из теоремы 9.6.7);

___ _____

б) x A(x)├─ x A(x)

Вывод:

___ ___
  1. x A(x)->A(x) (V1)

─── ───
  1. A(x) ->x A(x) (правило контрапозиции, 1)

──
  1. A(x) -> A(x) (IV1)

─────
  1. A(x) -> x A(x) (правило силлогизма, 2, 3)

────
  1. x A(x)-> x A(x) (lll, 4)

═════ ────
  1. x A(x) ->x A(x) (правило контрапозиции, 5)

___ ═════
  1. x A(x) -> x A(x) (IV1)

___ ______
  1. x A(x) ->x A(x) (правило силлогизма, 6, 7)



Правило -отрицания:

______ ___ ___ ______

а) x A(x) ├─ x A(x); б) x A(x)├─ x A(x).

Докажите в качестве упражнения.


Правило противоречия:

АА ├─ В (из противоречия выводима любая формула).


Распишем вывод произвольной формулы В из АА, используя при этом любую доказуемую формулу R, например, А->А.

  1. A->(R->A) (l1)



  1. ^ (R->A)->(A->R) (IV3)



  1. A->(A->R) (правило силлогизма, 1, 2)



  1. AA -> R (правило умножения посылок, 3)



  1. B->R ( теорема 2)

_
  1. R->B (правило контрапозиции, 5)


  1. AA ->B (правило силлогизма, 4, 6)


  1. B->B (IV2)



  1. AA->B (правило силлогизма, 7, 8)



  1. AA (посылка)



  1. B (1, 9, 10)



Правило (закон) исключенного третьего:

├─ A vA.


Доказательство (снова используем доказуемую формулу R).
  1. A->AvA (lll1)



  1. A->AvA (lll1)

_____
  1. A v A->A (правило контрапозиции, 1)

_____ _
  1. A vA->A (правило контрапозиции, 2)


  1. AvA->A (IV1)

_____
  1. A vA->A (правило силлогизма, 4, 5)

_____
  1. A vA->AA (правило умножения заключений, 7, 8)



  1. AA->R (правило противоречия и теорема дедукции )

____
  1. A vA ->R (правило силлогизма, 7, 8)



═ ═══
  1. R-> A vA (правило контрапозиции, 9)


  1. R->R (IV1)

════
  1. R->A vA (правило силлогизма, 10, 11)

════
  1. A vA->A vA (IV2)



  1. R->A vA (правило силлогизма, 12, 13)



  1. R (теорема)



  1. A vA (1, 14, 15)



Воспользуемся вспомогательными правилами вывода для доказательства еще одного частного случая теоремы дедукции.

Теорема дедукции (для замкнутой формулы). Если Т произвольное множество формул, В – произвольная, А – замкнутая формулы и

T, A├─ B,

то

T├─ A->B.

Доказательство производится так же, как теоремы об ограниченной дедукции. В дополнение нам необходимо лишь рассмотреть два случая (при m = n + 1):

а) В получается по правилу -введения из формулы Bi;

б) В получается по правилу -удаления из формулы Bi.


В случае «а» имеем:

Bi = C->D(x), B = C->x D(x),

причем С не содержит свободных вхождений х. По предположении индукции имеем:

T├─ A->(C->D(x)).

Дополним вывод формулы A->(C->D(x)) следующими формулами до вывода формулы А->В:

AC-> D(x) (правило умножения посылок)

AC->x D(x) (правило -ввведения)

A->(C->x D(x)) = A->B (правило разделения посылок)

В случае «б»:


Bi = C(x) -> D, B =  x C (x) ->D,


где D не содержит свободных вхождений х. По предположению индукции

T├─ A->(C(x)->D).

Отсюда, используя правила перестановки посылок и -удаления, получим:


T├─ C(x)->(A->D)

T├─ x C(x)->(A->D)

T├─ A->(x C(x) ->D) = A->B.

Теорема доказана.

Укажем одно следствие теоремы дедукции.

Следствие. Если Т – любое множество формул, А – замкнутая, В – любая формулы и

T, A ├─ BB

то

T ├─ A. (4)

Доказательство. По теореме дедукции


T ├─ A -> BB.

Применяя правило контрапозиции, получим

___

T├─ BB -> A. (5)

Из правила де Моргана «а» и закона исключенного третьего следует, что

___

├─ BB (6)

Для любой формулы В. Из (5), (6) следует (4).


§9.7. Семантика исчисления предикатов.


Для уяснения содержательного смысла аксиом и правил вывода введем понятие интерпретации языка и исчисления α.

Определение 9.7.1. Под интерпретацией языка исчисления α понимают любое множество М с зафиксированным отображением  сигнатуры σ во множество операций и предикатов, определенных на М, при котором символу n-арной операции f из σ соответствует n-арная операция f, определенная на множестве М, а символу n-арного предиката р из σ n-арный предикат р на М. Образ множества σ при отображении  обозначим через σ. В частности, образом констант из σ при  будут нуль-арные операции на М, т. е. некоторые элементы из М.

Если (М, ) – интерпретация языка α, то, заменив в любой формуле языка α константы, символы операций и символы предикатов их образами при  и условившись переменным из Х придавать значения из множества М, мы получим формулу А алгебры предикатов на алгебраической системе М(σ), и можно говорить о выполнимости, истинности или ложности этой формулы на системе М(σ).

Определение 9.7.2. Формула А исчисления предикатов называется выполнимой, истинной, ложной в интерпретации (М, ), если соответственно выполнима, истинна, ложна формула А на алгебраической системе М(σ).

Определение 9.7.3. Формула А исчисления предикатов α называется тождественно истинной, если она истинна во всех интерпретациях исчисления α.

Естественно возникает вопрос о соотношении между классами доказуемых и истинных формул исчисления предикатов. Ответ на этот вопрос можно получить из следующих теорем.

Теорема 9.7.4. Если каждая формула множества формул Т истинна в некоторой интерпретации (М, ) исчисления α и T├─ A, то А – истинна в (М, ).

Доказательство. Для простоты записей условимся считать, что операции и предикаты на М обозначены теми же буквами, что и соответствующие им символы операций из σ. Тогда  - тождественное отображение и в записи А индекс  можно опускать.

Из определения доказуемой формулы следует, что достаточно делать два утверждения:

а) все аксиомы – истинны;

б) формула, являющаяся непосредственным следствием по любому правилу вывода из истинных формул, является истинной.

Истинность аксиом первых четырех групп аксиом доказывается одним методом. Проиллюстрируем его на аксиоме

I1: A -> (B->A).

Заменив в А, В свободные вхождения переменных элементами из М, получим высказывания, имеющие вполне определенные значения £ и ß (каждое из £, ß есть «и» или «л»). Перебирая всевозможные наборы значений «и» и «л» для £, ß мы непосредственной проверкой (пользуясь определением операции ->) убедимся в том, что при любых £ , ß

£ -> (ß->£)= и.

Отсюда следует, что аксиома l1 истинна в интерпретации (М, ).

Докажем теперь истинность аксиомы

V1 : x A(x) -> A(t),

где t – терм, свободный для х в А(х). Пусть х, х1, …, хn суть все переменные, имеющие свободные вхождения в А(х) и xi1, …, xim – все переменные, участвующие в образовании терма t. Так как t свободен для х в А(х), то все вхождения переменных xi1, …, xim в терм t останутся свободными при подстановке t вместо х в формулу А(х). В связи с этим запишем:

A(t) = A(t (xi1, …, xim), х1, …, хn).

Допустим, что формула V1 не истинна в интерпретации (М, ). Это означает, что при некотором наборе значений переменных х1=a1, …, хn=an, xi1=ai1, …, xim=aim формула x A(x) принимает значение «и», а формула A(t) – значение «л». Если обозначить через b значение терма t при xi1=ai1, …, xim=aim, то будем иметь: с одной стороны, A(х0, a1, …, an) является истинным высказыванием при любом значении х0М, а с другой стороны, высказывание A(b, a1, …, an) - ложно. Полученное противоречие и доказывает наше утверждение.

Аналогично доказывается, что правила вывода позволяют из истинных формул в интерпретации (М, ) получать снова истинные формулы, т. е.:
  1. если истинны формулы А и А->В, то истинна и формула В;
  2. если истинна формула В->А(х) и х не имеет свободных вхождений в В, то истинна формула В -> х А(х);
  3. если истинна формула А(х)->В и х не имеет свободных вхождений в В, то истинна и формула х А(х) -> В.

Теорема доказана.

Следствие 9.7.5. Всякая доказуемая формула исчисления предикатов α является истинной в любой интерпретации (М, ) исчисления α.

Замечание. Теорема и следствие теряют силу, если в аксиомах V1 и V2 не накладывать ограничений на терм t или в правилах -введения и -удаления разрешить свободные вхождения х в В. Приведем соответствующие примеры.

1. Пусть множество натуральных чисел N, A(x) = y (x < y) и t = x + y – терм, не свободный для х в А(х), поскольку свободное вхождение буквы х в А(х) находится в области действия квантора  по букве у, входящий в терм t.

Нетрудно видеть, что формула

x A(x) ->A(t),

или подробнее,

x (y(x y (x + y
ложна в арифметике.
  1. В той же интерпретации, положим B = ( x < y ), A = (x < y +1) .

Тогда имеем: формула В->А истинна на N, а формула В -> xА ложна, поскольку, например, при х=2, у=3 имеем

(2<3)  и, x (x < 4)  л.

Доказанная теорема свидетельствует о том, что логические средства исчисления предикатов выбраны разумно, поскольку с помощью их можно доказать только утверждения, истинные с содержательной точки зрения.

Следствие 9.7.6. Исчисление предикатов непротиворечиво, т.е. в нем не может быть доказуемой никакая формула А вместе с ее отрицанием, или никакая формула вида АА.

Действительно формула АА является ложной в любой интерпретации, тогда как доказуемые формулы истинны в любой интерпретации.

Теперь естественно возникает вопрос: не слишком ли мало аксиом и правил вывода мы взяли при построении исчисления предикатов? Так, из доказательства предыдущей теоремы видно, что если бы нашлась формула А, не доказуемая в исчислении предикатов, но истинная в любой его интерпретации, то, присоединив А к системам аксиом, мы получили бы более сильное и непротиворечивое логическое исчисление. Однако ниже будет показано, что такой формулы А не существует, а именно имеет место следующая теорема Геделя о полноте исчисления предикатов.

Теорема 9.7.7. Если формула исчисления предикатов истинна во всех его интерпретациях, то она доказуема в исчислении предикатов.

Для доказательства этой теоремы введем сначала некоторые понятия М докажем одно общее утверждение (см. теорему 9.7.11).

Определение 9.7.8. Множество формул Т исчисления α называется противоречивым, если существует такая формула А языка α, что

Т├─ АА.

В противном случае Т называется непротиворечивым.

Определение 9.7.9. Множество формул Т исчисления α называется выполнимым, если существует интерпретация, в которой все формулы из Т принимают истинное значение хотя бы при одной (общей для всех формул из Т) замене переменных.

Определение 9.7.10. Множество формул Т исчисления α называется полным, если для каждой замкнутой формулы языка α имеет место

Т├─ А или Т ├─ А.

Теорема 9.7.11. Всякое непротиворечивое множество S замкнутых формул исчисления α выполнимо.

Доказательство. Добавим к множеству символов языка α еще счетное множество констант (символов нуль-арных операций)

ß = {b0, b1, b2, …} .

Получим новый язык α1 в сигнатуре σ1 = σ U ß. Заменяя в аксиомах и правилах вывода исчисления α формулы языка α1, мы получим новое логическое исчисление, которое обозначим той же буквой α1. Из определения языка α1 видно, что все доказанные факты об исчислении α (в частности, все доказанные формулы и дополнительные правила вывода) сохраняются и в α1. Так как язык α1 включает в себя α, то S можно рассматривать как множество предложений языка α1. Легко видеть, что S будет непротиворечивым и в исчислении α1. Действительно, если в α1 из S выводима формула АА, то, заменив в формулах вывода АА из S все константы из ß переменными, не участвующими в этом выводе, мы получим вывод в α из S формулы ВВ , где В получается из А указанной заменой констант. Чтобы убедиться в этом, достаточно заметить, что указанная замена аксиомы переводит в аксиомы и сохраняет свойство формулы быть непосредственным следствием предыдущих формул. Таким образом, S непротиворечиво в α1.

Теперь расширим определенным образом множество S. Для этого занумеруем все замкнутые формулы исчисления α1:

А0, А1, А2, …

По формуле А0 и системе S построим множество формул S0, положив:

 S U { А0 }, если S├─ А0

S0 =  S U { А0 }, если S├┼ А0 и А0  х В0 (х)

 S U { А0, B0, (bi0)}, если S├┼ А0 и А0 = х В0 (х),


где знаком ├┼ обозначено отрицание выводимости, а bi0 – символ с наименьшим номером из ß, не встречающийся в А0. Из определения S0 имеем:

S  S0 и S0 ├─ А0 или S0 ├─ А0

Покажем, что юю непротиворечиво. Допустим, что в α1

S0 ├─ ВВ

В соответствии с определением S0 рассмотрим три случая.

А) S ├─ А0. Тогда S0 = S U { А0 } и из (2) имеем:


S, А0 ├─ BB.


Отсюда по следствию из теоремы дедукции получаем



S ├─ А0, что невозможно в силу непротиворечивости S.


Б) S├┼ А0 и А0 не имеет вида х В0(х). Тогда S0 = S U {

А0} и мы точно так же, как и в случае «а», получим S ├─



А0, что противоречит условию.


В) S├┼ А0 и А0 = х В0 (х).

Тогда S0 = S U { А0, B0, (bi0)} , и потому

S, А0, B0, (bi0) ├─ ВВ.


Так как формула B0 (bi0) замкнута, то тем же приемом, что и выше, получим

______

S, А0 ├─ B0 (bi0).

Так как bi0 не входит в А0 и в формулы из S, то, повторив весь вывод с заменой bi0 на переменную xJ, не входящую в участвующие в выводе формулы, мы получим

_____ _____

S, А0 ├─ B0 (xJ), или S ├─ А0 -> B0 (xJ).

______

Дополним вывод А0 -> B0, (xJ) из S формулами:

______

А0 ->  xJ B0 (xJ) (правило -введения)

_____ _____

 xJ B0, (xJ) -> B0 (xJ) (аксиома)

_____

А0 -> B0 (x) (правило силлогизма)

____

А0 ->  x B0 (x) (правило -введения)

____ _______

 x B0 (x) ->  x B0 (x) (правило -отрицания)

_______

А0 ->  x B0 (x) (правило силлогизма)


Поскольку  x B0 (x) = А0, то мы получили вывод из S формулы А0 -> А0, т. е. S, А0 ├─ А0. А так как S, А0 ├─ А0, то по правилу умножения формул S, А0 ├─ А0А0. Отсюда следует S├─ А0, и мы снова пришли к противоречию с условием. Тем самым мы закончили доказывать непротиворечивость множества формул S0.

Далее, по А1 и S0 мы аналогично построим непротиворечивое множество S1, такое, что:

S0  S1, S1 ├─ А1 или S1 ├─ А1.

Продолжая этот процесс, мы получим последовательность непротиворечивых множеств формул

S0  S1 S2 …, 

таких, что Si ├─ Аi и Si ├─ Аi. Следовательно, T = U Si есть непротиворечивое и полное множество формул. i = 0

Теперь построим интерпретацию исчисления предикатов α, в которой истинны все формулы из α. В качестве основного множества возьмем множество М термов языка α1, в которых нет предметных переменных – это так называемые замкнутые термы языка α1. Определим на М операции f и предикаты р, соответствующие символам операций f и предикатов р из α.

Если а – символ 0-арной операции из σ, то положим а=а. Если f – символ n-арной операции из σ, p – символ n-арного предиката и t1, …, tn – термы из М, то положим


f (t1, …, tn)=f(t1, …, tn)


и, если Т ├─ р(t1, …, tn)

p (t1, …, tn)= 

л, если Т ├─ р(t1, …, tn)


Тем самым определена интерпретация (М, σ) исчисления α1, а потому и α.

Теперь индукцией по рангу формулы А докажем, что для любой замкнутой формулы языка α1:

Т├─ А в α1  А  и в (М, σ). (3)

Для упрощения записи верхний индекс  у формул будем опускать.

Если А = р(t1, …, tn) – элементарная формула, то (3) верно по определению предиката р.

Пусть А – замкнутая формула ранга r > 0. В зависимости от последней операции в А возможны 6 случаев.
  1. А = А1А2. Используя определение конъюнкции, предположение индукции и правила умножения и разделения формул, получим:

А  и А1 = и, А2 = и Т├─ А1 ,Т├─ А2 Т├─ А1А2.
  1. А = А1  А2. Если А1  А2 и, то А1 = и или А2 = и. Тогда по предположению индукции Т├─ А1 или Т├─ А2, а поэтому и Т├─ А1  А2. Обратно, пусть Т├─ А1  А2. Если Т├─ А1 или Т├─ А2, то по предположению индукции А1  и или А2  и, а потому и А  и. В противном случае в силу полноты системы Т имеем:

Т├─ А1 ,Т├─ А2

Тогда по правилам умножения формул и де Моргана получим:

_____

Т├─ А1А2, Т├─ А1  А2

Итак, имеем: _____

Т├─ А1  А2, Т├─ А1  А2

что невозможно в силу непротиворечивости Т.
  1. А = А1. Учитывая предположение индукции и полноту системы формул Т, получим:

А  и А1  л Т├─ А1 Т├─ А.
  1. А = А1->А2. В этом случае, используя предположение индукции и правила введения посылки, контрапозиции и двойного отрицания, получим:

А  и А1  л или А2  и Т├─ А1 ,

или Т├─ А2 Т├─ А2 -> А1 или Т├─ А2 -> А1 Т├─ А.
  1. А=х А1(х). Если А  и, то А1(t)и при любом tM. Тогда по предположению индукции Т├─ А1(t) для всех tM. Допустим, что

______ ___

T ├─ х А1(х). Тогда по правилу -отрицания T ├─ х А1(х) и по

____

построению множества Т в Т существует формула А1(b) при некоторой константе bM. В итоге мы получили:


Т├─ А1(t) при любом tM и Т├─ А1(b) при bM,


что невозможно в силу непротиворечивости Т. Следовательно, T ├─ х А1(х).

Обратно, пусть T ├─ х А1(х). Если х А1(х)и, то А1(t)л при некотором tM. Тогда по предположению индукции ___

Т├─ А1(t).

Отсюда по аксиоме V2 и по правилу -отрицания получим

____ _______

T ├─ х А1(х) и T ├─ х А1(х),

что невозможно в силу непротиворечивости Т.
  1. А = х А1(х). Если А  и, то А1(t)и при некотором tM и по предположению индукции Т├─ А1(t). Отсюда, используя аксиому V2, получим T ├─ х А1(х), т. е. Т├─ А.

Обратно, если Т├─ А, то в силу непротиворечивости Т имеем Т├┼ А. Тогда по построению Т в Т содержится формула А1(b) при некотором bM. По предположению индукции А1(b)и, а потому и х А1(х)=и.

Таким образом, все замкнутые формулы языка α, выводимые из Т, истинны в интерпретации (М, ). А так как ST, то и все формулы из S истинны в (М, ), т. е. множество S выполнимо и теорема доказана.

Теперь можно доказать и теорему Гёделя о полноте исчисления α.

Пусть А – формула исчисления предикатов α и А  и в любой интерпретации исчисления α. Если х1, …, хn суть все переменные, имеющие свободные вождения в А, то формула В = х1, …, хnА также истинна в любой интерпретации α, а потому формула В ложна в любой интерпретации α. Отсюда следует, что множество формул {B} невыполнимо.

Тогда по теореме о выполнимости множество {B} противоречиво, т. е. существует формула С языка α, такая, что

B ├─ CC.

Но тогда по следствию из теоремы дедукции ├─B. Теперь, применяя n раз аксиому V1 и правило заключения, получим ├─A, что и доказывает теорему Гёделя.

В качестве других следствий теоремы о выполнимости докажем так называемую теорему о совместной выполнимости и локальную теорему Мальцева.

Теорема (о совместной выполнимости). Если замкнутая формула А исчисления α истинна в любой интерпретации α, в которой истинны формулы некоторого Т замкнутых формул, то Т├─ А.

Доказательство. Из условия видно, что множество формул Т’ = Т U{A} невыполнимо. Значит, по теореме о выполнимости множество T’ противоречиво, т. е. T, A├─ BB для некоторой формулы В. Отсюда по следствию из теоремы дедукции Т├─ А.

Теорема Мальцева. Множество замкнутых формул S исчисления α выполнимо тогда и только тогда, когда выполнимо любое его конечное подмножество.

Доказательство. Выполнимость конечных подмножеств выполнимого множества формул очевидна. Докажем обратное утверждение. Допустим, что выполнимо любое конечное подмножество формул множества S, а само S невыполнимо. Тогда по теореме о выполнимости оно противоречиво, т. е. найдется такая формула А, что S├─ AA.

Но тогда AA выводима лишь из конечного подмножества S1 S формул, участвующих в выводе формулы AA из S. Следовательно, нашлось противоречивое конечное множество формул из S. Если бы S было выполнимым, то по теореме 9.7.4 нашлась бы интерпретация α, в которой была бы истинной формула AA, что невозможно. Полученное противоречие и доказывает теорему.