A weak form of Kőnig's lemma which states that every infinite binary tree has an infinite branch is used to define the subsystem WKL0 of second-order arithmetic. This subsystem has an important role in reverse mathematics. Here a binary tree is one in which every term of every sequence in the tree is 0 or 1, which is to say the tree is computably bounded via the constant function 2. The full form of Kőnig's lemma is not provable in WKL0, but is equivalent to the stronger subsystem ACA0.