Study on R-Calculus

The R-calculus, proposed by professor Li Wei, is a revision calculus for formal theories. It plays a key role in OPEN and GUINA logic. It can be considered as a tool to cut out the prerequisites of contradiction when a theory conflicts with some facts, hence resulting in a consistent sub-theory. In order to give a purely syntactic calculus, we make a deep exploration of the concept “necessary prerequisite”, and characterize it in three different ways. Furthermore, R-terminated sets and the maximally consistent subsets are also studied. The first way is a logical consequence of original R-calculus. And the second one is based on maximally consistent subset. The third one is an inductive formalization of R-prerequisite. By comparing these ways, we claim that each way has its own advantages and disadvantages. We chose the last one as our approach to derive a sound and relatively complete calculus, namely R′, which could be a better system for original purpose. The lower bound and upper bound of R-terminated sets are proposed. And we prove that deriving maximally consistent subsets of contradiction is not only non-recursive but even not recursive enumerable, which indicates that any purely syntactic system are not able to be both sound and complete.