补充资料：矢列式演算

矢列式演算
sequent calculus

矢列式演算[se妙时e川a目us:ce姗朋”盛。e叹，e爬“He] 谓词演算(Predicate calculus)的表述形式之一由于便于表示推导，矢列式演算在证明论(pIDof theo-ry)，数学基础以及推理的自动搜索等方面有着广泛的应用.矢列式演算是由G.Gentzen于1934年引进的(见fll).下面以矢列式演算的形式给出一种经典谓词演算. 公式集(c0Dection of form此派s)是某一逻辑一数学语言O的有限公式集r，其中允许公式重复.r中公式的次序不是本质的，但对每个公式，需要给出它在r中的重复数目.公式集可以是空集.集合切r是集合r加上公式价的一个重复.对两个公式集r和△，形式r~△称为一个矢列式(seql￡nt);r称为矢列式的前项(antecedent)，△为后项(successor). 矢列式演算公理的形式为价r~八价，其中r，△是任意公式集，毋是任何原子的(基本的)公式，演算的推导法则具有很对称的结构;由下列模式引人逻辑连接词: ‘八一卜而整备括会了 卜八)工二卫业生二二渔坐二 r~△(价八沙) (v一、空J二立生。红止乙色: (价V沙)r~△ 卜V)-止吐立竺里也一二 ’r~△(中丫沙)’ ‘卫一，气纸笋沪; ‘一夕片粤箭岩衍; 卜卜工二址勺七;卜们卫旦二立一: ’，毋r~A’、’了r~△，中’ 浑一、兰型坐妞因工二生鳖_ 丫戈沪r~△‘一丫片代撬箭而 门~)一一里卫二生-一; 日x中(y lx)r~△ 卜日)工;华望工典华丝.. r~△日x中在法则(~丫)和(日~)中，假定变元夕在r或么中不是自由的，x在职中不是自由的. 矢列式演算等价于通常形式的谓词演算，这是指一个公式职在谓词演算中可推导，当且仅当矢列式一~甲在矢列式演算中可推导.Gentzen基本定理((尧n-tZen丘田clamentalthe。恤)(或正规化定理(norrr以li-za七on theo比nl))对于证明这一点是基本的;这个定理可以陈述如下:如果矢列式r~△中和中r~八在矢列式演算中都可推导，则r~△也可推导.推导法则 r一，△职;价r~△ r一，△称为截法则(cutn习e)，正规化定理是说:在矢列式演算中允许截法则，或者加上截法则不改变可推导矢列式的集合.因此，Gent欢n定理也称为截消定理(cut·cl运止扭tion lheo化rn). 矢列式演算的对称结构对于其性质的研究提供了很大的方便.因此，在证明论中占有重要位置的是寻找应用演算的矢列式形式:算术，分析，类型论以及在演算中证明某种形式的截消除定理(见f2]，f31).许多基于非经典逻辑的演算中也有矢列式形式:直觉主义逻辑、模态逻辑、相关逻辑，以及其他逻辑(见【31，!4]).L种汪I直观地，矢列式r~△表示:如果r中所有公式成立，则△中至少必有一个公式也成立.

说明：补充资料仅用于学习参考，请勿用于其它任何用途。