Using Ramsey's Theorem Once
Logic
2020-07-24 v5
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.
Cite
@article{arxiv.1611.03134,
title = {Using Ramsey's Theorem Once},
author = {Jeffry L. Hirst and Carl Mummert},
journal= {arXiv preprint arXiv:1611.03134},
year = {2020}
}
Comments
Revised June 1, 2017. Added pointer to published article and included a corrigendum correcting Definition 1