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

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

Содержание

• 1 Аналитическое доказательство
• 2 Конструкции и связки
• 3 Устранение разрезов в последовательном исчислении
• 4 Естественная дедукция и соответствие формул как типов
• 5 Логическая двойственность и гармония
• 6 гиперсеквентов
• 7 Расчет конструкций
• 8 Вложенное последовательное исчисление
• 9 Примечания
• 10 Ссылки

Аналитическое доказательство

Основная статья: Аналитическое доказательство

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

Структуры и связки

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

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

Исключение отсечения в последовательном исчислении

Основная статья: Cut-elimination

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

Основная статья: Естественная дедукция

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

Основная статья: Логическая гармония

Гиперсеквенты

Основная статья: Hypersequent

Каркас гиперсеквенции расширяет структуру обычной секвенции до мультимножества секвенций, используя дополнительную структурную связку | (называется гиперпоследовательной полосой ) для разделения различных секвенций. Он использовался для обеспечения аналитических вычислений, например, для модальных, промежуточных и субструктурных логик. Гиперсеквенция - это структура.

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

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

${\ 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 _ { n})}$

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

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

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

и правило внешнего сжатия

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

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

${\ 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 \ Сигма \ vdash \ Box \ Pi \ mid \ Omega \ vdash \ Theta}}}$

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

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

${\ 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 \ Сигма _ {м} \ vdash \ Pi _ {m} \ mid \ Omega \ vdash B \ mid \ Theta \ vdash A}}}$

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

Расчет конструкций

Основная статья: Расчет структур

Вложенное последовательное исчисление

Основная статья: Вложенное последовательное исчисление

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

Ноты

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

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