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

Примеры

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

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

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

${\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 года в Тюбингене под названием «Логики с ограниченными структурными правилами». В ходе конференции, предложил термин «субструктурная логика», который используется и в настоящее время.

Примечания

• F. Paoli (2002), , Kluwer.
• G. Restall (2000) , Routledge.

Литература

• Galatos, Nikolaos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono (2007), Residuated Lattices. An Algebraic Glimpse at Substructural Logics , Elsevier, ISBN 978-0-444-52141-5 .