Published online by Cambridge University Press: 12 March 2014
With all seven of ‘∼’, ‘⊃’, ‘&’, ‘ν’, ‘≡’, ‘∀’, and ‘∃’ understood to serve as primitive signs, let an expression of the sort
A1, A2, … , An → B1, B2, … , Bm,
where A1, A2, …, Aη (η≥ 0), B1, B2, …, and Bm (m > 0 if n = 0, otherwise m ≥ 0) are wffs of the first-order quantificational calculus (QC), count as an L-sequent of QC; let an L-sequent of QC of the sort
A1, A2, … , An → B
count as an N-sequent of QC;2 and let an L-sequent S of QC count as a Gentzen L-sequent of QC if no individual variable of QC occurs both bound and free in S.