A~specialization of Gentzen-type deductions and its application

V. P. Orevkov

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part V, Tome 32 (1972), pp. 98-104

Résumé

Let $S$ be a sequent, $M$ be some class of formula occurences in $S$ and let $D$ be a proof of $S$ in Gentzen-type system (classical on intuitionistic). A logical inference $L$ in $D$ is said to adjoin to $M$ through the premise $U$ if all side formulas of $L$ in $U$ belong to $M$. $U$ is called then a $M$-premise of $L$. $L$ is said to conform to $M$ if $L$ adjoins to $M$, and all logical inferences above any $M$-premise of $L$ belong to the side formulas of $L$. $D$ conforms to $M$ if all logical inferences adjoining to $M$ conform to $M$. We prove that under certain rather broad syntactical conditions it is possible to transform every proof into a proof of the same sequent conforming to $M$. The obtained results could be applied to the construction of cut-free variants of some axiomatic theories and to proof procedures for the predicate calculus (classical or intuitionistic).