Mizar formalization of Jordan Curve Theorem

The proof of Jordan curve theorem for special polygons is the first part of the formalization of general Jordan curve theorem for simple closed curves:

Jordan curve theorem - the theorem that states that every simple closed curve divides a plane into two parts and is the common boundary between them (see The American Heritage Dictionary of the English Language).

Some other related links: 1, 2, 3, 4.

This theorem seems quite obvious, however it is common knowledge that it is very difficult to it prove rigorously. Mizar formalization follows the script 'On the Jordan curve theorem' by Y. Nakamura and Y. Takeuchi. The work actually started in 1992 with the article JORDAN1 by Y. Nakamura and J. Kotowicz in which the Jordan property was introduced. That article was preceded by several other articles in which Euclidean spaces and special polygonal arcs were defined. A polygonal curve is called special if its line segments are parallel to the axes. Another useful concept of so called Go-boards was also defined before the submission of JORDAN1. By a Go-board the authors ment a matrix of points of the plane as below

(x₁,y₁) ... (x₁,y_n)
... ... ...
(x_n,y₁) ... (x_n,y_n)

with the property that ordinates of points in the same column are equal as well as abscissae of points in rows and, moreover, x_i<x_j and y_i<y_j for i<j. Using the techniques of Go-boards the following theorem was proved in GOBOARD4:

Every two special arcs lying in a rectangle R such that the first arc joins the upper and lower sides of R and the second arc joins the left and right sides of R have a non empty intersection.

Together with several subsequent articles devoted to further development of the theory of Go-boards, the above lemma made it possible to complete the first part of the Jordan theorem (saying that the complement of the curve is the union of two components) in GOBRD12. Later, the second part (stating that these components are different) was proved in SPRECT_4, and finally, the complete theorem was proved in GOBRD14.
The preliminary work on the proof of general Jordan curve theorem started with defining the external (so called Cages) and internal (so called Spans) approximation of the curve by special polygons in JORDAN9 and JORDAN13 respectively. Recently, we work on proofs of lemmas left to complete the whole proof. 74 articles devoted to this theorem have been collected so far, which makes about 10% of the Mizar Mathematical Library. However, some of the articles contain suplementary theory, only indirectly relevant to the proof.

Last modified: January 21, 2003