自然演绎与相继式演算
自然演绎和相继式演算是两种根岑（Gentzen）风格的形式系统，它们通过逻辑联结词的引入规则和消除规则来表示证明，构成了结构证明论的基本机制。
用 PaperMind 寻找选题即将推出Find papers & topics
Tools & resources
Learn & explore
视频即将推出
Definition
自然演绎使用引入规则和消除规则从假设中推导出公式，这些规则反映了非形式推理；而相继式演算则通过作用于蕴涵式左右两边的规则来操作相继式，即关于一组公式蕴涵另一组公式的断言。
Scope
本主题涵盖了自然演绎的规则及其引入和消除对、相继式演算的结构及其左右规则和结构规则、自然演绎的范式化、两种系统之间的关系，以及它们的直觉主义和经典变体。
Core questions
- 引入规则和消除规则如何赋予逻辑联结词意义？
- 什么是相继式？它的规则与自然演绎的规则有何不同？
- 范式化如何简化自然演绎证明？
- 这些演算的经典版本和直觉主义版本之间有何关系？
Key theories
- 引入规则和消除规则
- 每个联结词都受引入它的规则和利用它的规则的支配，它们的和谐性（即消除规则精确地恢复了引入规则所引入的内容）表达了联结词的意义。
- 范式化定理
- 普拉维茨（Prawitz）证明了自然演绎证明可以被简化为没有迂回的范式，其中引入操作不会立即被消除操作抵消，这与切除消除（cut-elimination）在自然演绎中的对应物。
- 两种演算的对应关系
- 自然演绎和相继式演算证明相同的定理，并且可以相互转换，其中相继式的左规则对应于自然演绎的消除规则。
Clinical relevance
这些演算系统是结构性研究证明的标准形式：自然演绎通过“证明即程序”的对应关系支撑着类型论和证明助手，而相继式演算在切除消除（cut-elimination）后具有子公式性质（subformula property），是自动化证明搜索和分析图（analytic tableaux）的基础。
History
根岑（Gentzen）于1934年和1935年分别引入了自然演绎和相继式演算。他在发现自然演绎难以分析后，设计了相继式演算以获得其切除消除定理。普拉维茨（Prawitz）于1965年通过深入的范式化研究复兴了自然演绎，这些系统成为后来“证明即程序”发展中的核心。
Key figures
- Gerhard Gentzen
- Dag Prawitz
- Stanislaw Jaskowski
- Jan von Plato
Related topics
Seminal works
- troelstra2000
- prawitz1965
- negri2001
Frequently asked questions
- 自然演绎和相继式演算之间有什么区别？
- 自然演绎在假设的上下文中处理公式，并使用消除规则，这与非形式证明非常吻合。相继式演算处理明确的蕴涵关系，并用左引入规则取代消除规则，这种格式使得切除消除（cut-elimination）和子公式性质（subformula property）更加透明。
- 范式化为什么重要？
- 范式证明不包含任何迂回，并具有子公式性质，因此其中的每个公式都是结论或前提的子公式。这限制了证明的形状，产生了相容性结果，并且通过“证明即程序”的对应关系，它对应于将程序评估为一个值。