The Rado path decomposition theorem

Let c : [ ω ] 2 → r . A path of color j is a listing (possibly empty) of integers { a 0 , a 1 , a 2 ...} such that, for all i ≥ 0, if a i +1 exists then c ( a i , a i +1 ) = j . A empty list can be a path of any color. A singleton can be a path of any color. Paths might be finite or infinite. The color is determined for paths of more than one node. Improving on a result of Erdős, in 1978, Rado published a theorem which implies Rado Path Decomposition : Let c : [ ω ] 2 → r. Then, for each j < r, there is a path of color j such that these r paths (as sets) partition ω (so they are pairwise disjoint sets and their union is everything). Here we will provide some results and proofs which allow us to analyze the effective content of this theorem.