Rule-Generation Theorem and its Applications
Bulletin of the Section of Logic, Tome 47 (2018) no. 4
In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some case studies for illustration.
Keywords:
sequent calculus, cut elimination, proof theory, extralogical rules
@article{BSL_2018_47_4_a3,
author = {Indrzejczak, Andrzej},
title = {Rule-Generation {Theorem} and its {Applications}},
journal = {Bulletin of the Section of Logic},
year = {2018},
volume = {47},
number = {4},
language = {en},
url = {http://geodesic.mathdoc.fr/item/BSL_2018_47_4_a3/}
}
Indrzejczak, Andrzej. Rule-Generation Theorem and its Applications. Bulletin of the Section of Logic, Tome 47 (2018) no. 4. http://geodesic.mathdoc.fr/item/BSL_2018_47_4_a3/