Структурная теория доказательства

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

Аналитическое доказательство [ править ]

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

Структуры и связи [ править ]

Термин «структура» в теории структурных доказательств происходит от технического понятия, введенного в секвенциальное исчисление: секвенциальное исчисление представляет собой суждение, сделанное на любом этапе вывода с использованием специальных, экстралогических операторов, называемых структурными операторами: $A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}$ , запятые слева от турникета — это операторы, обычно интерпретируемые как союзы, справа — как дизъюнкции, а сам символ турникета интерпретируется как импликация. Однако важно отметить, что существует фундаментальное различие в поведении этих операторов и логических связок, с помощью которых они интерпретируются в секвенциальном исчислении: структурные операторы используются в каждом правиле исчисления и не учитываются при вопросе, является ли применяется свойство подформулы. Более того, логические правила действуют только в одном направлении: логическая структура вводится логическими правилами и не может быть устранена после создания, тогда как структурные операторы могут вводиться и устраняться в процессе вывода.

Идея рассматривать синтаксические особенности секвенций как специальные, нелогические операторы не стара и возникла благодаря нововведениям в теории доказательств: когда структурные операторы столь же просты, как в исходном секвенционном исчислении Гетцена, нет необходимости их анализировать. , но доказывают исчисления глубокого вывода, такие как логика отображения (введенная Нуэлем Белнапом в 1982 году) ^[1] поддерживают структурные операторы, столь же сложные, как и логические связи, и требуют сложной обработки.

Отсечение-исключение секвенциальном исчислении в

формул- типов соответствие Естественная дедукция и

Логическая двойственность и гармония [ править ]

Гиперсеквенции [ править ]

Структура гиперсеквенции расширяет обычную структуру секвенций до мультимножества секвенций, используя дополнительную структурную связку | (называемая полосой гиперсеквенции ) для разделения различных секвенций. Он использовался для предоставления аналитических вычислений, например, для модальной , промежуточной и субструктурной логики. ^[2]^[3]^[4] Гиперсеквенция – это структура

$\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}$

где каждый $\Gamma _{i}\vdash \Delta _{i}$ является обычной секвенцией, называемой компонентой гиперсеквенции. Что касается секвенций, гиперсеквенции могут быть основаны на множествах, мультимножествах или последовательностях, а компоненты могут быть секвенциями с одним или несколькими выводами . Формульная интерпретация гиперсеквенций зависит от рассматриваемой логики, но почти всегда представляет собой некоторую форму дизъюнкции. Наиболее распространенные интерпретации представляют собой простое дизъюнкцию.

$(\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})$

для промежуточной логики или как дизъюнкция коробок

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

для модальной логики.

В соответствии с дизъюнктивной интерпретацией гиперсеквенционной полосы, по существу, все гиперсеквентивные исчисления включают внешние структурные правила , в частности правило внешнего ослабления.

${\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma \vdash \Pi }}$

и правило внешнего сокращения

${\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}}$

Дополнительную выразительность гиперсеквенциальной структуры обеспечивают правила, управляющие гиперсеквенциальной структурой. Важным примером является модализованное правило разделения. ^[3]

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

для модальной логики S5 , где $\Box \Sigma$ означает, что каждая формула в $\Box \Sigma$ имеет форму $\Box A$ .

Другой пример – правило связи для промежуточной логики LC. ^[3]

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

Обратите внимание, что в правиле связи компоненты представляют собой последовательности с одним выводом.

Исчисление структур [ править ]

Вложенное секвенционное исчисление [ править ]

Вложенное секвенциальное исчисление — это формализация, напоминающая двустороннее исчисление структур.

Примечания [ править ]

^ Н. Д. Белнап. «Показать логику». Журнал философской логики , 11 (4), 375–417, 1982.
^ Минк, Г. Е. (1971) [Впервые опубликовано на русском языке в 1968 г.]. «О некоторых исчислениях модальной логики» . Исчисления символической логики. Известия Математического института им. Стеклова . 98 . АМС: 97–124.
↑ Перейти обратно: Перейти обратно: ^а ^б ^с Аврон, Арнон (1996). «Метод гиперсеквенций в теории доказательств пропозициональных неклассических логик» (PDF) . Логика: от основ к приложениям: Европейский коллоквиум по логике . Кларендон Пресс: 1–32.
^ Поттинджер, Гаррел (1983). «Единые формулировки T, S4 и S5 без разрезов». Журнал символической логики . 48 (3): 900. дои : 10.2307/2273495 . JSTOR 2273495 . S2CID 250346853 .

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

Сара Негри ; Ян фон Платон (2001). Структурная теория доказательств . Издательство Кембриджского университета. ISBN 978-0-521-79307-0 .
Энн Сьерп Трульстра ; Хельмут Швихтенберг (2000). Основная теория доказательств (2-е изд.). Издательство Кембриджского университета. ISBN 978-0-521-77911-1 .

[1] Н. Д. Белнап. «Показать логику». Журнал философской логики , 11 (4), 375–417, 1982.

[2] Минк, Г. Е. (1971) [Впервые опубликовано на русском языке в 1968 г.]. «О некоторых исчислениях модальной логики» . Исчисления символической логики. Известия Математического института им. Стеклова . 98 . АМС: 97–124.

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

[4] Поттинджер, Гаррел (1983). «Единые формулировки T, S4 и S5 без разрезов». Журнал символической логики . 48 (3): 900. дои : 10.2307/2273495 . JSTOR 2273495 . S2CID 250346853 .

[1]

[2]

[3]

[4]