Замятин, задачник по матлогике

другой стороны, известно, что аксиома ( x)G(x) → G(w) тождественно истинна. Посылка этой аксиомы истинна при интерпретации ϕ. Следовательно, ϕ(G(w)) = 1. Полученное противоречие показывает, что формула ( x)G(x) принадлежит P.

( )Пусть ( x)G(x) P. Надо доказать, что ϕ[( x)G(x)] = 1. Как а в части «туда» здесь удобно рассуждать от противного. Предположим, что ϕ[( x)G(x)] = 0. Тогда существует интерпретация ϕ′ I(ϕ, x) такая, что ϕ′(G(x)) = 0. Вспомним, наконец, что областью определения интерпретации ϕ является множество термов T. Следовательно, ϕ′(x) − это некоторый терм. Обозначим его через t.

Если подстановка t вместо x в формуле G(x) допустима, то все заканчивается довольно просто. Действительно, тогда по теореме 2 получаем равенство ϕ′(G(x)) = ϕ[G(t)] = 0. По предположению индукции имеем, что G(t) P. Получаем противоречие с предположением ( x)G(x) P и аксиомой ( x)G(x) → G(t) по схеме A5.

Предположим теперь, что подстановка t вместо x в формуле G(x) недопустима. Заменим в формуле G(x) все связанные переменные так, чтобы эта подстановка была допустима. Полученную формулу обозначим через G(x). Если ( x)G(x) P, то рассуждаем так же, как и в предыдущем абзаце. Пусть ( x)G(x) P. Тогда по условиям (α) и (β) существует переменная w такая, что ¬G(w) P. По предположению индукции имеем равенство ϕ(G(w)) = 0. Однако ϕ(G(w)) = ϕ(G(w)) по теореме 1 о замене. Следовательно, ϕ(G(w)) = 0 и G(w) P. Как и выше, получаем противоречие с предположением ( x)G(x) P и аксиомой ( x)G(x) → G(w) по схеме A5. Случай 3 полностью рассмотрен.

§8. Теоремы о полноте

ио компактности

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

Теорема 3.6 (о полноте). Формула выводима из множества формул тогда и только тогда, когда она является логическим следствием этого множества.

90

Доказательство. Необходимость уже доказана (см. теорему об оправданности аксиоматизации). Достаточность докажем методом от противного. Предположим, что формула G является логическим следствием множества формул P и G не выводима из P. Тогда по свойству 2 непротиворечивых множеств (см. § 6) множество формул P {¬G} непротиворечиво. Из теоремы о непротиворечивости следует, что оно выполнимо. Это означает, что существует интерпретация ϕ такая, ϕ(P) = 1 и ϕ(¬G) = 1, т. е. ϕ(P) = 1 и ϕ(G) = 0. Получили противоречие с тем, что формула G является логическим следствием множества P.

Теорема 3.7 (о компактности). Если формула F является логическим следствием бесконечного множества формул P, то она является логическим следствием некоторого конечного подмножества P0 множества P.

Доказательство. Пусть формула F является логическим следствием бесконечного множества формул P. Тогда по теореме о полноте формула F выводима из P. Это означает, что существует вывод из P, последней формулой которого является формула F:

F1 , F2 , …, Fn = F.

Обозначим через P0 множество тех формул из P, которые встречаются в выводе. Ясно, что P0 – конечное множество и что этот вывод является выводом из множества P0 . Применим теорему о полноте еще раз, получим, что формула F является логическим следствием множества P0 .

§ 9. Независимость аксиом

Как мы уже отмечали, есть некоторая математическая традиция, идущая еще от древних греков, согласно которой аксиом в той или иной теории должно быть как можно меньше. В идеальном варианте – наименее возможное число. Для этого обычно ставится следующий вопрос: будет ли данная аксиома следствием других аксиом? В случае положительно ответа аксиому можно удалить из списка аксиом. В случае отрицательного ответа ее удалить нельзя и аксиома называется независимой (от остальных аксиом). Здесь можно сослаться на известную ситуацию в геометрии, а именно на вопрос о том следует ли пятый постулат Евклида из первых четырех. Как показали Лобачевский и Бойяи, пятый постулат независим от остальных аксиом.

В этом параграфе вопрос о независимости мы поставим для схем аксиом в следующей формулировке: можно ли данную схему аксиом получить из остальных схем с помощью правил

91

вывода? Мы решим этот вопрос только для логики высказываний. Так что схемами аксиом будут первые три, а правило вывода будет одно – модус поненс. Как мы увидим, во всех трех случаях имеет место независимость.

Теорема 3.7. Схема A1 независима от схем A2 и A3. Доказательство. Возьмем трехэлементное множество M

={0, 1, 2}. Элементы этого множества будем обозначать заглавными буквами латиницы. На множестве M введем на нем две операции: унарную Y = ¬X (отрицание) и бинарную Z = X→ Y (импликацию). Отрицание определяется таблицей 3.1, импликация – таблицей 3.2.

Определение. Интерпретацией называется функция ϕ: A → {0, 1, 2}, где A – множество атомарных формул логики высказываний.

С помощью таблиц 1 и 2 интерпретацию можно расширить на все множество формул логики высказываний.

Определение. Формула F логики высказываний называется выделенной, если для любой интерпретации ϕ выполняется равенство ϕ(F) = 0.

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

92

Убедимся в том, что правило MP сохраняет выделенность. Действительно, если ϕ(F) = 0 и ϕ(F → G) = 0, то, как следует из таблицы 0.2, выполняется равенство ϕ(G) = 0. Следовательно, любая формула, которая получается из аксиом схем A2 и A3 с помощью правила MP является выделенной.

Рассмотрим теперь аксиому F = X → (Y → X) схемы A1 и интерпретацию ϕ(X) = 1, ϕ(Y) = 2. Легко видеть, что ϕ(F) = 2. Аксиома F выделенной не является, а поэтому не может быть получена из аксиом схем A2 и A3 с помощью правила MP.

Теорема 3.8. Схема A2 независима от схем A1 и A3. Доказательство проводится аналогично доказательству

предыдущей леммы. Только здесь функции Y = ¬X (отрицание) и Z = X→ Y(импликацию) определим по-другому (см. таблицы

3.4 и 3.5)

Нетрудно проверить, что любая аксиома схем A1 и A3 является выделенной, и что правило MP сохраняет выделенность. С другой стороны, аксиома F = [X → (Y → Z)] → [(X → Y) → (X → Z)] схемы A2 при интерпретации ϕ(X) = 0, ϕ(Y) = 0, ϕ(Z) = 1 получает значение 2. Следовательно, F не может быть получена из аксиом схем A1 и A3 с помощью MP.

Теорема 3.9. Схема A3 независима от схем A1 и A2. Доказательство будет проведено методом, отличным от

метода доказательства лемм 1 и 2. Для формулы F логики высказываний через h(F) обозначим формулу, полученную из F удалением всех знаков отрицания. Формулу F будем называть выделенной, если h(F) – тождественно истинная формула логики высказываний.

Поскольку h(F → G) = h(F) → h(G), все аксиомы схем A1 и A2 являются выделенными. Нетрудно видеть также, что правило MP сохраняет выделенность. С другой стороны, аксиома F =

93

(¬Y → ¬X) → ((¬Y → X) → X) схемы A3 не является выделенной, так как формула h(F) = (Y → X) → ((Y → X) → X) не является тождественно истинной. Действительно, если ϕ(X) = ϕ(Y) = 0, то ϕ(h(F)) = 0. Это означает, что формула F не может быть получена из аксиом схем A1 и A3 с помощью MP.

§ 9. Другие аксиоматизации

Рассмотренная в предыдущих параграфах система аксиом и правил вывода взята из книги [Mен]. Будем называть эту систему системой Мендельсона. Кроме этой аксиоматизации в литературе изучались и другие аксиоматизации.

В этом параграфе мы приведем некоторые их них, правда, только в случае логики высказываний.

1. Система Мендельсона с правилом подстановки [см.

Мен]. В этой системе вместо схем аксиом берутся конкретные формулы-аксиомы и к правилу модус поненс добавляется правило подстановки, позволяющее в аксиому подставлять вместо атомарной формулы любую формулу.

2. Система Гильберта и Аккермана [см. ГБ или Мен]. Ос-

новные связки: ¬ и . Формула F → G понимается как сокращение формулы ¬F G. Система содержит четыре схемы аксиом:

1)F F → F,

2)F → F G,

3)F G → G F,

4)(G → H) → (F G → F H).

Единственное правило вывода – модус поненс.

3. Система Клини [см. Кл, стр. 48]. Основные связки: ¬, &,

и →. Система содержит 10 схем аксиом:

1)F → (G → F),

2)(F → (G → H)) → [(F → G) → (F → H)],

3)F & G → F,

4)F & G → G,

5)F → (G → F & G),

6)F → F G,

7)G → F G,

8)(F → H) → [(G → H) → (F G → H)],

9)(F → G) → [(F → ¬G) → ¬F],

10)¬¬F → F.

Единственное правило вывода – модус поненс.

94

4. Система Черча [см. Ч, стр. 112 − 113]. Основные связки:

¬и →. Система содержит три схемы аксиом:

1)F → (G → F),

2)(F → (G → H)) → [(F → G) → (F → H)],

3)(¬G → ¬F) → (F → G).

Единственное правило вывода – модус поненс.

Все рассмотренные выше варианты аксиоматизаций логики высказываний (т. е. системы аксиом и правил вывода) относятся к так называемым системам гильбертовского типа. В этих сис-

темах определяется некоторое множество схем аксиом (или конкретных аксиом) и множество правил вывода. Множество схем аксиом и правил вывода должно быть конечным, а множество аксиом – рекурсивным. Вывод из множества формул P определяется как последовательность формул, каждая формула которой принадлежит P или является аксиомой, или следует из предыдущих формул по одному из правил вывода. Формула G называется выводимой из P, если существует вывод из P, последней формулой которого является G. С примером аксиоматизации, которая не относится к гильбертовскому типу, можно познакомиться по книгам [ЕП] или [СО].

Приведем примеры на выводимость в разных системах.

Пример 11. Доказать, что |− F → F в системе Гильберта и Аккермана.

1) F → F F,

2) F F → F,

3) F → F.

Пример 12. Доказать, что |− F → F в системе Черча. Доказательство то же самое, что и в системе Мендельсона (см. пример 1).

Пример 13. Доказать, что ¬F |− F → G в системе Черча. 1) ¬F → (¬G → ¬F), A1 2) ¬F,

95

Для всех рассмотренных выше систем справедлива теорема о полноте: формула G выводима (в данной системе) из множества формул P тогда и только тогда, когда G является логическим следствием этого множества формул.

Задачи

Если в формулировке задач не указана система аксиом и правил вывода, то предполагается, что это система Мендельсона, т. е. та, которая введена в § 3.

1. Доказать, что ¬F → F |− F.

2. Доказать, что F → G, ¬F → G |− G (разбор случаев).

3. Напомним, что формула F G понимается как сокращение формулы ¬F → G. Доказать, что F G |− G F (коммутативность дизъюнкции).

4. Напомним, что формула F & G понимается как сокращение формулы ¬(F → ¬G). Доказать, что F & G |− G & F (коммутативность дизъюнкции).

5. Формула ( x)F(x) была введена как сокращение формулы

¬( x)¬F(x). Доказать, что ¬( x)¬F(x) |− ( x)F(x).

6. Доказать, что ( x)(F(x) → G(x)) |− ( x)F(x) → ( x)G(x). 7. Доказать, что ( x)(F(x) → G(x)) |− ( x)F(x) → ( x)G(x)..

8. В системе Гильберта и Аккермана доказать, что |− F → (G → H) или, используя сокращение, доказать, что |− F → (¬G H).

96

9. В системе Черча доказать, что ¬¬F |− F.

10. В системе Клини доказать, что {F → G, ¬G} |− ¬F. 11. В системе Клини доказать, что {F, ¬F} |− G.

12. В системе Клини доказать, что {F → (G → H), F &G} |−

H.

13. В системе Клини доказать, что {F → G, G → H, F G} |− H.

14. В системе Клини доказать, что {¬G → ¬F, ¬G → F} |−

G.

Решения

4. С учетом закона контрапозиции и теоремы о дедукции задачу можно сформулировать следующим образом:

G → ¬F, G|− ¬F.

97

Тогда решение становится очевидным. Достаточно одного применения правила MP.

5. С учетом сокращения надо доказать, что ¬¬( x)¬¬F(x) |−( x)F(x). Приведем соответствующую последовательность формул.

1) ¬¬( x)¬¬F(x), 2) ( x)¬¬F(x),

3) ( x)¬¬F(x) → ¬¬F(u), 4) ¬¬F(u),

5) F(u),

6) ( x)F(x).

6. С учетом теоремы о дедукции надо доказать, что

( x)(F(x) → G(x)), ( x)F(x) |− ( x)G(x). Приведем соответст-

вующую последовательность формул:

7. С учетом способа введения квантора существования и теоремы о дедукции, задачу можно записать следующим обра-

зом: ( x)(F(x) → G(x)), ¬( x)¬F(x) |− ¬( x)¬G(x). Далее, ис-

пользуя закон контрапозиции, задачу можно переписать так: ( x)(F(x) → G(x)), ( x)¬G(x) |− ( x)¬F(x). Приведем соответст-

вующую последовательность формул:

98

99