Линейная логика III: предыстория. Конструктивная логика

One is the loneliest number that you'll ever do 
Two can be as bad as one 
It's the loneliest number since the number one

«One», Harry Nilsson 

Математика появляется, когда двоичность, что возникает из течения времени, абстрагируется от своих частных проявлений. Получившаяся таким образом, пустая форма общего содержания всех двоичностей становится первоначальной интуицией математики и, повторяясь неограниченно, создаёт новые математические объекты.¹  

Лейтзен Эгберт Ян Брауэр

Брауэр считал, что математика — это особый, доязыковой вид деятельности нашего разума, который заключается в конструировании и изучении свойств абстрактных объектов, в первую очередь натуральных чисел. Как особый вид деятельности математика не нуждается в сведении к формальной логике, хотя таковая и является частью математики. Впрочем, к логике бездумно применённой к бесконечным наборам объектов у него были претензии. Пусть, например, мы показали, что ¬∀x ¬P(x). Согласно классической логике это означает, что  ∃x P(x). И если x принимает конечное число значений, то проверив их по очереди, мы сможем найти требуемый. Но если x может принимать неограниченное количество значений, то мы не вправе говорить, что требуемый объект существует, поскольку мы не можем в этом удостоверится напрямую.

Обычно для математиков существование математического объекта установлено уже тогда, когда  показано, что предположение о невозможности его существования приводит к противоречию. Разрешено (существует), всё что не запрещено. Для интуициониста же нужно указать конкретный объект, который удовлетворяет условиям. Так что закон исключённого третьего для интуиционизма не выполняется — этот закон представляет собой общий принцип, а не рецепт.

Оппонентом Брауэра стал Давид Гильберт. "Никому не удастся изгнать математиков из Рая", говорил он. Не принимая и логицизм, Гильберт боялся за судьбу математического знания — если следовать конструктивному подходу, то многие из теорем, например, мат. анализа придётся выкинуть. Не желая ничего выкидывать, Гильберт затеял программу спасения математики — выделить содержательное ядро, метаматематику, в которой приемлемы только финитные методы, остальную же математику формализовать, свести к игре символами, и эту игру изучать в рамках содержательной математики, с целью показать непротиворечивость такой игры. Из попытки эту программу реализовать родилась computer science; деятельность  Чёрча, Тюринга, Гёделя, Клини напрямую связана с реализацией этой программы.

Брауэру формалистский подход Гильберта был неинтересен. "Ложная теория, не натолкнувшаяся на противоречие, не становится от этого менее ложной", утверждал он. Также, его не интересовало формальное изложение логики интуционистской математики. Но его ученики были свободны от несколько мистических взглядов учителя, и Аренд Хейтинг формализовал интуиционистскую логику. Она не сильно отличалась от классической, в ней просто отсутствовал закон исключенного третьего и его аналоги, а также правило отрицания для кванторов.

Но что значит интуиционистская логика? Для логики классической известны модели, в том числе конечные. Интуиционистская логика кажется уродливой по сравнению с классической, без столь симметричных правил де Моргана. Есть ли у неё собственные модели? Интерпретация интуиционистской логики была представлена Хейтингом и независимо от него А. Н. Колмогоровым. По давней математической традиции, именованные определения должны содержать имя математика, не имеющего отношения к определению. Интерпретация носит имена Брауэра — Хейтинга — Колмогорова (сокращенно BHK).

В чём же она заключалась? Как уже было замечено, интуиционисты по-другому трактуют связку или и квантор существования — они требуют чтобы, доказательство утверждения A или B содержало указание на то, в каких случаях выполняется A, а в каких B, а доказательство утверждения "существует  x такой что...", давало ответ, как найти такой x. Такой подход можно обобщить, поменяв смысл "утверждать, что высказывание верно". В интерпретации BHK нельзя ничего утверждать, не предоставив свидетельство. С каждым высказыванием сопоставляется набор свидетельств его истинности. Ложное высказывание не имеет свидетельств в свою пользу. Чтобы определить логические связки достаточно указать, какой объект мы ожидаем получить в качестве свидетельства истинности. Отношение "a свидетельствует об A" обозначим a : A. Кроме того, логические связки с поведением отличным от классического стоит иначе обозначать. Это другое "или", другой квантор существования, с точки зрения интуициониста более сильные нежели их классические варианты. Конструктивные аналоги обозначим так:

A + B — конструктивное или

∑x P(x) — конструктивное существует
⇒ — конструктивное следует

Тогда интуиционистские логические связки можно определить так:

• A ⋀ B — свидетельством служит пара (a,b), где a : A,  b : B
• A + B — свидетельством служит пара (l, a) или (r, b), где a : A, b : B, а l и r — теги, определяющие, какое из высказываний A, B полагается верным
• A ⇒ B — свидетельством служит алгоритм, по которому можно из a : A получить b : B 
• ¬A — свидетельством служит алгоритм, по которому можно из a : A получить свидетельство абсурдного высказывания. Если обозначить ⊥ некое ложное высказывание, то  ¬A  можно определить как A ⇒ ⊥
• ∀x P(x) — свидетельством служит алгоритм, по которому можно из x получить p : P(x)
• ∑x P(x) — свидетельством служит пара (x, p), где для х выполняется P(x), а p является свидетельством этого 

Таким образом, конструктивное доказательство утверждения есть описание конструирования объекта, подтверждающего это утверждение.

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

Хотелось бы еще обратить внимание на операцию следования. Её классический вариант никак не связывает причину и следствие, интуиционистское следование чуть более релевантно — требуется алгоритм, по которому можно перейти от причины к следствию. Ничего, правда, не сказано про то, должен ли алгоритм использовать причину при построении следствия. В линейной логике такое требование налагается, но всему своё время. 

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

---

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