 The resulting first-order formula is equivalent to \(\mathtt{\neg R(a, a)}\) which shows that \(\mathtt{{\downarrow} c\Box \neg c}\) indeed does correspond to the accessibility relation being irreflexive, cf. above.