Линейная логика VII: Слово как действие

Среди философов слишком долго было укоренено убеждение, что «утвер­ждение» может только «описывать» положение вещей или «утверждать нечто о каком-либо факте», который при этом должен быть либо истинным, либо ложным.

«Как совершать действия при помощи слов?», Джон Лэнгшо Остин

До нашего дня удержались некоторые абсурдные музыкальные понятия прошлого, например: увертюра к опере и антрактная музыка в драматическом представлении. С чисто музыкальной точки зрения и то и другое ‒ ерунда, ибо если дело идет только о том, чтобы дать публике время занять места, то с одинаковым успехом можно до начала оперы «Фиделио» играть «Ах, мой милый Августин». Если же увертюра написана в форме попурри, то спрашивается, зачем нужно вперед заставлять публику прослушивать мотивы, которые впоследствии будут пропеты?

«Короб мыслей», Антон Рубинштейн.

Увертюра закончилась. Начинается действие. В центре этого действия находится фигура Жана Ива Жирара, человека, который своими работами предопределил развитие логики в конце XX века, и который переопределил саму логику в XXI, но речь сейчас о более раннем времени. В начале 80-ых Жирар занимался изучением моделей интуиционистской логики. В одной из них он  обнаружил, что логические операции там можно разложить на более примитивные ‒ это и подвигло его на разработку линейной логики. Система получилась интересной, но необычной, уж больно странными были требования налагаемые на утверждения. Правда, не обязательно трактовать объекты, с которыми работает линейная логика, как утверждения, возможны и другие трактовки, например, как планы и действия, ресурсы и их преобразования, диалоги и сюжеты, игры и стратегии, химические реакции и программы с параллельным вычислением.  

Мы пока сосредоточимся на логической трактовке. Ограничение состоит в следующем: в стандартном случае в линейной логике каждую гипотезу полагается использовать ровно один раз. То есть, мы обязаны использовать гипотезу, и не можем использовать более одного раза. В логике такое ограничение позволяет ввести вариант закона двойного отрицания и правил де Моргана, восстановив симметрию классической логики внутри конструктивной теории. Это достигается за счёт увеличения количества логических связок ‒ теперь у нас два "и" и два "или". Рассмотрим их:

A ⊗ B — "мультипликативное и", A и B справедливы одновременно, их вывод использует разные наборы гипотез.  

A ⊕ B — "аддитивное или", справедливо А или справедливо B, в каждом конкретном случае известно, что именно. Такую операцию можно трактовать как операцию внешнего выбора. Мы не можем выбрать, что произошло, но можем узнать.

A & B — "аддитивное и", можно вывести и A и B, но надо выбрать только одно из них, у них общий набор гипотез. Это операция внутреннего выбора.

A ℘ B — "мультипликативное или",¹ связка, которая указывает на зависимость между утверждениями ‒ возможно, что справедливо A или B, но неизвестно, что именно. Узнать, что выполняется можно лишь при наличии дополнительной информации (например, что не выполняется A, тогда можно вывести B и наоборот). 

В линейной логике даже понятия истины и лжи присутствуют в двух вариантах: 0 и ⊤ ‒ аддитивная ложь и истина, ⊥, 1 ‒ мультипликативная ложь и истина. По одной константе на каждую из связок.

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

p^⊥⊥ = p

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

(A ⊗ B)^⊥ = A^⊥℘ B^⊥
(A & B)^⊥ = A^⊥⊕ B^⊥
(A ⊕ B)^⊥ = A^⊥& B^⊥
(A ℘ B)^⊥ = A^⊥⊗ B^⊥ 

Чтоб читатель не вглядывался в обилие разных странных значков, правила достаточно просты: при отрицании свойство аддитивности/мультипликативности сохраняется (а округлость значка - нет). Правила сформулированы так, чтоб для любого утверждения A

A^⊥⊥ = A

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

Какие еще операции есть в линейной логике? Мы не ввели линейную операцию следования, и в классической линейной логике она не является базовой. Но если обратить внимание на "мультипликативное или", то в нём угадывается алгоритмическое содержание, это почти функция. Это не случайно, линейную импликацию определяют как

A ⊸ B = A^⊥℘ B

A^⊥℘ B можно прочесть как "мне не хватает одного A, чтоб построить одно B" (или если я отдам вам одно B, мне будет не хватать одного A).  То есть, линейную импликацию можно представить как действие, которое можно совершить над A, превратив его в B. A в процессе перестаёт существовать.  Подставив вместо B ⊥ мы получим знакомое

A ⊸ ⊥ = A^⊥℘ ⊥, что равносильно  A^⊥

Таким образом, линейное отрицание является более сильным, чем интуиционистское отрицание ‒ чтобы утверждать A^⊥ необходимо прийти к противоречию, имея одну гипотезу A без возможности её дублировать.

Чтобы линейная логика могла доказывать обычные теоремы, нам необходимо ввести дополнительные одноместные логические связки ‒ ! и ?:
! — задаёт модальность "конечно", гипотезы такого типа можно невозбранно дублировать и удалять, если среди гипотез еще остаётся копия.
? — задаёт дуальную модальность "не исключено". Очень классическая модальность. С точки зрения линейной логики свидетельство непротиворечивости, которое является конструктивным содержанием классических теорем, можно трактовать как "конечно не исключено,  что ...".

Связки ! и ? называют экспоненциальными поскольку ! переводит "аддитивное и" в мультипликативное (? аналогичным образом поступает с или), подобно тому как экспонента переводит сумму в произведение:

!(A & B) = !A ⊗ !B
?(A ⊕ B) = ?A ℘ ?B

Экспоненциальные связки связаны соотношениями:

?(A^⊥) = (!A)^⊥
!(A^⊥) = (?A)^⊥

которые объясняют, каким образом нарушается симметрия, когда мы рассматриваем интуиционистское, нелинейное отрицание (! - )^⊥. Два нелинейных отрицания A дадут не A, а только ?!A. Предваряя разговор о том, как с помощью линейной логики передать конструктивные и классические теоремы, можно сказать, что интуиционистская логика не "замечает" наличие/отсутствие !, но "замечает" присутствие ?, в отличие от логики классической, которая не замечает обоих. Потому классическая логика обладает симметрией, а интуиционистская нет.

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

---

¹ Каноническим обозначением для "мультипликативного или" является значок перевёрнутого амперсанда ⅋, но он не везде нормально отображается.