The line you are talking about in the rest of your post seems to be an 'unrelated' object that is used in geometry. I am not familiar with the formal definition of line that is used in geometry, but one way of defining a line is as the set of all points which satisfy "y=mx+b", for a given (m,b). A line segment would be the above definition with restrictions on the domain: x_0<x<x_f.

That is not how Euclid defined it and how it is still seen in geometry today. What you describe is called a (line) segment (http://en.wikipedia.org/wiki/Line_segment)

"but does not contain any points"

Lines extend indefinitely in two directions (if you go past Euclidean geometry, that 'indefinitely' changes meaning a bit)

One talks of a point being _on_ a line in geometry. 'contains' is something from set theory: "the set of all points on line l contains point P" is a perfectly valid expression (but "P is on l" is way shorter)

Can you make this rigorous? Because using the standard definitions, this statement is not true. It's true that a countable number of points must have total length zero (and you can even give a rigorous proof of this) but not necessarily true for a non-countable number of points. The study of "lengths of sets of points" is called measure theory.

I think it is unnecessary, however, to bring in the whole concept of length when defining lines. For example, we could simply define a line as a set of points obeying some special properties.

Infinities are weird; anybody who wants to learn math has to accept that. 0.99999… does equal 1, there are as many even numbers as integers, etc. these things are 'true' not because they make sense initially, but because they make the most sense of all the other things we have thought of so far. Similarly, a set of Aleph-0 points can completely cover a line.

Aleph_0 is the cardinality of the integers. I don't think that'll cover a line. For that, you need the cardinality of the reals, C, which may or may not be Aleph_1.

Charles Sanders Peirce said in 1903, ”Now if we are to accept the common idea of continuity […] we must either say that a continuous line contains no points or […] that the principle of excluded middle does not hold of these points. The principle of excluded middle applies only to an individual […] but places being mere possibilities without actual existence are not individuals.”

This isn't true for an uncountably infinite set of points, assuming by 'extension' you mean what is usually called 'meausre' in modern mathematics. Modern theory is perfectly fine with saying that a line of nonzero length contains an infinite number of points of zero length, and trying to draw on Euclidean notions definitions of 'point' and 'line' to find conclusions about real analysis is going to be unhelpful.

I'm not sure what that Peirce quote is trying to say.

A line is (or can be viewed as) an infinite set of points.

> To elaborate, no point could be "on" a line because a point has no extension, whereas a line does.

That seems to be a consequence of an unusual definition of "on".

You can deal instead with Euclid's axiomatization of geometry, and there "line" is an abstract thing defined by two points. Different animal, although seldom explained clearly by teachers, who often themselves don't really understand what's going on. (Although some do, and don't get the chance to explore these things because of the pressure of the curriculum, and students who don't care, but need to pass.)

All too often people get confused about this and are told to shut up by their teacher, whereas in fact the student has had an insight, and demonstrated deeper understanding.

You may find the Fano plane (a three-dimensional finite projective space) interesting:

  * http://en.wikipedia.org/wiki/Fano_plane (brief description)
  * http://math.ucr.edu/home/baez/octonions/node4.html (connections with higher math)