The subsystem WKL0 consists of RCA0 plus a weak form of Kőnig's lemma, namely the statement that every infinite subtree of the full binary tree (the tree of all finite sequences of 0's and 1's) has an infinite path. This proposition, which is known as "weak Kőnig's lemma", is easy to state in the language of second-order arithmetic. WKL0 can also be defined as the principle of Σ separation (given two Σ formulas of a free variable "n" which are exclusive, there is a class containing all "n" satisfying the one and no "n" satisfying the other).