Editing Reverse mathematics (section)

=== Weak Kőnig's lemma WKL<sub>0</sub>===

The subsystem WKL<sub>0</sub> consists of RCA<sub>0</sub> 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. WKL<sub>0</sub> can also be defined as the principle of &Sigma;{{su|p=0|b=1}} separation (given two &Sigma;{{su|p=0|b=1}} formulas of a free variable ''n'' that are exclusive, there is a set containing all ''n'' satisfying the one and no ''n'' satisfying the other). When this axiom is added to RCA<sub>0</sub>, the resulting subsystem is called WKL<sub>0</sub>. A similar distinction between particular axioms on the one hand, and subsystems including the basic axioms and induction on the other hand, is made for the stronger subsystems described below.

In a sense, weak Kőnig's lemma is a form of the [[axiom of choice]] (although, as stated, it can be proven in classical Zermelo–Fraenkel set theory without the axiom of choice).  It is not constructively valid in some senses of the word "constructive".

To show that WKL<sub>0</sub> is actually stronger than (not provable in) RCA<sub>0</sub>, it is sufficient to exhibit a theorem of WKL<sub>0</sub> that implies that noncomputable sets exist. This is not difficult; WKL<sub>0</sub> implies the existence of separating sets for effectively inseparable recursively enumerable sets.

It turns out that RCA<sub>0</sub> and WKL<sub>0</sub> have the same first-order part, meaning that they prove the same first-order sentences.  WKL<sub>0</sub> can prove a good number of classical mathematical results that do not follow from RCA<sub>0</sub>, however.  These results are not expressible as first-order statements but can be expressed as second-order statements.

The following results are equivalent to weak Kőnig's lemma and thus to WKL<sub>0</sub> over RCA<sub>0</sub>:

* The [[Heine–Borel theorem]] for the closed unit real interval, in the following sense: every covering by a sequence of open intervals has a finite subcovering.
* The Heine–Borel theorem for complete totally bounded separable metric spaces (where covering is by a sequence of open balls).
* A continuous real function on the closed unit interval (or on any compact separable metric space, as above) is bounded (or: bounded and reaches its bounds).
* A continuous real function on the closed unit interval can be uniformly approximated by polynomials (with rational coefficients).
* A continuous real function on the closed unit interval is uniformly continuous.
* A continuous real function on the closed unit interval is [[Riemann integral|Riemann]] integrable.
* The [[Brouwer fixed point theorem]] (for continuous functions on an <math>n</math>-simplex).<ref name="Simpson2009" /><sup>Theorem IV.7.7</sup>
* The separable [[Hahn–Banach theorem]] in the form: a bounded linear form on a subspace of a separable Banach space extends to a bounded linear form on the whole space.
* The [[Jordan curve theorem]].
* Gödel's completeness theorem (for a countable language).
* Determinacy for open (or even clopen) games on {0,1} of length ω.
* Every countable [[commutative ring]] has a [[prime ideal]].
* Every countable formally real field is orderable.
* Uniqueness of algebraic closure (for a countable field).
* The [[De Bruijn–Erdős theorem (graph theory)|De Bruijn–Erdős theorem]] for countable graphs: every countable graph whose finite subgraphs are <math>k</math>-colorable is <math>k</math>-colorable.<ref>{{cite journal
 | last = Schmerl | first = James H.
 | doi = 10.1002/1521-3870(200010)46:4<543::AID-MALQ543>3.0.CO;2-E
 | issue = 4
 | journal = Mathematical Logic Quarterly
 | mr = 1791549
 | pages = 543–548
 | title = Graph coloring and reverse mathematics
 | volume = 46
 | year = 2000}}</ref>