Editing Jordan curve theorem (section)

== History and further proofs ==

The statement of the Jordan curve theorem may seem obvious at first, but it is a rather difficult theorem to prove. [[Bernard Bolzano]] was the first to formulate a precise conjecture, observing that it was not a self-evident statement, but that it required a proof.<ref>{{cite journal
 | last = Johnson | first = Dale M.
 | doi = 10.1007/BF00499625
 | issue = 3
 | journal = Archive for History of Exact Sciences
 | mr = 446838
 | pages = 262–295
 | title = Prelude to dimension theory: the geometrical investigations of Bernard Bolzano
 | volume = 17
 | year = 1977}} See p. 285.</ref>
It is easy to establish this result for [[polygon]]s, but the problem came in generalizing it to all kinds of badly behaved curves, which include [[nowhere differentiable]] curves, such as the [[Koch snowflake]] and other [[fractal curve]]s, or even [[Osgood curve|a Jordan curve of positive area]] constructed by {{harvtxt|Osgood|1903}}.

The first proof of this theorem was given by [[Camille Jordan]] in his lectures on [[real analysis]], and was published in his book ''Cours d'analyse de l'École Polytechnique''.{{sfnp|Jordan|1887}} There is some controversy about whether Jordan's proof was complete: the majority of commenters on it have claimed that the first complete proof was given later by [[Oswald Veblen]], who said the following about Jordan's proof:

<blockquote>His proof, however, is unsatisfactory to many mathematicians. It assumes the theorem without proof in the important special case of a simple polygon, and of the argument from that point on, one must admit at least that all details are not given.<ref>{{harvs|txt|authorlink=Oswald Veblen|first=Oswald |last=Veblen|year=1905}}</ref></blockquote>

However, [[Thomas Callister Hales|Thomas C. Hales]] wrote:

<blockquote>Nearly every modern citation that I have found agrees that the first correct proof is due to Veblen... In view of the heavy criticism of Jordan’s proof, I was surprised when I sat down to read his proof to find nothing objectionable about it. Since then, I have contacted a number of the authors who have criticized Jordan, and each case the author has admitted to having no direct knowledge of an error in Jordan’s proof.<ref>{{harvtxt|Hales|2007b}}</ref></blockquote>

Hales also pointed out that the special case of simple polygons is not only an easy exercise, but was not really used by Jordan anyway, and quoted Michael Reeken as saying:
<blockquote>Jordan’s proof is essentially correct... Jordan’s proof does not present the details in a satisfactory way. But the idea is right, and with some polishing the proof would be impeccable.<ref>{{harvtxt|Hales|2007b}}</ref></blockquote>

Earlier, Jordan's proof and another early proof by [[Charles Jean de la Vallée Poussin]] had already been critically analyzed and completed by Schoenflies (1924).<ref>{{cite journal |author=A. Schoenflies |author-link=Arthur Moritz Schoenflies |title=Bemerkungen zu den Beweisen von C. Jordan und Ch. J. de la Vallée Poussin |journal=Jahresber. Deutsch. Math.-Verein |volume=33 |year=1924 |pages=157–160}}</ref>

Due to the importance of the Jordan curve theorem in [[low-dimensional topology]] and [[complex analysis]], it received much attention from prominent mathematicians of the first half of the 20th century. Various proofs of the theorem and its generalizations were constructed by [[James Waddell Alexander II|J. W. Alexander]], [[Louis Antoine]], [[Ludwig Bieberbach]], [[Luitzen Brouwer]], [[Arnaud Denjoy]], [[Friedrich Hartogs]], [[Béla Kerékjártó]], [[Alfred Pringsheim]], and [[Arthur Moritz Schoenflies]].

New elementary proofs of the Jordan curve theorem, as well as simplifications of the earlier proofs, continue to be carried out.

* Elementary proofs were presented by {{harvtxt|Filippov|1950}} and {{harvtxt|Tverberg|1980}}.
* A proof using [[non-standard analysis]] by {{harvtxt|Narens|1971}}.
* A proof using constructive mathematics by  {{harvs | txt|last1=Berg | first1=Gordon O. | last2=Julian | first2=W. | last3=Mines | first3=R. | last4=Richman | first4=Fred | title=The constructive Jordan curve theorem | mr=0410701 | year=1975 | journal=[[Rocky Mountain Journal of Mathematics]] | issn=0035-7596 | volume=5 | pages=225–236}}.
* A proof using the [[Brouwer fixed point theorem]] by {{harvtxt|Maehara|1984}}.
* A proof using [[planar graph|non-planarity]] of the [[complete bipartite graph]] ''K''<sub>3,3</sub> was given by {{harvtxt| Thomassen| 1992}}.

The root of the difficulty is explained in {{harvtxt|Tverberg|1980}} as follows. It is relatively simple to prove that the Jordan curve theorem holds for every Jordan polygon (Lemma 1), and every Jordan curve can be approximated arbitrarily well by a Jordan polygon (Lemma 2). A Jordan polygon is a [[polygonal chain]], the boundary of a bounded connected [[open set]], call it the open polygon, and its [[Closure (topology)|closure]], the closed polygon. Consider the diameter <math>\delta</math> of the largest disk contained in the closed polygon. Evidently, <math>\delta</math> is positive. Using a sequence of Jordan polygons (that converge to the given Jordan curve) we have a sequence <math>\delta_1, \delta_2, \dots</math> ''presumably'' converging to a positive number, the diameter <math>\delta</math> of the largest disk contained in the [[closed region]] bounded by the Jordan curve. However, we have to ''prove'' that the sequence <math>\delta_1, \delta_2, \dots</math> does not converge to zero, using only the given Jordan curve, not the region ''presumably'' bounded by the curve. This is the point of Tverberg's Lemma 3. Roughly, the closed polygons should not thin to zero everywhere. Moreover, they should not thin to zero somewhere, which is the point of Tverberg's Lemma 4.

The first [[formal proof]] of the Jordan curve theorem was created by {{harvtxt|Hales|2007a}} in the [[HOL Light]] system, in January 2005, and contained about 60,000 lines. Another rigorous 6,500-line formal proof was produced in 2005 by an international team of mathematicians using the [[Mizar system]]. Both the Mizar and the HOL Light proof rely on libraries of previously proved theorems, so these two sizes are not comparable. {{harvs|txt | last1=Sakamoto | first1=Nobuyuki | last2=Yokoyama | first2=Keita | title=The Jordan curve theorem and the Schönflies theorem in weak second-order arithmetic | doi=10.1007/s00153-007-0050-6 | mr=2321588 | year=2007 | journal=Archive for Mathematical Logic | issn=0933-5846 | volume=46 | issue=5 | pages=465–480}} showed that in [[reverse mathematics]] the Jordan curve theorem is equivalent to [[weak Kőnig's lemma]] over the system [[Reverse mathematics#The base system RCA0|<math>\mathsf{RCA}_0</math>]].