相繼式

相繼式((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。是恆假式;-}B‑Bz,...,8，意義為B,VBzV…VB，是恆真式.