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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle {\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 \Пи }}}$

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

${\displaystyle {\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}}}}$

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

${\displaystyle {\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 , где означает, что каждая формула в имеет вид .${\displaystyle \Box \Sigma }$${\displaystyle \Box \Sigma }$${\displaystyle \Коробка A}$

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

${\displaystyle {\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 \Тета \vdash A}}}$

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

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

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

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