In the context of constructive reverse mathematics, we characterize the difference between König’s lemma and weak König’s lemma by a particular fragment of the countable choice principle. Specifically, we show that König’s lemma can be decomposed into weak König’s lemma and the choice principle over a weak intuitionistic two-sorted arithmetic.
BergerJ.IshiharaH., Brouwer’s fan theorem and unique existence in constructive analysis, Mathematical Logic Quarterly51(4) (2005), 360–364. doi:10.1002/malq.200410038.
2.
BergerJ.IshiharaH.KiharaT.NemotoT., The binary expansion and the intermediate value theorem in constructive reverse mathematics, Arch. Math. Logic58(1–2) (2019), 203–217. doi:10.1007/s00153-018-0627-2.
3.
FujiwaraM., Intuitionistic and uniform provability in reverse mathematics, PhD thesis, Tohoku University, 2015.
4.
FujiwaraM., König’s lemma, weak König’s lemma, and the decidable fan theorem, Mathematical Logic Quarterly67(2) (2021), 241–257. doi:10.1002/malq.202000020.
5.
FujiwaraM., An extension of the equivalence between Brouwer’s fan theorem and weak König’s lemma with a uniqueness hypothesis, in: Revolutions and Revelations in Computability, BergerU.FranklinJ.N.Y.ManeaF.PaulyA., eds, Springer International Publishing, Cham, 2022, pp. 115–124. doi:10.1007/978-3-031-08740-0_10.
6.
IshiharaH., Constructive reverse mathematics: Compactness properties, in: From Sets and Types to Topology and Analysis, Oxford Logic Guides, Vol. 48, Oxford Univ. Press, Oxford, 2005, pp. 245–267. doi:10.1093/acprof:oso/9780198566519.003.0016.
7.
MoschovakisJ.R., Another unique weak König’s lemma, in: Logic, Construction, Computation, Ontos Mathematical Logic, BergerU.DienerH.SchusterP.SeisenbergerM., eds, De Gruyter, Berlin, Boston, 2012, pp. 343–352. doi:10.1515/9783110324921.343.
8.
NemotoT., Systems for constructive reverse mathematics, in: Handbook of Constructive Mathematics, Encyclopedia of Mathematics and Its Applications, BridgesD.IshiharaH.RathjenM.SchwichtenbergH., eds, Cambridge University Press, 2023, pp. 661–699. doi:10.1017/9781009039888.025.
9.
SchwichtenbergH., A direct proof of the equivalence between Brouwer’s fan theorem and König’s lemma with a uniqueness hypothesis, Journal of Universal Computer Science11(12) (2005), 2086–2095. doi:10.3217/jucs-011-12-2086.
10.
SimpsonS.G., Subsystems of Second Order Arithmetic. Perspectives in Logic, 2nd edn, Cambridge University Press, Cambridge, 2009.
11.
TroelstraA.S. (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, Vol. 344, Springer-Verlag, Berlin, New York, 1973.
