Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-22T16:30:31.569Z Has data issue: false hasContentIssue false

Subformula theorems for N-sequents

Published online by Cambridge University Press:  12 March 2014

Hugues Leblanc*
Affiliation:
Temple University

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
Copyright
Copyright © Association for Symbolic Logic 1968

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

[1]Bernays, P., Betrachtungen zum Sequenzen-Kalkul, Contributions to logic and methodology in honor of J. M. Bocheński, Tymieniecka, A.-T., ed., North-Holland, Amsterdam, 1965, pp. 144.Google Scholar
[2]Gentzen, G., Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1934), pp. 176210, 403–431.CrossRefGoogle Scholar
[3]Gentzen, G., Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathemathehe Annalen, vol. 112 (1936), pp. 493565.CrossRefGoogle Scholar
[4]Kanger, S., Provability in logic, Almquist and Wiksell, Stockholm, 1957.Google Scholar
[5]Leblanc, H., Techniques of deductive inference, Prentice-Hall, Englewood Cliffs, N.J., 1966.Google Scholar
[6]Prawitz, D., Natural deduction, A proof-theoretical study, Almquist and Wiksell, Stockholm, 1965.Google Scholar