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

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

Примеры

В секвенциальном исчислении каждую строку доказательства записывают как

$\Gamma \vdash \Sigma$.

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

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

как последовательное обозначение для

( A и B ) влечет C .

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

Поскольку конъюнкция является коммутативной и ассоциативной операцией, формальная структура теории секвенций обычно включает структурные правила для соответствующего переписывания секвенции Γ - например, для вывода

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

от

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

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

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

мы можем сделать вывод

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

Также из

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

можно вывести для любого B ,

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

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

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

Состав помещения

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

История

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

См. также

• Система субструктурных типов
• Оставшаяся решетка

Ссылки

• Ф. Паоли (2002), Субструктурная логика: учебник для начинающих , Kluwer.
• Дж. Рестолл (2000) Введение в субструктурную логику , Routledge.

Дальнейшее чтение

• Галатос, Николаос, Питер Джипсен, Томаш Ковальски и Хироакира Оно (2007), Остаточные решетки. Алгебраический взгляд на субструктурную логику , Elsevier, ISBN   978-0-444-52141-5 .

Внешние ссылки

• СМИ, связанные с субструктурной логикой, на Викискладе?
• Ресталл, Грег. «Субструктурная логика» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .