A Model Theory for R-calculus without Cut

ABSTRACT. In this paper, we propose a model theory for R-calculus without cut. First, validity of R-transitions and R-transition sequences is defined using models of first-order languages. Then reducibility of R-transition sequences is defined and it is proved that every R-transition sequence, which transits to an R-termination, can be reduced to an irreducible R-transition sequence. Finally, the soundness and completeness of R-calculus is redefined. And R-calculus without cut is proved to still be sound and complete.