Post #2566013

Proposition 129, p. 83: If 𝐹 is a function and (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹, the successor of 𝐴 is either 𝐵 or it follows 𝐵 or it comes before 𝐵 in the #TransitiveClosure of 𝐹. Hyp. ⊢ (𝜑 → 𝐹 ∈ V) Hyp. ⊢ (𝜑 → 𝐴 ∈ dom 𝐹) Hyp. ⊢ (𝜑 → 𝐶 = (𝐹‘𝐴)) Hyp. ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝐹)𝐴)) Hyp. ⊢ (𝜑 → Fun 𝐹) Therefore ⊢ (𝜑 → (𝐵(tc‘𝐹)𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶(tc‘𝐹)𝐵)) ——— Proposition 131, p. 85: If 𝐹 is a function and 𝐴 contains all elements of 𝑈 and all elements before or after those elements of 𝑈 in the transitive closure of 𝐹, then the image under 𝐹 of 𝐴 is a subclass of 𝐴. Hyp. ⊢ (𝜑 → 𝐹 ∈ V) Hyp. ⊢ (𝜑 → 𝐴 = (𝑈 ∪ ((◡(tc‘𝐹) “ 𝑈) ∪ ((tc‘𝐹) “ 𝑈)))) Hyp. ⊢ (𝜑 → Fun 𝐹) Therefore ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐴) ——— Proposition 133, p. 86: If 𝐹 is a function and 𝐴 and 𝐵 both follow 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐵) either 𝐴 follows 𝐵 or 𝐵 follows 𝐴 in the transitive closure of 𝐹 (or both if it loops). Hyp. ⊢ (𝜑 → 𝐹 ∈ V) Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐴) Hyp. ⊢ (𝜑 → 𝑋(tc‘𝐹)𝐵) Hyp. ⊢ (𝜑 → Fun 𝐹) Therefore ⊢ (𝜑 → (𝐴(tc‘𝐹)𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵(tc‘𝐹)𝐴)) ——— So what's nice about the transitive closure that #Frege felt compelled to invent a new language in which to present mathematical arguments? When 𝑅 is a function, two sets being related by the transitive closure of 𝑅 is much like induction. When 𝑅 is a more general relation, we have a more general form of induction, that is truly #ancestral in the language of #Whitehead and #Russell.