Analytic cut
- 1 January 1969
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 33 (4), 560-564
- https://doi.org/10.2307/2271362
Abstract
The real importance of cut-free proofs is not the elimination of cuts per se, but rather that such proofs obey the subformula principle. In this paper we accomplish this latter objective in a different manner.In the usual formulations of Gentzen systems, there is only one axiom scheme; all the other postulates are inference rules. By contrast, we consider here some Gentzen type axiom systems for propositional logic and Quantification Theory in which there is only one inference rule; all the other postulates are axiom schemes. This admits of an unusually elegant axiomatization of logic.Keywords
This publication has 3 references indexed in Scilit:
- Gerhard Gentzen. Investigations into logical deduction. English translation of 4422 by M. E. Szabo. American philosophical quarterly, vol. 1 (1964), pp. 288–306, and vol. 2 (1965), pp. 204–218. - Paul Bernays. Introduction. Therein, vol. 1, p. 288.The Journal of Symbolic Logic, 1970
- Uniform Gentzen systemsThe Journal of Symbolic Logic, 1969
- Introduction to Metamathematics. By S. C. Kleene. Pp. x, 550, Fl. 32.50. 1952. (Noordhoff, Groningen; North-Holland Publishing Co., Amsterdam)The Mathematical Gazette, 1954