Elektrine lite

← Feed

@Arpie4Math@mathstodon.xyz

Post #2566012

2026-04-27 06:42 UTC

Proposition 111, p. 75: If either 𝐴 and 𝐢 are the same or 𝐢 follows 𝐴 in the transitive closure of 𝑅 and 𝐡 is the successor to 𝐢, then either 𝐴 and 𝐡 are the same or 𝐴 follows 𝐡 or 𝐡 and 𝐴 in the #TransitiveClosure of 𝑅. Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V) Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ V) Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V) Hyp. ⊒ (πœ‘ β†’ 𝐢 ∈ V) Hyp. ⊒ (πœ‘ β†’ (𝐴(tcβ€˜π‘…)𝐢 ∨ 𝐴 = 𝐢)) Hyp. ⊒ (πœ‘ β†’ 𝐢𝑅𝐡) Therefore ⊒ (πœ‘ β†’ (𝐴(tcβ€˜π‘…)𝐡 ∨ 𝐴 = 𝐡 ∨ 𝐡(tcβ€˜π‘…)𝐴)) β€”β€”β€” Proposition 122, p. 79: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐡 is the successor of 𝑋, then 𝐴 and 𝐡 are the same (or 𝐡 follows 𝐴 in the transitive closure of 𝐹). Hyp. ⊒ (πœ‘ β†’ 𝐴 = (πΉβ€˜π‘‹)) ; 𝐴 is the value of 𝐹 (implicitly assumed to be a function) at 𝑋 such that 𝐴 is the unique value that 𝐴 immediately follows 𝑋, 𝑋𝐹𝐴. Hyp. ⊒ (πœ‘ β†’ 𝐡 = (πΉβ€˜π‘‹)) Therefore ⊒ (πœ‘ β†’ (𝐴(tcβ€˜πΉ)𝐡 ∨ 𝐴 = 𝐡)) β€”β€”β€” Proposition 124, p. 80: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐡 follows 𝑋 in the transitive closure of 𝐹, then 𝐴 and 𝐡 are the same or 𝐡 follows 𝐴 in the transitive closure of 𝐹. Hyp. ⊒ (πœ‘ β†’ 𝐹 ∈ V) Hyp. ⊒ (πœ‘ β†’ 𝑋 ∈ dom 𝐹) ; 𝑋 is in the domain of relation 𝐹 Hyp. ⊒ (πœ‘ β†’ 𝐴 = (πΉβ€˜π‘‹)) Hyp. ⊒ (πœ‘ β†’ 𝑋(tcβ€˜πΉ)𝐡) Hyp. ⊒ (πœ‘ β†’ Fun 𝐹) ; relation 𝐹 is a function Therefore ⊒ (πœ‘ β†’ (𝐴(tcβ€˜πΉ)𝐡 ∨ 𝐴 = 𝐡)) β€”β€”β€” Proposition 126, p. 81: If 𝐹 is a function, 𝐴 is the successor of 𝑋, and 𝐡 follows 𝑋 in the transitive closure of 𝐹, then (for distinct 𝐴 and 𝐡) either 𝐴 follows 𝐡 or 𝐡 follows 𝐴 in the transitive closure of 𝐹. Hyp. ⊒ (πœ‘ β†’ 𝐹 ∈ V) Hyp. ⊒ (πœ‘ β†’ 𝑋 ∈ dom 𝐹) Hyp. ⊒ (πœ‘ β†’ 𝐴 = (πΉβ€˜π‘‹)) Hyp. ⊒ (πœ‘ β†’ 𝑋(tcβ€˜πΉ)𝐡) Hyp. ⊒ (πœ‘ β†’ Fun 𝐹) Therefore ⊒ (πœ‘ β†’ (𝐴(tcβ€˜πΉ)𝐡 ∨ 𝐴 = 𝐡 ∨ 𝐡(tcβ€˜πΉ)𝐴))

Replies (1)

  • @Arpie4Math@mathstodon.xyz 2026-04-27 06:47

    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.

    Open ##2566013