Choice principles characterizing the difference between König’s lemma and weak König’s lemma in constructive reverse mathematics
Makoto Fujiwara, Takako Nemoto · Computability · 2024
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.