Логика
Contents
Логика#
Математика это в первую очередь не вычисления, а доказательства. Традиционно, доказательство определяют как рассуждение, убедительное настолько, что тот, кто его воспринял, будет готов убеждать других с помощью того же рассуждения. Математическое доказательство убеждает, что высказываемое утверждение без сомнения является истинным, а противное — невозможно.
Но смысл слов определяется тем, как их используют, и в математике слова используют значительно иначе, чем в обычной жизни. И отличаются не только сложные понятия вроде «убедительности», даже базовые логические конструкции вроде «из \(P\) следует \(Q\)» используются иначе, чем в быту.
Обычно, точный смысл слов познаётся в процессе взаимодействия с людьми, обладающими нужными знаниями. Но в математике смысл слов определён настолько точно, что его можно обозначить не только с помощью общих принципов, но даже с помощью формальных правил.
Мы сформулируем принципы и правила естественного вывода для логики первого порядка. Эта логика является основой многих математических теорий, включая аксиоматическую теорию множеств. А рассматриваемые идеи станут основой и для исчисления построений — формальной системы, которую мы будем использовать в будущем.
Естественный вывод это набор правил, позволяющих вывести заключение из посылок. Посылки и заключение являются суждениями, называемыми также утверждениями
Утверждение это утверждаемое высказывание — то есть высказывание, которое мы признаём истинным. Оно записывается после знака \(\vdash\) (турникет). Так, например, утверждение, что \(1+2 = 3\) записывается так:
Эту запись можно читать следующим образом: «я утверждаю (я знаю), что \(1+2 = 3\)».
Высказывания формируются из логических связок и констант, кванторов и предикатов (отношений). Предикаты применяются к одному или более выражению. Например, в высказывании \(1 + 2 = 3\) отношение \((=)\) применяется к выражениям \(1+2\) и \(3\).
Логические связки формируют новые высказывания из существующих: если \(P\) и \(Q\) — высказывания, то высказываниями являются также \(P → Q\) («если \(P\), то \(Q\)»), \(P ∧ Q\) («\(P\) и \(Q\)»), \(P ∨ Q\) («\(P\) или \(Q\)»), \(P ↔ Q\) («\(P\) равносильно \(Q\)»), и \(¬P\) («не \(P\)»).
Кванторы формируют высказывание, связывая переменную в логической формуле: например, \(∃x.\; 2 = x\) («существует такое \(x\), что \(2 = x\)») связывает переменную \(x\) в формуле \(2 = x\).
Логические константы являются высказываниями. Единственной константой которую мы рассмотрим является \(⊥\) (абсурд).
Выражения это обычные математически выражения. Они строятся из констант, функциональных символов и переменных. Мы считаем, что выражению соответствует единственное конкретное значение.
Правила, по которым из посылок выводится заключение, имеют следующий вид:
Здесь \(\cal A_1, \dots, \cal A_n\) это посылки, когда же \(\cal B\) — заключение.
Некоторые высказывания мы утверждаем без доказательства — они называются аксиомами. Кроме аксиом бывают также схемы аксиом — они отличаются от аксиом наличием метапеременных, и становятся утверждениями после подстановки конкретных формул на место метапеременных.
Обозначив сеттинг, разберём последовательно все связки и кванторы.
Импликация#
Импликация \(P → Q\) (если \(P\), то \(Q\)) означает, что из \(P\) следует \(Q\). Конкретный смысл этого высказывания мы обозначим следующим принципами.
Мы можем утверждать \(P → Q\) если располагаем таким рассуждением, что оно, будучи соединено с доказательством \(P\), автоматически бы давало доказательство \(Q\). Двойственно, если мы располагаем доказательством \(P → Q\), то тогда, если мы знаем что верно \(P\), то можем утверждать и \(Q\).
Чтобы построить требуемое для доказательства \(P → Q\) рассуждение, нам нужен способ временно постулировать истинность \(P\). Таким способом являются гипотетические суждения.
Гипотетическое суждение отличается от обычного утверждения наличием контекста — списка предположений по левую сторону от турникета. Например, утверждение, что в предположении \(f(2) = 2\) и \(f(3) = 6\) верно \(f(2) + f(3) = 8\) записывается следующим образом:
Эту запись можно читать следующим образом: «в предположении, что \(f(2) = 2\) и \(f(3) = 3\) я утверждаю, что \(f(2) + f(3) = 8\)».
Обозначая произвольный (возможно даже пустой) контекст как \(Γ\), запишем следующие два правила вывода для предположений:
Первое правило, называемое рефлексивностью, выражает то, что в предположении \(A\) верно \(A\). Это соответствует предназначению предположений: временно постулировать высказывание. При этом по левую сторону от \(A\) может быть произвольный набор предположений. Это правило позволяет вводить и использовать предположения.
Второе правило, называемое монотонностью, выражает то, что верно без \(A\) остаётся верным если предположить \(A\). Это правило позволяет не использовать предположения.
Определив гипотетические суждения, сформулируем теперь правила для импликации:
Эти правила называются, соответственно, введением и удалением импликации. Они соответствуют определяющим импликацию принципам (мы это наглядно покажем чуть позже).
Множеству предположений соответствует цепь импликаций:
Подобную цепь можно читать следующим образом: если \(P\), и если \(Q\), то \(R\). Мы полагаем, что импликация правоассоциативна, и записываем это высказывание без скобок как \(P → Q → R\).
Определив все необходимые правила для импликации, рассмотрим пример. Докажем следующее высказывание: если из \(P\) следует \(Q\), и если из \(Q\) следует \(R\), то тогда из \(P\) следует \(R\).
Мы докажем его двумя способами: сначала записав доказательство как список предположений и утверждений, где каждое утверждение следует из предыдущих утверждений или предположений. Затем, мы разберём полный вывод требуемого утверждения с помощью правил.
Доказываемое высказывание записывается символьно как \((P → Q) → (Q → R) → P → R\). Запишем само доказательство:
Пусть \(P → Q\)
Пусть \(Q → R\)
Пусть \(P\)
Тогда \(Q\)
И затем \(R\)
Следовательно, \(P → R\)
Следовательно, \((Q → R) → P → R\)
Следовательно, \((P → Q) → (Q → R) → P → R\)
Уровень вложенности соответствует области действия предположений. Слово «пусть» вводит предположение и увеличивает отступ, когда же слово «следовательно» снимает предположение, уменьшает отступ и вводит импликацию.
Суждения, выводимые с помощью удаления импликации, просто пишутся друг за другом.
Теперь полностью выведем утверждения используя правила вывода. Сначала мы должны привести все предположения к одному контексту, сделаем это:
Затем дважды используем удаление импликации:
И, наконец, снимем предположения, последовательно вводя импликации:
Всё доказательство целиком можно записать как одно большое дерево вывода:
Даже для столь простого утверждения соответствующее ему дерево вывода весьма громоздко. Поэтому мы будем использовать доказательства в виде списка. Правила вывода при этом определяют то, какие последовательности утверждений допустимы.
Мы говорили, что смысл логических связок в математике отличается от смысла похожих высказываний в обычной жизни. Чтобы показать это наглядно, докажем, что для любых высказываний \(P\) и \(Q\) верно \(P → Q → P\):
С одной стороны, это высказывание аналогично высказыванию «из \(P\) следует \(P\)», но с неиспользованным предположением \(Q\). Но с другой стороны оно означает следующее: пусть верно \(P\). Тогда из \(Q\) следует \(P\).
Иначе говоря, высказывание \(Q → P\) может быть истинным для логически никак не связанных высказываний \(P\) и \(Q\). Так, например, верно высказывание «если \(1=1\), то \(2+3 = 5\)».
Это значительно отличается от обычного понятия следствия, где предположения и вывод логически связаны друг с другом. Высказывание вроде «если Лондон это столица Великобритании, то \(3\cdot 3 = 9\)» алогично в быту, но допустимо в том смысле, в котором мы используем импликацию в математике.
Мы говорили, что можем утверждать \(P → Q\) в том случае, если располагаем рассуждением, которое в сочетании с доказательством \(P\) даёт доказательство \(Q\). Чтобы этот принцип выполнялся, нам нужен метод, превращающий последовательное введение и удаление импликации в прямое доказательство следствия.
Покажем этот метод на примере использования утверждения \(P → Q → P\).
Редукция импликации осуществляется в три шага:
Сначала подставляем доказательство \(P\) во все места, где используется правило рефлексивности для \(P\): в данном случае, на место \(P \vdash P\)
Затем стираем предположение \(P\) в суждениях вида \(Γ, P, Δ \vdash \cdots\).Так \(P,Q \vdash P\) превращается в \(Q \vdash P\)
Наконец, стираем последовательные введение и удаление импликации
Таким образом, наши правила вывода действительно соответствуют определяющему импликацию принципу.
В высказывании \(P → Q\) роли составляющих его высказываний \(P\) и \(Q\) существенно различны: тот, кто использует утверждение \(P → Q\) должен предоставить доказательство \(P\) чтобы получить доказательство \(Q\). Двойственно, когда мы доказываем \(P → Q\), мы рассуждаем так, будто обладаем доказательством \(P\), и должны построить доказательство \(Q\).
Обобщим эту идею на составные высказывания. Рассмотрим сначала высказывание \(P → Q → R\). Тот, кто использует это утверждение, должен предоставить доказательство \(P\) чтобы получить доказательство \(Q → R\). Но затем, чтобы получить \(R\), он должен предоставить доказательство \(Q\). Двойственно, когда мы доказываем \(P → Q → R\), мы предполагаем \(P\) и \(Q\) и должны доказать \(R\).
Таким образом, в высказывании \(P → Q → R\) высказывания \(P\) и \(Q\) имеют одну и ту же роль, отличающуюся от роли \(R\).
Теперь рассмотрим высказывание \((P → Q) → R\). Тот, кто использует это утверждение, должен предоставить доказательство \(P → Q\). Но при построение этого доказательства он предполагает \(P\) и должен доказать \(Q\). Когда же мы доказываем \((P → Q) → R\), мы предполагаем \(P → Q\). Но чтобы воспользоваться этим предположением, мы должны предоставить доказательство \(P\).
Таким образом, в случае \((P → Q) → R\) доказательства высказываний \(P\) и \(R\) строит доказывающий утверждение, когда же доказательство \(Q\) строит тот, кто использует утверждение.
Обобщением этих рассуждений является понятие полярности. Полярность высказываний определяется рекурсивно:
Высказывание целиком имеет положительную полярность
Если \(P → Q\) имеет положительную полярность, то полярность \(P\) отрицательна, а полярность \(Q\) — положительна
Если же \(P → Q\) имеет отрицательную полярность, то тогда полярность \(P\) положительна, а полярность \(Q\) отрицательна
В качестве примера разберём полярность высказывания \((S → P) → (Q → R)\).
Высказывание \((S → P) → (Q → R)\) целиком имеет положительную полярность
Высказывание \(S → P\) имеет отрицательную полярность, когда же полярность высказывания \(Q → R\) положительна
\(S\) имеет положительную полярность когда же \(P\) — отрицательную, \(Q\) имеет отрицательную полярность, когда же \(R\) — положительную.
Таким образом мы разобрали все полярности этого выражения.
Квантор всеобщности#
Из выражений, отношений и связок можно составлять не только высказывания, но и формулы вроде \(x + 1 > 0\). Они отличаются от высказываний наличием свободных переменных в выражении. Подставляя в формулу различные значения можно получить различные высказывания, например \(2+1 > 0\) или \(-3+1 > 0\).
Формула со свободными переменными сама по себе не является высказыванием, так как непонятно, о каких значениях идёт речь. Но кроме непосредственно подстановки, возможные значения можно обозначить с помощью квантора.
Пусть \(\phi\) это формула со свободной переменной \(x\). Высказывание \(∀x.\; \phi\) («для любого \(x\) верно \(\phi\)») означает, что \(\phi\) верно для любого значения на месте переменной \(x\).
Мы можем утверждать \(∀{\color{red}x}.\; \phi\) в том случае, когда располагаем рассуждением, с помощью которого можно доказать \(\phi[{\color{red}x} := {\color{red}t}]\) для любого значения \({\color{red}t}\). Двойственно, если мы располагаем доказательством \(∀{\color{red}x}.\; \phi\), то можем утверждать \(\phi[{\color{red}x} := {\color{red}t}]\) для любого \({\color{red}t}\).
Чтобы построить доказательство \(∀x.\; \phi\) нам нужен способ временно предположить, что \(x\) это некоторое значение. Для этого мы расширяем понятие контекста: теперь это список как высказываний, так и переменных.
Например, утверждение, что \(x+1 = 3\) в предположении, что \(x\) это значение, равное двум, записывается следующим образом:
Эту запись можно читать следующим образом: «в предположении, что \(x\) — значение и \(x = 2\), я утверждаю, что \(x + 1 = 3\)».
Для введения переменных в контекст нам потребуется новое правило вывода:
Запись \({\color{red}x}\mathrel\#Γ,P\) означает, что переменная \({\color{red}x}\) не входит ни в контекст \(Γ\), ни в высказывание \(P\). Это важное ограничение: мы предполагаем произвольное значение, никак не связанное с другими.
Правила для предположений остаются теми же, но с учётом того, что высказывания могут использовать только те переменные, которые уже есть в контексте. Так, например, в контексте \(Γ,A\) высказывание \(A\) может содержать только те свободные переменные, которые уже есть в \(Γ\). При этом если в контексте уже есть переменная, то во всех рассуждениях с этим контекстом мы воспринимаем эту переменную как полноценное значение.
Учитывая всё сказанное, запишем правила введения и удаления квантора всеобщности:
Эти правила похожи на соответствующие правила для импликации.
Переменная \(x\) в \(∀x.\; \phi\) связывается точно также, как связываются переменные в лямбда выражении. И точно также мы считаем альфа-эквивалентные высказывания одним и тем же высказыванием.
Квантор захватывает всё, что справа него: например, \(∀x.\; \phi → P\) это то же самое, что и \(∀x.\; (\phi → P)\). Запись \(∀x\,y.\; \phi\) означает высказывание \(∀x.\;∀y.\; \phi\).
Рассмотрим теперь пример рассуждения, использующего импликацию и квантор всеобщности.
Предположим, что нам дано некоторое отношение \(R\), про которое известно следующее:
Для любых трёх чисел \(a\), \(b\) и \(c\), если \(R(a, b)\), то \(R(a, b+c)\)
Для любых трёх чисел \(a\), \(b\) и \(c\), если \(R(a+c, b+c)\), то \(R(a, b)\)
Докажем следующее утверждение: для любых чисел \(n\) и \(k\), если \(R(k,n)\), то и \(R(0,n)\).
Пусть \(n\) и \(k\) — числа
Пусть \(R(k,n)\)
\(R(k,n) → R(k, n+k)\) (первое свойство)
Отсюда \(R(k, n+k)\)
\(k = 0+k\)
Отсюда \(R(0+k, n+k)\)
\(R(0+k, n+k) → R(0,n)\) (второе свойство)
Отсюда \(R(0,n)\)
Следовательно, \(R(k,n) → R(0,n)\)
Следовательно, \(∀n\,k.\; R(k,n) → R(0,n)\)
Рассмотрим вывод, соответствующий шагам этого доказательства.
Сначала нам нужно ввести свойства отношения \(R\) в нужный контекст. Покажем как на примере первого свойства \(R\) (второе свойство вводится аналогично):
В контексте с переменными \(n\) и \(k\) мы можем применить удаление квантора всеобщности:
Дальнейшие утверждения в доказательстве, кроме равенства и его использования, выводятся с помощью удаления импликации. Подробный разбор отношения равенства мы оставим на потом.
Вывод завершает последовательное введение импликации и квантора всеобщности:
Теперь рассмотрим как редуцировать последовательное введение и удаление квантора всеобщности, тем самым получив прямое доказательство для данного значения \(t\).
Условно, редукцию можно описать следующим образом:
Последовательно же мы делаем следующее:
Всюду при предположении значения \(x\) подставляем \(t\) на место \(x\) в выражения
Стираем \(x\) из контекстов
Стираем введение и удаление квантора всеобщности
Таким образом правила для квантора всеобщности соответствуют определяющим его принципам.
Когда мы рассматривали импликацию, мы замечали, что различные части высказывания \(P → Q\) имеют различные роли. Аналогичные рассуждения можно применить и к квантору всеобщности. Однако, в логике первого порядка высказывания не являются значениями, и поэтому положительная полярность значений может быть обусловлена только импликацией.
Конъюнкция и дизъюнкция#
Высказывание \(P ∧ Q\) («\(P\) и \(Q\)») означает, что верны оба высказывания, когда же высказывание \(P ∨ Q\) («\(P\) или \(Q\)») означает, что верно по крайней мере одно из них.
Мы можем утверждать высказывание \(P ∧ Q\) в том случае, когда располагаем доказательствами как \(P\), так и \(Q\). Двойственно, если мы располагаем доказательством \(P ∧ Q\), то можем утверждать любое из этих высказываний.
Высказывание \(P ∨ Q\) же мы можем утверждать в том случае, когда располагаем либо доказательством \(P\), либо доказательством \(Q\). Принцип использования у \(P ∨ Q\), однако, несколько сложнее, чем у \(P ∧ Q\). Пусть мы располагаем двумя рассуждениями: одно доказывает некоторое высказывание \(R\) в предположении \(P\), другое же доказывает \(R\) в предположении \(Q\). Тогда, если мы располагаем доказательством \(P ∨ Q\), то можем утверждать \(R\).
Запишем теперь соответствующие правила введения и удаления. Сначала для конъюнкции:
Затем для дизъюнкции:
Конъюнкция и дизъюнкция связываются с высказываниями сильнее, чем импликация: например, \(S → P ∧ Q\) означает \(S → (P ∧ Q)\). Запись \(P ∨ Q ∧ R\) означает \(P ∨ (Q ∧ R)\), однако в подобных формулах принято использовать скобки.
Рассмотрим теперь пример доказательства с конъюнкцией и дизъюнкцией. Докажем следующее утверждение: если \(P\) и \(Q ∨ R\), то тогда \(P ∧ Q\) или \(P ∧ R\).
Пусть \(P ∧ (Q ∨ R)\)
Тогда \(P\)
И \(Q ∨ R\)
Разберём \(Q ∨ R\)
Пусть \(Q\)
Тогда \(P ∧ Q\)
И, следовательно, \((P ∧ Q) ∨ (P ∧ R)\)
Пусть \(R\)
Тогда \(P ∧ R\)
И, следовательно, \((P ∧ Q) ∨ (P ∧ R)\)
Cледовательно, \(P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)\)
В этом доказательстве используются все четыре правила:
С помощью удаления конъюнкции мы получаем \(P\) и \(Q ∨ R\) из \(P ∧ (Q ∨ R)\)
Введение конъюнкции позволяет получить \(P ∧ Q\) из \(P\) и \(Q\)
Введение дизъюнкции превращает \(P ∧ Q\) в \((P ∧ Q) ∨ (P ∧ R)\)
И, наконец, удаление дизъюнкции позволяет получить \((P ∧ Q) ∨ (P ∧ R)\) из соответствующих рассуждений для \(P\) и для \(R\)
Как и для остальных связок, последовательное введение и удаление конъюнкции или дизъюнкции в доказательстве можно редуцировать.
В случае конъюнкции редукцию совсем просто выполнить:
Для дизъюнкции она сложнее, но не сильно сложнее:
Предположения стираются по тому же принципу что и при редукции импликации.
Ни конъюнкция, ни дизъюнкция не влияют на полярность выражений, из которых они состоят. Однако, с полярностью связана возможность выбора высказывания: когда мы доказываем \(P ∧ Q\), мы должны предоставить оба доказательства, но когда используем \(P ∧ Q\), то можем выбрать то, какое именно из утверждений нужно. Двойственно, когда мы доказываем \(P ∨ Q\), то вольны выбрать любое из них для доказательства, но при использовании \(P ∨ Q\) должны рассмотреть обе возможности.
Высказывание \(P ↔ Q\) («\(P\) равносильно \(Q\)») означает равносильность высказываний \(P\) и \(Q\). Оно определяется как конъюнкция импликаций:
Отрицание#
Отрицание \(¬P\) означает невозможность \(P\) в сильном смысле этого слова: из \(P\) следует абсурд. Это сокращённая запись высказывания \(P → ⊥\).
Чтобы понять сущность абсурда, рассмотрим следующее рассуждение:
Пусть верно \(P ∨ Q\)
Пусть \(P\) невозможно
Тогда верно \(Q\)
Знание того, что \(P\) не может быть истинным позволяет отсечь ветвь дизъюнкции и получить \(Q\).
Но наличие одновременно доказательств \(P\) и \(¬P\) позволяет таким образом вывести произвольное высказывание \(Q\):
Мы знаем, что \(P\)
Следовательно, \(P ∨ Q\) (введение дизъюнкции!)
Мы знаем, что \(¬P\)
Следовательно, \(Q\)
Отсюда, учитывая определение \(¬P\), мы получаем, что из абсурда следует что угодно. Этот принцип выражается следующим правилом вывода:
Ранее мы замечали, что если существует доказательство \(Q\), то тогда высказывание \(P → Q\) верно для любого высказывания \(P\). Теперь же мы видим двойственное свойство: если существует доказательство \(¬P\), то тогда высказывание \(P → Q\) верно для любого \(Q\).
Это свойство снова противоречит бытовому представлению о следствии, но вполне соответствует определяющему импликацию принципу: давать доказательство \(Q\) при наличии доказательства \(P\).
В непротиворечивой теории абсурд может быть доказан только при наличии дополнительных противоречивых предположений. И если предположение \(P\) абсурдно, то любое изощрённое доказательство \(P → Q\) оказывается бессодержательным, так как из \(P\) следует вообще любое высказывание. Содержательным оказывается лишь доказательство \(P → \bot\), так как оно явно показывает невозможность \(P\).
Рассмотрим теперь пример доказательства с отрицанием. Докажем следующее утверждение: если \(P → Q\) и \(¬Q\), то тогда \(¬P\).
Пусть \(P → Q\) и пусть \(¬Q\)
Пусть \(P\)
Тогда \(Q\)
Что абсурдно, так как \(¬Q\)
Следовательно, \(¬P\)
Следовательно, \((P → Q) → ¬Q → ¬P\)
Квантор существования#
Высказывание \(∃x.\;\phi\) («существует такое \(x\) что \(\phi\)») означает, что существует такое значение \(t\) что верно \(\phi[x:=t]\).
Мы можем утверждать \(∃x.\;\phi\) в том случае, когда располагаем доказательством \(\phi[x:=t]\) для некоторого значения \(t\). Принцип использования квантора существования сложнее и похож на соответствующий принцип для импликации. Пусть мы располагаем рассуждением, которое, предполагая наличие значения \(x\) удовлетворяющего свойству \(\phi\), доказывает некоторое высказывание \(P\). Тогда, если мы знаем, что \(∃x.\;\phi\), то можем утверждать \(P\).
Запишем правила введения и удаления, соответствущие этим принципам:
Особенности, касающиеся синтаксиса и захвата переменных, у квантора существования те же, что и у всеобщности: квантор захватывает всё, что справа и связывает соответствующую переменную. И как и раньше, мы считаем альфа-эквивалентные высказывания одним и тем же высказыванием.
Рассмотрим пример доказательства с использованием квантора существования. Докажем следующее: если не существует такого \(x\), что \(\phi\), то тогда для любого \(x\) верно \(¬\phi\).
Пусть \(¬∃x.\;\phi\)
Пусть \(x\) это некоторое значение
Пусть \(\phi\)
Тогда \(∃x.\;\phi\)
Что абсурдно, так как \(¬∃x.\;\phi\)
Следовательно, \(¬\phi\)
Следовательно, \(∀x.\; ¬\phi\)
Следовательно, \((¬∃x.\;\phi) → ∀x.\; ¬\phi\)
Кванторы всеобщности и существования можно совмещать в высказывании, причём его смысл зависит от их порядка. Рассмотрим влияние порядка кванторов на смысл высказываний на паре примеров.
Сначала докажем следующее высказывание: для любого \(x\) существует такое \(y\), что \(x = y\).
Пусть \(x\) — значение
\(x = x\)
Значит, \(∃y.\; x = y\)
Следовательно, \(∀x.\;∃y.\; x = y\)
В доказательстве этого высказывания мы сначала предположили наличие значения \(x\) и затем выбрали значение \(y\) в зависимости от значения \(x\).
При другом порядке кванторов мы должны были бы сначала выбрать значение \(x\), а уже затем показать, что соответствующее этому значению свойство выполняется для любого \(y\). Чтобы показать это наглядно, докажем следующее высказывание: существует такое число \(x\), что для любого \(y\) верно \(x \cdot y = x\).
\(∀y.\; 0 \cdot y = 0\)
Следовательно, \(∃x.\; ∀y.\; x \cdot y = x\)
Квантор существования двойственен квантору всеобщности в смысле полярности значения: если в случае \(∀x.\;\phi\) мы предполагаем \(x\) и должны доказать \(\phi\), то в случае \(∃x.\; \phi\) мы должны как найти подходящее значение, так и доказать соответствующее ему высказывание.
Двойственность можно заметить и в плане выбора значения: если при доказательстве \(∀x.\; \phi\) мы ожидаем любое \(x\), но при использовании \(∀x.\; \phi\) вольны выбрать любое значение для подстановки, то в случае \(∃x.\; \phi\) мы выбираем подходящее значение когда доказываем высказывание, когда же при использовании \(∃x.\; \phi\) мы должны ожидать любое значение удовлетворяющее свойству \(\phi\). Эта двойственность в выборе схожа с двойственностью \(P ∧ Q\) и \(P ∨ Q\).
Как и в случае с квантором всеобщности, доказательство с последовательным введением и удалением квантора существования можно редуцировать. Условно, редукцию можно описать так:
Чтобы выполнить редукцию, нужно сначала преобразовать доказательство \(Γ,x,\phi \vdash P\) в доказательство \(Γ,\phi[x:=t] \vdash P\) действуя также, как и при редукции квантора всеобщности. Затем доказательство \(Γ,\phi[x:=t] \vdash P\) преобразуется в доказательство \(Γ \vdash P\) точно так же, как и при редукции импликации.
Квантор существования завершает список логических конструкций в логике первого порядка. Нам осталось лишь рассмотреть принцип, разделяющий конструктивную (интуиционистскую) и классическую логики.
Принцип исключённого третьего#
Для каждого высказывания \(P\) принцип исключённого третьего утверждает \(P ∨ ¬P\). На первый взгляд это совершенно очевидное утверждение: высказывание либо истинно, либо ложно, как же иначе? Но здесь также есть различие между математикой и обычной жизнью.
В математических теориях есть высказывания, которые невозможно ни доказать, ни опровергнуть. Самым известным (и, наверное, первым) примером такого высказывания является аксиома параллельности в нейтральной геометрии. Это высказывание недоказуемо в ней, и более того, добавив его или его отрицание к аксиомам, мы получаем различные геометрии: евклидову и гиперболическую, соответственно.
Другим примером является континуум-гипотеза в теории множеств — и как и в случае с геометрией, добавление этого высказывания или его отрицания к аксиомам приводит к различным новым теориям множеств.
Пусть \(E\) это именно подобное высказывание. Как и для любого другого высказывания, принцип исключённого третьего утверждает, что
Это довольно странное утверждение: мы утверждаем, что по крайней мере одно из высказываний истинно, однако невозможно в принципе утверждать ни одно из них.
Но странности на этом не заканчиваются. Принцип исключённого третьего также позволяет вывести следующее утверждение:
Мы оказываемся в противоестественной ситуации: мы утверждаем «существует число!», однако в принципе невозможно назвать ни одно число, которое бы удовлетворяло требуемому свойству.
Есть два способа разрешить подобную ситуацию. Конструктивная (или интуиционистская) математика не признаёт принцип исключённого третьего, и в ней подобная проблема не возникает: каждому доказательству существования соответствует некоторое построенное значение, а каждой дизъюнкции — конкретное доказанное значение.
Классическая математика принимает принцип исключение третьего и никак не обосновывает его в понятиях самой логики. Вместо этого она сопоставляет логической теории различные её модели, в которых каждое высказывание имеет определённое логическое значение. При этом в одних моделях высказывание \(E\) оказывается истинным, а в других — ложным. И во всех моделях соответствующие им значения \(n\) существуют, хотя могут быть различны в различных моделях.
Таким образом, классическая логика это логика реальности — в реальности вещи либо имеют место, либо не имеют места быть, хотя мы можем не знать, что именно из этого истинно. Конструктивная логика же это логика фактов: мы утверждаем высказывание только тогда, когда мы можем установить факт его истинности. И не существует метода, показывающего истинность или ложность произвольного высказывания.
В этой книге мы будем использовать конструктивную логику везде, где это возможно, переключаясь на классическую логику там, где конструктивное доказательство невозможно или непрактично. Кроме эстетических, на это есть также и практические причины.
Различные объекты в математике образуют математические структуры, которые называются категориями, и у этих категорий может быть внутренняя логика. Эта логика, как правило, конструктивна. Доказательство снаружи может быть перенесено вовнутрь, тем самым превращаясь в доказательство утверждения про объекты этой категории. Но это возможно только в случае, когда доказательство совместимо со внутренней логикой категории, что в случае большинства интересных категорий означает конструктивность.
Хотя принцип исключённого третьего не выполняется в конструктивной логике, его отрицание в этой логике ложно:
Пусть \(¬(P ∨ ¬P)\)
Пусть \(P\)
Тогда \(P ∨ ¬P\)
Что абсурдно, так как \(¬(P ∨ ¬P)\)
Следовательно, \(¬P\)
Тогда снова \(P ∨ ¬P\)
Что абсурдно, так как \(¬(P ∨ ¬P)\)
Следовательно, \(¬¬(P ∨ ¬P)\)
Таким образом, название «принцип исключённого третьего» является вводящим в заблуждение: речь идёт не о каком-то третьем логическом значении, а о предположении какого-либо значения без явных свидетельств.
Эквивалентным принципу исключению третьего является закон двойного отрицания, который утверждает, что из \(¬¬P\) следует \(P\). Рассуждение выше фактически доказывает, что из закона двойного отрицания следует принцип исключённого третьего, доказательство в другую сторону же сводится с разбору дизъюнкции.
В конструктивной логике принцип исключённого третьего можно использовать при доказательстве отрицания. Покажем это, доказав следующее: если из \(P ∨ ¬P\) следует \(¬Q\), то тогда \(¬Q\).
Пусть \(P ∨ ¬P → ¬Q\)
Пусть \(Q\)
Пусть \(P\)
Тогда \(P ∨ ¬P\)
И, следовательно, \(¬Q\)
Что абсурдно, так как \(Q\)
Следовательно, \(¬P\)
И снова \(P ∨ ¬P\)
И, следовательно, \(¬Q\)
Что абсурдно, так как \(Q\)
Следовательно, \(¬Q\)
Следовательно, \((P ∨ ¬P → ¬Q) → ¬Q\)
Приведём теперь пример утверждения, выводимого только в классической логике. Докажем, что если из \(P\) следует \(Q\), то тогда \(¬P\) или \(Q\).
Пусть \(P → Q\)
Разберём \(P ∨ ¬P\)
Пусть \(P\). Тогда \(Q\) и, следовательно, \(¬P ∨ Q\)
Пусть \(¬P\). Тогда \(¬P ∨ Q\)
Следовательно, \((P → Q) → ¬P ∨ Q\)
Логика первого порядка#
В заключение сформулируем логику первого порядка, правила для который мы всё это время рассматривали.
Синтаксис выражений и формул:
\({\color{red}pred}\), \({\color{red}fun}\) и \({\color{red}const}\) означают конечные наборы отношений, функциональных символов и констант. Этот набор у каждой теории свой. Например, теория множеств вводит только отношения \((=)\) и \((∈)\), когда же арифметика Пеано вводит отношение \((=)\), функциональный символ \(S\) и константу \(0\).
Логика определяется тем, какие высказывания в ней можно выражать, и тем, какие утверждения выводимы. Рассмотренный нами естественный вывод это одна из многих систем дедукции для логики первого порядка. Тем не менее, запишем ещё раз все правила вывода.
Предположения:
Импликация:
Конъюнкция:
Дизъюнкция:
Абсурд:
Квантор всеобщности:
Квантор существования:
Вместе с синтаксисом формул, правила вывода завершают описание логики первого порядка.