Субструктурная логика

В исчисление секвенций каждая строка доказательства записывается как:

${\displaystyle \Gamma \vdash \Sigma }$.

Здесь, структурные правила — правила переписывания левой части (условия), изначально представляемого как строка (последовательность) суждений. Стандартная интерпретация этой строки — конъюнкция. Поэтому

${\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {C}}}$

является записью секвента для:

(A и B) влечёт за собой C.

В данном случае мы принимаем правую часть (консеквент) логического вывода Σ за единственное суждение C (интуиционистский стиль секвента), но для общего случая ситуация не меняется, поскольку все манипуляции происходят слева от символа турникета ${\displaystyle \vdash }$.

Так как конъюнкция является коммутативной и ассоциативной операцией, формальное изложение теории секвенций обычно включает структурные правила для соответствующего переписывания последовательности — например, для вывода:

${\displaystyle {\mathcal {B}},{\mathcal {A}}\vdash {\mathcal {C}}}$

Из:

${\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {C}}}$.

Существуют дополнительные структурные правила, соответствующие идемпотентным и монотонным свойствам конъюнкции.

Так, из:

${\displaystyle \Gamma ,{\mathcal {A}},{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

можно сделать вывод, что:

${\displaystyle \Gamma ,{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$.

А из:

${\displaystyle \Gamma ,{\mathcal {A}},\Delta \vdash {\mathcal {C}}}$

что для любого B верно:

${\displaystyle \Gamma ,{\mathcal {A}},{\mathcal {B}},\Delta \vdash {\mathcal {C}}}$.

Линейная логика, в которой дубликаты гипотез «учитываются» иначе, чем единичные вхождения, исключает оба эти правила. Релевантная логика просто игнорирует последнее правило на том основании, что B явно не имеет отношения к заключению.

Выше приведены основные примеры структурных правил. В рамках логики высказываний применение данных правил выглядит достаточно убедительным. В теории доказательств они возникают естественным образом и впервые были замечены именно там (до того, как получили название).

Правило позволяет заменить два одинаковых высказывания одним. Например, A,A |- B эквивалентно A |- B. В субструктурной логике это правило может быть отменено, что приводит к тому, что A,A |- B не следует из A |- B.

Допустим, было куплено два яблока, в разных магазинах. Предположим, что A означает «яблоко куплено», а B означает «яблоко съедено».

В классической логике можно сказать, что если яблоко куплено и яблоко куплено, то, в итоге яблоко съедено. Это эквивалентно тому, что в любом случае, купленное яблоко будет съедено.

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

Правило позволяет добавить любое высказывание к доказательству без изменения его заключения. Например, A |- B эквивалентно A,C |- B. В субструктурной логике это правило может быть отменено, что приводит к тому, что A,C |- B не следует из A |- B.

Предположим, что A означает «жить в России», а B означает «говорить по-русски», а C это «любовь к футболу».

В классической логике можно сказать, что если человек живёт в России, то говорит по-русски. Это эквивалентно тому, что если кто-то живёт в России и любит футбол, то говорит по-русски.

В субструктурной логике иначе. Если кто-то живёт в России и любит футбол, то это не означает то, что он говорит по-русски. Может быть, что человек родился вне России или не изучал русский язык или предпочитает говорить на другом языке или живёт в России несколько дней. Поэтому, из того, что кто-то живёт в России, не значит говорить по-русски. Правило ослабления не работает в этом случае.

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

Однако, так как, например:

${\displaystyle \{a,a\}=\{a\}}$,

то сокращение выполняется абсолютно свободно, если предпосылки являются множествами.

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

Субструктурные логики — относительно молодое направление. Первая конференция по этой теме состоялась в октябре 1990 года в Тюбингене под названием «Логики с ограниченными структурными правилами». В ходе конференции, Коста Дошен предложил термин «субструктурная логика», который используется и в настоящее время.