Гиперсеквенциальный

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

\Gamma _{1}\Rightarrow \Delta _{1}\mid \cdots \mid \Gamma _{n}\Rightarrow \Delta _{n}

Секвенции, составляющие гиперсеквенцию, называются компонентами. Дополнительная выразительность структуры гиперсеквенции обеспечивается правилами, управляющими различными компонентами, такими как правило связи для промежуточной логики LC (логика Гёделя – Даммета).

{\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Sigma \Rightarrow A\qquad \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Pi \Rightarrow B}{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Sigma \Rightarrow B\mid \Pi \Rightarrow A}}

или правило модального разделения для модальной логики S5 : ^[1]

{\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma ,\Theta \Rightarrow \Box \Pi ,\Omega }{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma \Rightarrow \Box \Pi \mid \Theta \Rightarrow \Omega }}

Гиперсеквенциальные исчисления использовались для лечения модальных логик , промежуточных логик и субструктурных логик . Гиперсеквенции обычно имеют формульную интерпретацию, т. е. интерпретируются формулой объектного языка, почти всегда как своего рода дизъюнкцию. Точная интерпретация формулы зависит от рассматриваемой логики.

и пропозициональные правила Формальные определения

Формально под гиперсеквенцией обычно понимают конечное мультимножество обычных секвенций , записываемое

\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}

Секвенции, составляющие гиперсеквенцию, состоят из пар мультимножеств формул и называются компонентами гиперсеквенции. Также рассматриваются варианты определения гиперсеквенций и секвенций через множества или списки вместо мультимножеств, причем в зависимости от рассматриваемой логики секвенции могут быть классическими или интуиционистскими. Правила для пропозициональных связок обычно представляют собой адаптацию соответствующих стандартных правил секвенции с дополнительной боковой гиперсеквенцией, также называемой гиперсеквенционным контекстом. Например, общий набор правил для функционально полного набора связок. $\{\bot ,\to \}$ для классической логики высказываний задается следующими четырьмя правилами:

{\frac {}{{\mathcal {G}}\mid \Gamma ,p\Rightarrow p,\Delta }}

{\frac {}{{\mathcal {G}}\mid \Gamma ,\bot \Rightarrow \Delta }}

{\frac {{\mathcal {G}}\mid \Gamma ,B\Rightarrow \Delta \qquad {\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }{{\mathcal {G}}\mid \Gamma ,A\to B\Rightarrow \Delta }}

${\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow B,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A\to B,\Delta }}$

Благодаря дополнительной структуре в гиперсеквенциальной постановке структурные правила рассматриваются во внутреннем и внешнем вариантах. Правила внутреннего ослабления и внутреннего сокращения представляют собой адаптацию соответствующих секвенциальных правил с добавленным гиперсеквенциальным контекстом:

{\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Sigma \Rightarrow \Delta ,\Pi }}

${\frac {{\mathcal {G}}\mid \Gamma ,A,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }}$

${\frac {{\mathcal {G}}\mid \Gamma \Rightarrow A,A,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }}$

Правила внешнего ослабления и внешнего сжатия — это соответствующие правила на уровне гиперсеквентных компонент, а не формул:

${\frac {\mathcal {G}}{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}$

${\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta \mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}$

Правильность этих правил тесно связана с интерпретацией формулы гиперсеквенциальной структуры, почти всегда как некоторой формы дизъюнкции . Точная интерпретация формулы зависит от рассматриваемой логики, некоторые примеры см. ниже.

Основные примеры [ править ]

Модальная логика [ править ]

Гиперсеквенции использовались для получения аналитических исчислений для модальных логик , для которых аналитические секвенционные исчисления оказались неуловимыми. В контексте модальной логики стандартная интерпретация формулы гиперсеквенции

\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}

это формула

\Box (\bigwedge \Gamma _{1}\to \bigvee \Delta _{1})\lor \dots \lor \Box (\bigwedge \Gamma _{n}\to \bigvee \Delta _{n})

Вот если $\Gamma$ это мультимножество $A_{1},\dots ,A_{n}$ мы пишем $\Box \Gamma$ для результата добавления префикса к каждой формуле в $\Gamma$ с $\Box$ , т. е. мультимножество $\Box A_{1},\dots ,\Box A_{n}$ . Обратите внимание, что отдельные компоненты интерпретируются с использованием стандартной интерпретации формулы для секвенций и полосы гиперсеквенций. $\mid$ интерпретируется как дизъюнкция коробок. Ярким примером модальной логики, для которой гиперсеквенции обеспечивают аналитическое исчисление, является логика S5 . В стандартном гиперсеквенциальном исчислении для этой логики ^[1] интерпретация формулы аналогична приведенной выше, а пропозициональные и структурные правила — те же, что и в предыдущем разделе. Кроме того, исчисление содержит модальные правила

{\frac {{\mathcal {G}}\mid \Box \Gamma \Rightarrow A}{{\mathcal {G}}\mid \Box \Gamma \Rightarrow \Box A}}

${\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Box A\Rightarrow \Delta }}$

${\frac {{\mathcal {G}}\mid \Box \Gamma ,\Sigma \Rightarrow \Box \Delta ,\Pi }{{\mathcal {G}}\mid \Box \Gamma \Rightarrow \Box \Delta \mid \Sigma \Rightarrow \Pi }}$

Приемлемость правильно сформулированной версии правила отсечения может быть показана путем синтаксического рассуждения о структуре выводов или путем демонстрации полноты исчисления без правила отсечения непосредственно с использованием семантики S5. В соответствии с важностью модальной логики S5 был сформулирован ряд альтернативных исчислений. ^[2]^[3]^[1]^[4]^[5]^[6]^[7] Гиперсеквенциальные исчисления также были предложены для многих других модальных логик. ^[6]^[7]^[8]^[9]

Промежуточная логика [ править ]

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

\Gamma _{1}\Rightarrow A_{1}\mid \dots \mid \Gamma _{n}\Rightarrow A_{n}

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

(\bigwedge \Gamma _{1}\to A_{1})\lor \dots \lor (\bigwedge \Gamma _{n}\to A_{n})

Большинство гиперсеквенциальных исчислений для промежуточных логик включают однопоследовательные версии пропозициональных правил, приведенных выше, и набор структурных правил. Характеристики конкретной промежуточной логики в основном фиксируются с помощью ряда дополнительных структурных правил . Например, стандартное исчисление для промежуточной логики LC , иногда также называемое логикой Гёделя – Даммета, дополнительно содержит так называемое правило связи: ^[1]

{\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Sigma \Rightarrow A\qquad \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Pi \Rightarrow B}{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Sigma \Rightarrow B\mid \Pi \Rightarrow A}}

Были введены гиперсеквентивные исчисления для многих других промежуточных логик. ^[1]^[10]^[11]^[12] и есть очень общие результаты об исключении разрезов в таких исчислениях. ^[13]

Субструктурная логика [ править ]

Что касается промежуточных логик, гиперсеквенции использовались для получения аналитических исчислений для многих субструктурных и нечетких логик . ^[1]^[13]^[14]

История [ править ]

Гиперсеквенциальная структура, по-видимому, впервые появилась в ^[2] под названием кортеж , чтобы получить исчисление для модальной логики S5 . Судя по всему, он был разработан независимо в ^[3] также для рассмотрения модальной логики и во влиятельных, ^[1] где рассматриваются исчисления для модальной, промежуточной и субструктурной логик и вводится термин гиперсеквенция.

Ссылки [ править ]

↑ Перейти обратно: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г Аврон, Арнон (1996). «Метод гиперсеквенций в теории доказательств пропозициональных неклассических логик». Логика: от основ к приложениям . стр. 1–32. ISBN 978-0-19-853862-2 .
↑ Перейти обратно: Перейти обратно: ^а ^б Минц, Григорий (1971). «О некоторых исчислениях модальной логики». Учеб. Стеклова. Из математики . 98 : 97–122.
↑ Перейти обратно: Перейти обратно: ^а ^б Поттинджер, Гаррелл (1983). «Единые формулировки T, S4 и S5 без разрезов (аннотация)». Дж. Симб. Бревно. 48 (3): 900.
^ Поджолези, Франческа (2008). «Простое секвенциальное исчисление без разрезов для модальной логики S5» (PDF) . Преподобный Симб. Бревно. 1 :3–15. дои : 10.1017/S1755020308080040 . S2CID 37437016 .
^ Рестолл, Грег (2007). Димитракопулос, Костас; Невельский, Людомир; Норманн, Даг; Стил, Джон Р. (ред.). «Сети доказательств для S5: секвенции и схемы модальной логики». Логический коллоквиум 2005 . Конспект лекций по логике. 28 : 151–172. дои : 10.1017/CBO9780511546464.012 . hdl : 11343/31712 . ISBN 9780511546464 .
↑ Перейти обратно: Перейти обратно: ^а ^б Курокава, Хиденори (2014). «Гиперсеквенционные исчисления для модальной логики, расширяющие S4». Новые рубежи искусственного интеллекта . Конспекты лекций по информатике. Том. 8417. стр. 51–68. дои : 10.1007/978-3-319-10061-6_4 . ISBN 978-3-319-10060-9 .
↑ Перейти обратно: Перейти обратно: ^а ^б Лахав, Ори (2013). «От свойств фрейма к гиперсеквенционным правилам в модальной логике». 2013 28-й ежегодный симпозиум ACM – IEEE по логике в информатике . стр. 408–417. дои : 10.1109/LICS.2013.47 . ISBN 978-1-4799-0413-6 . S2CID 221813 .
^ Инджейчак, Анджей (2015). «Устранимость разреза в гиперсеквенциальных исчислениях для некоторых модальных логик линейных фреймов». Письма об обработке информации . 115 (2): 75–81. дои : 10.1016/j.ipl.2014.07.002 .
^ Леллманн, Бьёрн (2016). «Гиперсеквенционные правила с ограниченным контекстом для пропозициональной модальной логики» . Теор. Вычислить. наук. 656 : 76–105. дои : 10.1016/j.tcs.2016.10.004 .
^ Чиабаттони, Агата ; Феррари, Мауро (2001). «Гиперсеквенциальные исчисления для некоторых промежуточных логик с ограниченными моделями Крипке». Дж. Лог. Вычислить. 11 (2): 283–294. дои : 10.1093/logcom/11.2.283 .
^ Чиабаттони, Агата ; Маффезиоли, Паоло; Спендиер, Лара (2013). Гальмиш, Дидье; Ларчи-Вендлинг, Доминик (ред.). «Гиперсеквенции и помеченные исчисления для промежуточной логики». Таблицы 2013 : 81–96.
^ Бааз, Матиас; Чиабаттони, Агата ; Фермюллер, Кристиан Г. (2003). «Гиперсеквенционные исчисления для логики Гёделя - обзор». Дж. Лог. Вычислить . 13 (6): 835–861. CiteSeerX 10.1.1.8.5319 . дои : 10.1093/logcom/13.6.835 .
↑ Перейти обратно: Перейти обратно: ^а ^б Чиабаттони, Агата ; Галатос, Николаос; Теруи, Казусигэ (2008). «От аксиом к аналитическим правилам неклассической логики». 2008 23-й ежегодный симпозиум IEEE по логике в информатике . стр. 229–240. CiteSeerX 10.1.1.405.8176 . дои : 10.1109/LICS.2008.39 . ISBN 978-0-7695-3183-0 . S2CID 7456109 .
^ Меткалф, Джордж; Оливетти, Никола; Габбай, Дов (2008). Теория доказательств нечеткой логики . Шпрингер, Берлин.

[:0-1] Перейти обратно: Перейти обратно: ^а ^б ^с ^д ^и ^ж ^г Аврон, Арнон (1996). «Метод гиперсеквенций в теории доказательств пропозициональных неклассических логик». Логика: от основ к приложениям . стр. 1–32. ISBN 978-0-19-853862-2 .

[:4-2] Перейти обратно: Перейти обратно: ^а ^б Минц, Григорий (1971). «О некоторых исчислениях модальной логики». Учеб. Стеклова. Из математики . 98 : 97–122.

[:5-3] Перейти обратно: Перейти обратно: ^а ^б Поттинджер, Гаррелл (1983). «Единые формулировки T, S4 и S5 без разрезов (аннотация)». Дж. Симб. Бревно. 48 (3): 900.

[4] Поджолези, Франческа (2008). «Простое секвенциальное исчисление без разрезов для модальной логики S5» (PDF) . Преподобный Симб. Бревно. 1 :3–15. дои : 10.1017/S1755020308080040 . S2CID 37437016 .

[5] Рестолл, Грег (2007). Димитракопулос, Костас; Невельский, Людомир; Норманн, Даг; Стил, Джон Р. (ред.). «Сети доказательств для S5: секвенции и схемы модальной логики». Логический коллоквиум 2005 . Конспект лекций по логике. 28 : 151–172. дои : 10.1017/CBO9780511546464.012 . hdl : 11343/31712 . ISBN 9780511546464 .

[:1-6] Перейти обратно: Перейти обратно: ^а ^б Курокава, Хиденори (2014). «Гиперсеквенционные исчисления для модальной логики, расширяющие S4». Новые рубежи искусственного интеллекта . Конспекты лекций по информатике. Том. 8417. стр. 51–68. дои : 10.1007/978-3-319-10061-6_4 . ISBN 978-3-319-10060-9 .

[:2-7] Перейти обратно: Перейти обратно: ^а ^б Лахав, Ори (2013). «От свойств фрейма к гиперсеквенционным правилам в модальной логике». 2013 28-й ежегодный симпозиум ACM – IEEE по логике в информатике . стр. 408–417. дои : 10.1109/LICS.2013.47 . ISBN 978-1-4799-0413-6 . S2CID 221813 .

[8] Инджейчак, Анджей (2015). «Устранимость разреза в гиперсеквенциальных исчислениях для некоторых модальных логик линейных фреймов». Письма об обработке информации . 115 (2): 75–81. дои : 10.1016/j.ipl.2014.07.002 .

[9] Леллманн, Бьёрн (2016). «Гиперсеквенционные правила с ограниченным контекстом для пропозициональной модальной логики» . Теор. Вычислить. наук. 656 : 76–105. дои : 10.1016/j.tcs.2016.10.004 .

[10] Чиабаттони, Агата ; Феррари, Мауро (2001). «Гиперсеквенциальные исчисления для некоторых промежуточных логик с ограниченными моделями Крипке». Дж. Лог. Вычислить. 11 (2): 283–294. дои : 10.1093/logcom/11.2.283 .

[11] Чиабаттони, Агата ; Маффезиоли, Паоло; Спендиер, Лара (2013). Гальмиш, Дидье; Ларчи-Вендлинг, Доминик (ред.). «Гиперсеквенции и помеченные исчисления для промежуточной логики». Таблицы 2013 : 81–96.

[12] Бааз, Матиас; Чиабаттони, Агата ; Фермюллер, Кристиан Г. (2003). «Гиперсеквенционные исчисления для логики Гёделя - обзор». Дж. Лог. Вычислить . 13 (6): 835–861. CiteSeerX 10.1.1.8.5319 . дои : 10.1093/logcom/13.6.835 .

[:3-13] Перейти обратно: Перейти обратно: ^а ^б Чиабаттони, Агата ; Галатос, Николаос; Теруи, Казусигэ (2008). «От аксиом к аналитическим правилам неклассической логики». 2008 23-й ежегодный симпозиум IEEE по логике в информатике . стр. 229–240. CiteSeerX 10.1.1.405.8176 . дои : 10.1109/LICS.2008.39 . ISBN 978-0-7695-3183-0 . S2CID 7456109 .

[14] Меткалф, Джордж; Оливетти, Никола; Габбай, Дов (2008). Теория доказательств нечеткой логики . Шпрингер, Берлин.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]