From the conceptual viewpoint, many mathematical propositions implicitly contain at least two kinds of principle. One is a logical principle such as the law-of-excluded-middle or De Morgan's law. Another is a function-existence principle. For both conceptual and practical reasons, it is an interesting enterprise to calibrate how amount of logical and function-existence principles are implicit in mathematical theorems and axioms. This is the topic of constructive reverse mathematics, which specifies necessary and sufficient axioms to prove each mathematical proposition constructively. In this paper, we decompose weak König's lemma with a uniqueness hypothesis [Formula: see text] by Moschovakis, into logical and function-existence principles in a recent framework of constructive reverse mathematics. This article is part of the theme issue 'Modern perspectives in Proof Theory'.
Keywords: constructive reverse mathematics; decomposition; unique choice; uniqueness hypothesis; weak König’s lemma.