The first axiomatization of relevant logic (Q1206805)

This paper presents a survey review of a much neglected, but historically most interesting paper by the Russian \textit{I. E. Orlov} [Mat. Sb. 35, 263-286 (1928; JFM 54.0054.03)]. In that paper Orlov formulated the first known axiomatization of relevance logic, in particular the implication- negation fragment of the Anderson-Belnap system \(R\). Orlov considered this a `calculus of compatibility' (in modern terms, intensional conjunction) where compatibility is to be defined by means of the given implication and negation, and thus requires a connection of meaning. He consciously rejected the paradoxes of material implication, \(A\to.B\to A\), and \(A\to.\neg A\to B\). In addition to his axiomatization for relevant implication and negation, Orlov also presented the earliest formulation of what is now the standard form for postulates for modal \(S4\) which he adjoined to his axioms for implication and negation. His purpose was to capture formally Brouwer's intuitionistic principles of assertability and negation through interpreting the modal `necessity' operator as provability. Orlov thus anticipated Gödel's later translation of intuitionistic logic into classical \(S4\). (The present paper translates Orlov's formulations into modern notation, and compares his results with later counterparts).