Русская Википедия:Субструктурная логика
Субструктурная логика — логика, в которой отсутствует одно из обычных Шаблон:Iw (например, классической и интуиционистской), таких как ослабление, контракция, обмен или ассоциативность. Двумя наиболее значимыми субструктурными логиками являются релевантная и линейная.
Примеры
В исчисление секвенций каждая строка доказательства записывается как:
- <math>\Gamma\vdash\Sigma</math>.
Здесь, структурные правила — правила переписывания Шаблон:Нп4, изначально представляемого как строка (последовательность) суждений. Стандартная интерпретация этой строки — конъюнкция. Поэтому
- <math>\mathcal A,\mathcal B \vdash\mathcal C</math>
является записью секвента для:
- (A и B) влечёт за собой C.
В данном случае мы принимаем правую часть (консеквент) логического вывода Σ за единственное суждение C (интуиционистский стиль секвента), но для общего случая ситуация не меняется, поскольку все манипуляции происходят слева от символа турникета <math>\vdash</math>.
Так как конъюнкция является коммутативной и ассоциативной операцией, формальное изложение теории секвенций обычно включает структурные правила для соответствующего переписывания последовательности — например, для вывода:
- <math>\mathcal B,\mathcal A\vdash\mathcal C</math>
Из:
- <math>\mathcal A,\mathcal B\vdash\mathcal C</math>.
Существуют дополнительные структурные правила, соответствующие идемпотентным и монотонным свойствам конъюнкции.
Так, из:
- <math> \Gamma,\mathcal A,\mathcal A,\Delta\vdash\mathcal C</math>
можно сделать вывод, что:
- <math> \Gamma,\mathcal A,\Delta\vdash\mathcal C</math>.
А из:
- <math> \Gamma,\mathcal A,\Delta\vdash\mathcal C</math>
что для любого B верно:
- <math> \Gamma,\mathcal A,\mathcal B,\Delta\vdash\mathcal C</math>.
Линейная логика, в которой дубликаты гипотез «учитываются» иначе, чем единичные вхождения, исключает оба эти правила. Релевантная логика просто игнорирует последнее правило на том основании, что 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 это «любовь к футболу».
В классической логике можно сказать, что если человек живёт в России, то говорит по-русски. Это эквивалентно тому, что если кто-то живёт в России и любит футбол, то говорит по-русски.
В субструктурной логике иначе. Если кто-то живёт в России и любит футбол, то это не означает то, что он говорит по-русски. Может быть, что человек родился вне России или не изучал русский язык или предпочитает говорить на другом языке или живёт в России несколько дней. Поэтому, из того, что кто-то живёт в России, не значит говорить по-русски. Правило ослабления не работает в этом случае.
Состав предпосылок
Существует множество способов составления посылок (а в случае многозначного вывода — и заключений). Один из способов — собрать их во множество.
Однако, так как, например:
- <math>\{a, a\} = \{a\}</math>,
то сокращение выполняется абсолютно свободно, если предпосылки являются множествами.
Кроме того, в числе прочих свойств присутствуют ассоциативность и коммутативность. В субструктурных логиках, как правило, предпосылки не сводятся ко множествам, а представляют собой более сложные структуры, такие как дерево, мультимножества (множества, различающие несколько вхождений элементов) или секвенции формул. Например, в линейной логике, учитывая, что контракция не работает, предпосылки должны быть составлены в виде структуры, по крайней мере, такой же подробной, как мультимножества.
История
Субструктурные логики — относительно молодое направление. Первая конференция по этой теме состоялась в октябре 1990 года в Тюбингене под названием «Логики с ограниченными структурными правилами». В ходе конференции, Коста Дошен предложил термин «субструктурная логика», который используется и в настоящее время.
Примечания
- F. Paoli (2002), Substructural Logics: A Primer, Kluwer.
- G. Restall (2000) An Introduction to Substructural Logics, Routledge.
Литература
- Galatos, Nikolaos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono (2007), Residuated Lattices. An Algebraic Glimpse at Substructural Logics, Elsevier, Шаблон:ISBN.
