相继式演算
数学术语
证明论数理逻辑中,相继式演算(又译矢列演算、矢列式演算)是众所周知的一阶逻辑(和作为它的特殊情况的命题逻辑)的演绎系统。这个系统也叫做LK系统,用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是Gentzen系统。
简介
证明论数理逻辑中,相继式演算(又译矢列演算、矢列式演算)是众所周知的一阶逻辑(和作为它的特殊情况的命题逻辑)的演绎系统。这个系统也叫做LK系统,用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是Gentzen系统。
相继式演算LK由Gerhard Gentzen介入为研究自然演绎的工具。它已经变成构造逻辑推导的非常有用的演算。它的名字得来自德语的Logischer Kalkül
自然演绎
数理逻辑中,自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。这种方式对比于使用公理公理系统
相继式
证明论中,相继式是对在规定演绎演算的时候经常用到的可证明性的形式陈述。
相继式有如下形式
这里的Γ和Σ二者是逻辑公式的序列(就是说公式的数目和出现次序都是重要的)。符号
参见
参考资料
最新修订时间:2022-08-25 16:33
目录
概述
简介
自然演绎
参考资料