König Dierk
Richard PennerProposition 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.
ULB Münster › FachInfos
Ian Brown 
yudukikun5120
Pete
yoxem