{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T23:03:26Z","timestamp":1781046206114,"version":"3.54.1"},"reference-count":5,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":9598,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1987,12]]},"abstract":"The system RM<\/jats:bold> 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<\/jats:bold> from a constructive point of view. For example, we give a new proof of the completeness of RM<\/jats:bold> 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<\/jats:italic> in RM<\/jats:bold> language yields either a proof of it in RM<\/jats:bold> or a refuting valuation for it in the Sugihara matrix SZ<\/jats:sub><\/jats:italic>.<\/jats:p>Two topics dealt with in this work deserve a special attention.<\/jats:p>a) The admissibility of \u03b3<\/jats:italic>. This is a famous theorem of Meyer and Dunn. In [1] Anderson and Belnap emphasize that \u201cthe Meyer-Dunn argument \u2026 guarantees the existence of a proof of B<\/jats:italic>, but there is no<\/jats:italic> guarantee that the proof of B<\/jats:italic> is related in any sort of plausible way to the proofs of A<\/jats:italic> and \u0100<\/jats:italic> \u2228 B<\/jats:italic>.\u201d In \u00a72 we provide such a guarantee for the RM<\/jats:bold>-case. In fact, we give there a direct method of obtaining a proof of B<\/jats:italic> from given proofs of A<\/jats:italic> and \u0100<\/jats:italic> \u2228 B<\/jats:italic>.<\/jats:p>b) The relationships between<\/jats:italic>RM<\/jats:bold>and its full negation-implication fragment<\/jats:italic>. RM<\/jats:bold> is known ([1, pp. 148\u2013149], and [3]) to be a conservative extension of (Soboci\u0144ski 3-valued logic; see [4]). Anderson and Belnap admit [1, p. 149] that this fact came to them as a distinct surprise, since RM<\/jats:bold> as a whole is far from being three-valued. In this paper, however, this \u201csurprising\u201d fact appears quite natural (see III.3). In fact, we show that , is the \u201chard core\u201d of RM<\/jats:bold>, since our proof of the completeness of RM<\/jats:bold> is based in an essential way on the completeness of relative to the Soboci\u0144ski matrix, and since the Gentzen-type calculus we develop for RM<\/jats:bold> 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.<\/jats:p>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<\/jats:bold> without distribution.)<\/jats:p>","DOI":"10.2307\/2273828","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:23:41Z","timestamp":1146939821000},"page":"939-951","source":"Crossref","is-referenced-by-count":92,"title":["A constructive analysis of RM<\/b>"],"prefix":"10.1017","volume":"52","author":[{"given":"Arnon","family":"Avron","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200029339_ref003","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093894720"},{"key":"S0022481200029339_ref001","volume-title":"Entailment","volume":"1","author":"Anderson","year":"1975"},{"key":"S0022481200029339_ref005","first-page":"900","volume":"48","author":"Pottinoer","year":"1983","journal-title":"Uniform, cut-free formulations of T, S4 and S5"},{"key":"S0022481200029339_ref002","first-page":"334","volume":"49","author":"Avron","year":"1984","journal-title":"Relevant entailment\u2014semantics and formal systems"},{"key":"S0022481200029339_ref004","first-page":"23","article-title":"Axiomatization of a partial system of three-valued calculus of propositions","volume":"1","author":"Soboci\u0144ski","year":"1952","journal-title":"Journal of Computing Systems"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200029339","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T17:16:57Z","timestamp":1558372617000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200029339\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,12]]},"references-count":5,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1987,12]]}},"alternative-id":["S0022481200029339"],"URL":"https:\/\/doi.org\/10.2307\/2273828","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1987,12]]}}}