Analytic cut
1969; Cambridge University Press; Volume: 33; Issue: 4 Linguagem: Inglês
10.2307/2271362
ISSN1943-5886
Autores Tópico(s)Logic, programming, and type systems
ResumoThe 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.
Referência(s)