4 Пропозициональная логика: доказательства

4.1 II.1 Введение в пропозиционные доказательства

В этой главе вводится доказательная система в стиле Гильберта (Hilbert-style proof system) для пропозициональной логики, называемая PL. Метод таблиц истинности уже является доказательной системой, но PL имеет то преимущество, что предоставляет формальную доказательную систему, основанную на пошаговом рассуждении, начиная с аксиом или других предположений и используя Modus Ponens как правило вывода.

Правило Modus Ponens записывается так:

\[ \frac{A \quad A \to B}{B} \] и позволяет вывести формулу B при условии, что две формулы A и A → B уже были выведены. Это позволяет PL моделировать (в определённой степени) то, как люди строят доказательства.

Введение доказательной системы PL — это первый шаг к развитию метаматематики. «Метаматематика» означает использование математических инструментов, особенно математической логики, для изучения формализации самой математики. Определение PL-доказательств даёт математическое определение доказательств; это позволяет рассматривать доказательства как математические объекты сами по себе и даже доказывать теоремы о доказательствах. Логика первого порядка даст гораздо более содержательное рассмотрение метаматематики, но пропозициональная логика и PL-доказательства уже иллюстрируют многие ключевые концепции.

Цель пропозиционного доказательства — установить, что некоторая формула является тавтологией или что выполняется некоторая тавтологическая импликация. Мы будем писать ⊢ A, чтобы обозначить, что A имеет пропозициональное доказательство, и будем писать B₁, …, Bₖ ⊢ A, чтобы обозначить, что A имеет PL-доказательство из гипотез B₁, …, Bₖ. Таким образом, одинарный символ «⊢» используется для доказуемости (provability), в отличие от двойного символа «⊧» для тавтологической истинности/импликации.

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

(1) Алгоритмичность. Доказательства будут строками символов (также называемыми «выражениями») с заданными синтаксическими свойствами. Должен существовать алгоритм, который, получив строку w символов, определяет, является ли w корректным доказательством, и если да — какую формулу оно доказывает или какую тавтологическую импликацию оно доказывает. Мы ещё не дали формального определения понятия «алгоритм», но неформально это означает любую процедуру, которую может выполнить соответствующая (идеализированная) компьютерная программа.

(2) Корректность. Формула A должна иметь доказательство только в том случае, если она является тавтологией. Аналогично, если A можно доказать из гипотез B₁, …, Bₖ, то должна выполняться тавтологическая импликация B₁, …, Bₖ ⊧ A.

(3) Полнота. Наоборот, любая тавтология A должна иметь доказательство. Аналогично, если выполняется B₁, …, Bₖ ⊧ A, то должно существовать доказательство A из гипотез B₁, …, Bₖ12.

Вместе свойства корректности и полноты означают, что ⊢ A выполняется тогда и только тогда, когда ⊧ A выполняется. То же самое справедливо и для тавтологических импликаций.

(4) Удобство для пользователя. Есть несколько аспектов:
(i) Доказательная система должна уметь эффективно имитировать человеческое рассуждение.
(ii) В частности, она должна позволять рассуждать пошаговыми выводами.
(iii) Доказательства должны быть понятны человеку без чрезмерных усилий.

(5) Элегантность. Доказательная система должна быть математически элегантной и не содержать чрезмерно большого количества аксиом или правил.

(6) Эффективный поиск доказательств. Должны существовать эффективные, практичные алгоритмы для поиска и построения доказательств.

К сожалению, остаётся открытой проблемой (связанной с вопросом P versus NP), возможно ли всегда осуществлять действительно эффективный поиск доказательств. Тем не менее, одни доказательные системы лучше других позволяют осуществлять такой поиск. Это большая и активная область текущих исследований, и современное состояние дел позволяет находить доказательства по крайней мере для некоторых очень больших пропозициональных формул, включая многие формулы с сотнями тысяч или миллионами переменных.

Метод таблиц истинности (truth tables) может служить пропозиционной доказательной системой. Для этого нужно лишь установить канонический способ кодировать всю таблицу истинности в виде строки символов. Таблицы истинности, безусловно, удовлетворяют критериям (1)–(3) выше. Они не удовлетворяют критерию (6), поскольку таблицы истинности обычно имеют экспоненциальный размер. Они также не удовлетворяют критериям (4) и (5).

Система доказательств в стиле Гильберта PL хорошо удовлетворяет критериям (1)-(5), за исключением условия (4.iii) — лёгкости понимания. Остаётся открытым вопрос, удовлетворяет ли PL критерию (6) — возможности эффективного поиска доказательства; на самом деле, обычно предполагается, что поиск доказательства в PL может быть очень трудным, требуя экспоненциального времени в худшем случае.

4.2 II.2 Система доказательств PL

Теперь мы определим систему доказательств высказываний PL. Это так называемая система доказательств «в стиле Гильберта» 13.

В целях упрощения PL использует только формулы с {¬, →}. Другие связки, такие как ∨, ∧ и ↔︎, являются сокращениями для эквивалентных формул, которые используют только {¬, →}. Конкретно:

  1. A ∨ B — сокращение для ¬A → B
  2. A ∧ B — сокращение для ¬(A → ¬B)
  3. A ↔︎ B — сокращение для (A → B) ∧ (B → A)

Доказательства в PL начинаются с аксиом или других гипотез и выводят новые формулы с помощью правила Modus Ponens. В PL разрешены четыре типа аксиом.

Аксиомы PL
Аксиомы PL — это все формулы следующих форм14:

  1. PL1: A → (B → A)
  2. PL2: [A → (B → C)] → [(A → B) → (A → C)]
  3. PL3: ¬A → (A → B)
  4. PL4: (¬A → A) → A

где A, B и C могут быть любыми {¬, →}-формулами.

Modus Ponens. Единственное правило вывода для PL — Modus Ponens; а именно:
из A и A → B разрешается вывести B. Это обозначается так:

\[ \frac{A \quad A \to B}{B} \]

Здесь A и B могут быть любыми {¬, →}-формулами.

Определение II.1. Пусть A — это {¬, →}-формула. PL-доказательство формулы A — это последовательность {¬, →}-формул

A₁, A₂, A₃, …, A_ℓ

такая, что A_ℓ — это A и что каждая Aᵢ удовлетворяет одному из следующих условий:

(a) Aᵢ является аксиомой PL; или
(b) Aᵢ выводится по правилу Modus Ponens из двух более ранних формул Aⱼ и Aₖ с j, k < i.
Конкретно, имеем Aₖ = Aⱼ → Aᵢ, так что применение Modus Ponens имеет вид:

\[ \frac{A_j \quad A_j \to A_i}{A_i} \]

Последняя формула A_ℓ является заключением PL-доказательства и именно она считается доказанной формулой.

Более общо, можно использовать множество Γ формул в качестве дополнительных гипотез в PL-доказательстве, которые можно свободно применять в ходе доказательства.

Определение II.2. PL-доказательство формулы A из гипотез Γ — это последовательность {¬, →}-формул

A₁, A₂, …, A_ℓ

такая, что A_ℓ есть A и каждая Aᵢ удовлетворяет одному из следующих условий:
(a) Aᵢ является PL-аксиомой;
(b) Aᵢ принадлежит Γ; или
(c) Aᵢ выводится с помощью Modus Ponens из двух более ранних формул Aⱼ и Aₖ при j, k < i.

PL-доказательства также иногда называют PL-выводами. Мы записываем ⊢ A для обозначения того, что A имеет PL-доказательство; в этом случае мы говорим, что A является теоремой. Аналогично, мы записываем Γ ⊢ A для обозначения того, что A имеет PL-доказательство из гипотез Γ; тогда мы говорим, что A является теоремой множества Γ. Заметьте, что допускается, что Γ бесконечно; однако одно доказательство может содержать только конечное число формул, а значит, может использовать только конечное число гипотез из Γ.

Когда Γ — конечное множество {B₁, …, Bₖ}, мы обычно опускаем фигурные скобки и пишем просто B₁, …, Bₖ ⊢ A. Мы также вольно используем обозначения вида Γ, A ⊢ B вместо Γ ∪ {A} ⊢ B.

Теорема II.3.

  1. Если Γ ⊢ A и Γ′ ⊃ Γ, то Γ′ ⊢ A.
  2. Если Γ ⊢ A, то существует конечное подмножество Γ₀ ⊆ Γ такое, что Γ₀ ⊢ A.

Доказательство. Часть (a) следует непосредственно из определения Γ ⊢ A. Часть (b) вытекает из того наблюдения, что доказательство может содержать только конечное число формул.

Чтобы упростить запись, предполагаем, что все формулы являются {¬, →}-формулами до конца этой главы.

Пример II.4. Существует PL-доказательство формулы (¬A → A) → (¬A → B), где A и B — произвольные формулы.
PL-доказательство состоит из следующих трёх формул:

  1. ¬A → A → B аксиома PL3
  2. (¬A → A → B) → (¬A → A) → (¬A → B) аксиома PL2
  3. (¬A → A) → (¬A → B) Modus Ponens, 1, 2

Аксиома PL2 выше получается, если в определении аксиомы PL2 положить A = ¬A, B = A и C = B.

Пример II.5. Существует PL-доказательство формулы A → A, где A — произвольная формула.
То есть, ⊢ A → A. PL-доказательство состоит из следующих пяти формул:

  1. (A → ((A → A) → A)) → (A → (A → A)) → (A → A) аксиома PL2
  2. A → ((A → A) → A) аксиома PL1
  3. (A → (A → A)) → (A → A) Modus Ponens, 1, 2
  4. A → (A → A) аксиома PL1
  5. A → A Modus Ponens, 3, 4

Аксиома PL2 выше получается, если положить B = (A → A) и C = A.
Первая аксиома PL1 получается, если положить B = (A → A); вторая — если положить B = A.

Пример II.6. Для любых A и B формулы B → (A ∨ B) и ¬¬A → (A ∨ B) имеют PL-доказательства.
Чтобы это увидеть, напомним, что формула C ∨ D является сокращением для ¬C → D.
Таким образом, эти две формулы равны B → (¬A → B) и ¬¬A → (¬A → B). Первая является частным случаем аксиомы PL1; вторая — частным случаем аксиомы PL3. Следовательно, каждая из них имеет PL-доказательство, состоящее из единственной формулы — аксиомы.

Упражнение II.11 предлагает показать, что A → (A ∨ B) имеет PL-доказательство.

Пример II.7. Формула A → B имеет PL-доказательство из гипотезы B.
То есть, B ⊢ A → B. PL-доказательство состоит из трёх формул:

  1. B → (A → B) аксиома PL1
  2. B гипотеза
  3. A → B Modus Ponens

Пример II.8. Любая формула A имеет доказательство из самой себя как гипотезы;
то есть, A ⊢ A. PL-доказательство состоит всего из одной формулы A.

Теорема II.9. Множество теорем (теорем PL) замкнуто относительно подстановки. Другими словами, если ⊢ A, то ⊢ A(B/pᵢ) для любых формул A и B и любой переменной pᵢ.

Доказательство. Множество аксиом PL очевидно замкнуто относительно подстановки.
Также, корректные применения Modus Ponens замкнуты относительно подстановки, так как

\[ \frac{D(B/p_i) \quad (D \to E)(B/p_i)}{E(B/p_i)} \quad\text{то же самое, что и}\quad \frac{D(B/p_i) \quad D(B/p_i) \to E(B/p_i)}{E(B/p_i)} \]

Отсюда следует, что если A₁, A₂, A₃, …, A_ℓ — это PL-доказательство, то
A₁(B/pᵢ), A₂(B/pᵢ), A₃(B/pᵢ), …, A_ℓ(B/pᵢ)
также является PL-доказательством.

Это утверждение доказывается индукцией по шагам в PL-доказательстве.

4.3 II.3 Теорема о дедукции

Теорема о дедукции — это наш первый основной инструмент для доказательства существования доказательств в исчислении высказываний. Она является аналогом для доказуемости теоремы I.16, в которой утверждалось, что Γ ⊧ A → B эквивалентно Γ, A ⊧ B.

Интуиция, лежащая в основе теоремы о дедукции, заключается в том, что доказательство импликации A → B эквивалентно предположению, что A выполняется, и доказательству B с использованием гипотезы A.

Теорема II.10 (Теорема о дедукции). Γ, A ⊢ B тогда и только тогда, когда Γ ⊢ A → B.

Доказательство. Направление «если» (“if”) очень простое. Предположим, что Γ ⊢ A → B. Тогда также
Γ, A ⊢ A → B. Поскольку Γ, A ⊢ A, модус поненс даёт Γ, A ⊢ B.

Направление «только если» (“only if”) — это важное направление. Предположим, что Γ, A ⊢ B и что
C₁, C₂, C₃, …, C_ℓ
— это PL-доказательство формулы B из Γ, A, так что C_ℓ — это формула B. Каждая Cᵢ является либо аксиомой, либо элементом множества Γ, либо формулой A, либо выведена с помощью модуса поненс.

Докажем по индукции по i, что Γ ⊢ A → Cᵢ. Доказательство по индукции делится на три случая.

Случай 1: Предположим, что Cᵢ является либо аксиомой, либо элементом множества Γ. Тогда, очевидно, Γ ⊢ Cᵢ. Также, Cᵢ → (A → Cᵢ) является экземпляром аксиомы PL1. Следовательно, по модусу поненс, Γ ⊢ A → Cᵢ, что и требовалось.

Случай 2: Предположим, что Cᵢ — это A. По примеру II.5, Γ ⊢ A → A, что эквивалентно Γ ⊢ A → Cᵢ, что и требовалось.

Случай 3: Предположим, что Cᵢ выведена по модусу поненс из Cⱼ и Cₖ при j, k < i. Без потери общности считаем, что Cₖ равна Cⱼ → Cᵢ. Индукционные предположения для Cⱼ и Cₖ состоят в том, что A → Cⱼ и A → Cₖ являются теоремами множества Γ. Докажем, что существует доказательство A → Cᵢ из Γ следующим образом:

  1. Γ ⊢ A → Cⱼ — индукционное предположение
  2. Γ ⊢ A → (Cⱼ → Cᵢ) — индукционное предположение
  3. Γ ⊢ (A → (Cⱼ → Cᵢ)) → (A → Cⱼ) → (A → Cᵢ) — аксиома PL2
  4. Γ ⊢ (A → Cⱼ) → (A → Cᵢ) — модус поненс
  5. Γ ⊢ A → Cᵢ — модус поненс

Это завершает доказательство по индукции, и, поскольку A → C_ℓ эквивалентно A → B, это также завершает доказательство теоремы о дедукции.

Заметим, что аксиома PL2 — это именно то, что нужно, чтобы рассуждение в случае 3 работало легко.

Теорема II.9 и Теорема о дедукции являются первыми примерами «метаматематики», то есть использования математических инструментов для изучения математических объектов, таких как теоремы и доказательства. Мы дали формальные определения «теорем» и «доказательств» как математических объектов, и теперь теоремы II.9 и Теорема о дедукции утверждают свойства о (PL-)теоремах; их доказательства используют индукцию на данном PL-доказательстве для доказательства существования другого PL-доказательства.

Гипотетический силлогизм. В качестве примера того, как использовать теорему о дедукции, мы покажем, что правило вывода гипотетического силлогизма (формула II.1)

\[ \frac{A \to B \quad B \to C}{A \to C} \]

является производным правилом вывода для исчисления высказываний (PL).

Теорема II.11. Для любых формул A, B и C: ⊢ (A → B) → ((B → C) → (A → C)).

Доказательство.
Мы используем “⇔” в значении «тогда и только тогда». Применяя теорему о дедукции три раза, получаем следующие эквивалентности:

⊢ (A → B) → ((B → C) → (A → C))

⇔ A → B ⊢ (B → C) → (A → C) — теорема о дедукции

⇔ A → B, B → C ⊢ A → C — теорема о дедукции

⇔ A → B, B → C, A ⊢ C — теорема о дедукции

A → B, B → C, A ⊢ C выполняется, поскольку объединение трёх гипотез с двумя применениям модуса поненс доказывает C.

Следствие II.12. Если Γ ⊧ A → B и Γ ⊧ B → C, то Γ ⊧ A → C.

Это следствие означает, что правило вывода гипотетического силлогизма допустимо в доказательствах в исчислении высказываний как «производное правило» вывода. То есть, хотя модус поненс — единственное разрешённое правило вывода для PL-доказательств, мы, тем не менее, можем разрешить применения гипотетического силлогизма при доказательстве существования PL-доказательства. Это связано с тем, что гипотетический силлогизм может быть смоделирован несколькими шагами в PL-доказательстве. Следовательно, если бы гипотетический силлогизм был добавлен в PL в качестве дополнительного правила вывода, это не сделало бы систему доказательств PL более сильной.

  1. Полнота иногда называется «Адекватность» (“Adequacy”), например, у Ходела [10], но здесь мы следуем общепринятой конвенции и называем это «полнотой».↩︎

  2. Системы в стиле Гильберта названы в честь Давида Гильберта, одного из основателей математической логики, так как этот стиль доказательств использовался в книге Д. Гильберта и В. Аккермана Grundzüge der theoretischen Logic (1928) (Foundations of Mathematical Logic). Система, подобная гильбертовской, уже использовалась А. Н. Уайтхедом и Б. Расселом в 1910 г. в их классическом труде Principia Mathematica. Ещё раньше Г. Фреге использовал предшественника гильбертовских систем доказательств в своей работе Begriffsschrift (1879). Все три этих работы стали вехами в становлении современного изучения математической логики. Система в стиле Гильберта PL, которую мы используем, взята из Ходела (Hodel) [10], который назвал её L.↩︎

  3. Квадратные скобки в PL2 имеют тот же смысл, что и обычные круглые скобки, и используются только для улучшения читаемости.↩︎