Using Ramsey's Theorem Once

TL;DR

The paper investigates the proof-theoretic strength of Ramsey's Theorem for specific parameters within higher-order reverse mathematics, showing how classical logic influences provability.

Contribution

It demonstrates that RT(2,4) cannot be proved with a single application of RT(2,2) in an intuitionistic setting, but can be in classical logic, using advanced formalizations.

Findings

RT(2,4) unprovable with one RT(2,2) in intuitionistic RCA0 extension

Adding classical logic allows proving RT(2,4) from RT(2,2)

Uses Kohlenbach's axiomatization and Weihrauch reducibility formalization

Abstract

We show that RT(2,4) cannot be proved with one typical application of RT(2,2) in an intuitionistic extension of RCA0 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.