 Well, first, the consequence relation ⊢R needs to be explained. Blok and Pigozzi have in mind the least consequence relation for which φ, φ → ψ ⊢ ψ and φ, ψ⊢ φ ∧ ψ and ⊢ φ for all φ provable in the Fmla logic R. (This third condition can be restricted to all axioms of any axiomatization of R with formula-to-formula rules corresponding to the first and second conditions.) Now the loose summary just given to the effect that every formula is equivalent to an equivalence makes a misleading double use of the equivalence vocabulary for two different things: equivalence as mutual consequence (“⊣⊢”) and equivalence as the biconditional connective. Removing the conflation, it means that for every φ there exist ψ, χ, with φ ⊣⊢Rψ ↔  χ.[49]  This is a very different matter from having ⊢Rφ ↔(ψ ↔ χ). The latter would indeed be equivalent to the provability in the sequent calculus described for R in Section  3  of φ ≻ ψ ↔ χ and the converse sequent. But the apparently matching ⊢R-statements mean something very different, building in the structural features (such as weakening) that the substructural sequent calculus was designed to avoid. Note in particular that ⊢R is not →-introductive, in the sense of Example 2 above.