Введение
В математической логике структурная теория доказательств — это подраздел теории доказательств, изучающий доказательственные исчисления, поддерживающие понятие аналитического доказательства, разновидность доказательства, семантические свойства которого явно выражены. Если все теоремы логики, формализованной в структурной теории доказательств, имеют аналитические доказательства, то эта теория доказательств может быть использована для демонстрации таких свойств, как непротиворечивость, предоставления процедур доказывания и выделения математических или вычислительных свидетельств, соответствующих теоремам – задача, которая чаще решается с помощью теории моделей.
Аналитическое доказательство
Понятие аналитического доказательства было введено в теорию доказательств Герхардом Гентценом для исчисления секвенций; аналитические доказательства — это доказательства, не содержащие отсечений. Его исчисление натуральных выводов также поддерживает понятие аналитического доказательства, как показал Даг Правиц; определение несколько сложнее — аналитические доказательства — это нормальные формы, которые связаны с понятием нормальной формы в переписывании термов.
Структуры и соединители
Термин "структура" в теории структурных доказательств происходит от технического понятия, введенного в исчислении секвенций: исчисление секвенций представляет суждение, сделанное на любой стадии вывода, с использованием специальных, дополнительных логических операторов, называемых структурными операторами: в , запятые слева от символа секвенции обычно интерпретируются как конъюнкции, запятые справа – как дизъюнкции, а сам символ секвенции интерпретируется как импликация. Однако важно отметить, что существует принципиальная разница в поведении между этими операторами и логическими связками, которыми они интерпретируются в исчислении секвенций: структурные операторы используются во всех правилах исчисления и не принимаются во внимание при проверке применимости свойства подформулы. Более того, логические правила действуют только в одном направлении: логическая структура вводится логическими правилами и не может быть удалена после создания, в то время как структурные операторы могут вводиться и удаляться в процессе вывода. Идея рассматривать синтаксические особенности секвенций как специальные, нелогические операторы относительно нова и была обусловлена инновациями в теории доказательств: когда структурные операторы так же просты, как в оригинальном исчислении секвенций Гетцена, необходимости в их анализе немного, но доказательные исчисления глубокого вывода, такие как логика отображений (введенная Нуэлем Белнапом в 1982 году), поддерживают структурные операторы, столь же сложные, как логические связки, и требуют сложной обработки.
Вложенный последовательный вычисление
Вложенное секвенциальное исчисление — это формализация, напоминающая двустороннее исчисление структур.