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

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

Примеры

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

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

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

${\ displaystyle {\ mathcal {A}}, {\ mathcal {B}} \ vdash {\ mathcal {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), Остаточные решетки. Алгебраический взгляд на субструктурную логику , Elsevier, ISBN   978-0-444-52141-5 .

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

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