Натуральный вывод и исчисление секвенций

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

Definition

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

Scope

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

Core questions

• Как правила введения и удаления придают смысл логическим связкам?
• Что такое секвенция и чем ее правила отличаются от правил натурального вывода?
• Как нормализация упрощает доказательства натурального вывода?
• Как связаны классическая и интуиционистская версии этих исчислений?

Key theories

Правила введения и удаления

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

Теорема о нормализации

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

Соответствие двух исчислений

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

Clinical relevance

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

History

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

Key figures

• Gerhard Gentzen
• Dag Prawitz
• Stanislaw Jaskowski
• Jan von Plato

Seminal works

• troelstra2000
• prawitz1965
• negri2001

Frequently asked questions

В чем разница между натуральным выводом и исчислением секвенций?

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

Почему нормализация важна?

Нормальное доказательство не содержит обходных путей и обладает свойством подформулы, поэтому каждая формула в нем является подформулой заключения или посылок. Это ограничивает форму доказательств, дает результаты непротиворечивости и, через соответствие «доказательства как программы», соответствует вычислению программы до значения.