相继式

相继式((sequent)一种条件蕴含式.设r，o是有穷公式序列.那么r->。称为一个相继式.r和乙分别称为这个相继式的前项和后项.如果r为山，Az，... Cams。为Bl}jjZ}...}g‑(m，n妻1)，那么r}0(即A}，Az，...}Am->B1，BZ，...，8})表示若A:八AZ八…八A。成立，则B，VBzV"'VB，成立.A‑Az，" ，Am~意义为A，八A:八，…，八A。