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

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

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

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

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

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

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

(А и B) подразумевает C.

Здесь мы берем RHS Σ как одно предложение 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} = {a} у нас есть сокращение бесплатно, если предпосылки являются наборами. У нас также есть бесплатные ассоциативность и перестановка (или коммутативность), среди других свойств. В субструктурной логике обычно предпосылки не объединяются в наборы, а скорее объединяются в более мелкие структуры, такие как деревья или мультимножества (наборы, которые различают множественные вхождения элементов) или последовательности формул. Например, в линейной логике, поскольку сжатие не удается, предпосылки должны быть составлены по крайней мере в чем-то столь же мелкомасштабном, как мультимножества.

История

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

Смотрите также

• Система субструктурного типа
• Остаточная решетка

Примечания

Рекомендации

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

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

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

внешняя ссылка

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