A constructive analysis of RM

The system RM is the most well-understood (and to our opinion, also the most important) system among the logics developed by the Anderson and Belnap school. In this paper we investigate RM from a constructive point of view. For example, we give a new proof of the completeness of RM relative to the Sugihara matrix (first shown by Meyer), a proof in which a p.r. procedure is presented, applying which to a sentence A in RM language yields either a proof of it in RM or a refuting valuation for it in the Sugihara matrix S Z . Two topics dealt with in this work deserve a special attention. a) The admissibility of γ . This is a famous theorem of Meyer and Dunn. In 1 Anderson and Belnap emphasize that “the Meyer-Dunn argument … guarantees the existence of a proof of B , but there is no guarantee that the proof of B is related in any sort of plausible way to the proofs of A and Ā ∨ B .” In §2 we provide such a guarantee for the RM -case. In fact, we give there a direct method of obtaining a proof of B from given proofs of A and Ā ∨ B . b) The relationships between RM and its full negation-implication fragment . RM is known (1, pp. 148–149, and 3) to be a conservative extension of (Sobociński 3-valued logic; see 4). Anderson and Belnap admit 1, p. 149 that this fact came to them as a distinct surprise, since RM as a whole is far from being three-valued. In this paper, however, this “surprising” fact appears quite natural (see III.3). In fact, we show that , is the “hard core” of RM , since our proof of the completeness of RM is based in an essential way on the completeness of relative to the Sobociński matrix, and since the Gentzen-type calculus we develop for RM is a direct extension of a similar (but much simpler) calculus for . Because of the importance has in this work, we devote the first section to a constructive investigation of it. We note, finally, that the Gentzen-type calculus mentioned above admits cut-elimination and normal-form techniques. (Such calculi were found till now only for RM without distribution.)