Theorem·T14
Parallelism is an equivalence relation
Playfair's axiom makes parallel with a common line mean parallel to each other.
In every affine plane
, the parallelism relation is an equivalence relation on
: reflexive, symmetric, and transitive:
In words
In every affine plane with points P and lines L, parallelism is an equivalence relation on the lines: every line is parallel to itself, parallelism is symmetric, and if l is parallel to m and m is parallel to n then l is parallel to n.
Never needed: F13 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1Reflexive: , so by the first disjunct of D042 (reflexivity of equality, disjunction introduction).
- 2Symmetric: if then (symmetry). If , then , since (D008, F05) and Extensionality. Either way .
- 3Transitive, degenerate cases: let and . If , then is exactly the second hypothesis (substitutivity); if , it is the first. If , reflexivity (step 1) closes it. So assume from now on that are pairwise distinct, with and (D042).
- 4
- 5The crossing point avoids : if , then , but has no members (D008, D002): absurd (falsum). Since and every line is a subset of (D041), (set difference), i.e. and .
- 6Playfair closes the trap: axiom (AP2) of D041, applied to the line and the point , provides exactly one line through disjoint from . But both and pass through and are disjoint from . Uniqueness forces , contradicting the standing assumption . Hence after all, and (excluded middle discharging the supposition).
∎
Remarks
Euclid, Elements Book I, Proposition 30, in modern dress: this is precisely where the parallel postulate earns its keep. The theorem is equivalent, over the other axioms, to the uniqueness half of (AP2) (at most one parallel through each external point): the proof above uses only that half, and conversely two distinct parallels to a line through one point would be parallel to each other by transitivity yet share that point. The existence half is independent: in a projective plane every two lines meet, so parallelism collapses to equality and is trivially transitive while (AP2) fails. In the hyperbolic plane, where Playfair fails (many parallels through a point), disjointness of lines is genuinely not transitive: two lines through one point can each miss a third line. The equivalence classes of
, guaranteed to partition
, are the directions (pencils of parallels) of the plane; adjoining one point at infinity per direction and one line at infinity through all of them builds the projective plane, where "at most one common point" sharpens to "exactly one".