Article contents
Subformula theorems for N-sequents
Published online by Cambridge University Press: 12 March 2014
Extract
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.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1968
References
- 1
- Cited by