Using Ramsey’s theorem once

We show that 𝖱𝖳 (2,4) cannot be proved with one typical application of 𝖱𝖳 (2,2) in an intuitionistic extension of 𝖱𝖢𝖠_0 to higher types, but that this does not remain true when the law of the excluded middle is added. The argument uses Kohlenbach’s axiomatization of higher order reverse mathematics, results related to modified reducibility, and a formalization of Weihrauch reducibility.