home.social

#transitiveclosure β€” Public Fediverse posts

Live and recent posts from across the Fediverse tagged #transitiveclosure, aggregated by home.social.

  1. Richard Penner @[email protected] Β·

    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.

    #russell #whitehead #ancestral #frege #transitiveclosure
  2. Richard Penner @[email protected] Β·

    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.

    #russell #whitehead #ancestral #frege #transitiveclosure
  3. Richard Penner @[email protected] Β·

    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.

    #russell #whitehead #ancestral #frege #transitiveclosure
  4. Richard Penner @[email protected] Β·

    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.

    #transitiveclosure #frege #ancestral #whitehead #russell
  5. Richard Penner @[email protected] Β·

    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β€˜πΉ)𝐴))

    #transitiveclosure
  6. Richard Penner @[email protected] Β·

    Proposition 98, p. 71: If 𝐢 follows 𝐴 and 𝐡 follows 𝐢 in the #TransitiveClosure of 𝑅, then 𝐡 follows 𝐴 in the transitive closure of 𝑅.

    Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐢 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐢)

    Hyp. ⊒ (πœ‘ β†’ 𝐢(tcβ€˜π‘…)𝐡)

    Therefore ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐡)

    β€”β€”β€”

    Proposition 102, p. 72: If either 𝐴 and 𝐢 are the same or 𝐢 follows 𝐴 in the transitive closure of 𝑅 and 𝐡 is the successor to 𝐢, then 𝐡 follows 𝐴 in the transitive closure of 𝑅.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐢 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ (𝐴(tcβ€˜π‘…)𝐢 ∨ 𝐴 = 𝐢))

    Hyp. ⊒ (πœ‘ β†’ 𝐢𝑅𝐡)

    Therefore ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐡)

    β€”β€”β€”

    Proposition 106, p. 73: If 𝐡 follows 𝐴 in 𝑅, then either 𝐴 and 𝐡 are the same or 𝐡 follows 𝐴 in 𝑅.

    Hyp. ⊒ (πœ‘ β†’ 𝐴𝑅𝐡)

    Therefore ⊒ (πœ‘ β†’ (𝐴𝑅𝐡 ∨ 𝐴 = 𝐡))

    β€”β€”β€”

    Proposition 108, p. 74: 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 𝐴 in the transitive closure of 𝑅.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐢 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ (𝐴(tcβ€˜π‘…)𝐢 ∨ 𝐴 = 𝐢))

    Hyp. ⊒ (πœ‘ β†’ 𝐢𝑅𝐡)

    Therefore ⊒ (πœ‘ β†’ (𝐴(tcβ€˜π‘…)𝐡 ∨ 𝐴 = 𝐡))

    β€”β€”β€”

    Proposition 109, p. 74: If 𝐴 contains all elements of π‘ˆ and all elements after those in π‘ˆ in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴 = (π‘ˆ βˆͺ ((tcβ€˜π‘…) β€œ π‘ˆ)))

    Therefore ⊒ (πœ‘ β†’ (𝑅 β€œ 𝐴) βŠ† 𝐴)

    β€”β€”β€”

    Proposition 114, p. 76: If either 𝑅 relates 𝐴 and 𝐡 or 𝐴 and 𝐡 are the same, then either 𝐴 and 𝐡 are the same, 𝑅 relates 𝐴 and 𝐡, 𝑅 relates 𝐡 and 𝐴.

    Hyp. ⊒ (πœ‘ β†’ (𝐴𝑅𝐡 ∨ 𝐴 = 𝐡))

    Therefore ⊒ (πœ‘ β†’ (𝐴𝑅𝐡 ∨ 𝐴 = 𝐡 ∨ 𝐡𝑅𝐴))

    #transitiveclosure
  7. Richard Penner @[email protected] Β·

    Proposition 83, p. 65: If the image of the union of π‘ˆ and π‘Š is a subset of the union of π‘ˆ and π‘Š, 𝐴 is an element of π‘ˆ and 𝐡 follows 𝐴 in the #TransitiveClosure of 𝑅, then 𝐡 is an element of the union of π‘ˆ and π‘Š.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V) ; 𝑅 is a set, i.e. an element of the universal class V (not 𝑉).

    Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ π‘ˆ) ; 𝐴 is an element of class π‘ˆ.

    Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V) ; 𝐡 is a set.

    Hyp. ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐡)

    Hyp. ⊒ (πœ‘ β†’ (𝑅 β€œ (π‘ˆ βˆͺ π‘Š)) βŠ† (π‘ˆ βˆͺ π‘Š)) ; Relation 𝑅 is hereditary in the union of classes π‘ˆ and π‘Š.

    Therefore ⊒ (πœ‘ β†’ 𝐡 ∈ (π‘ˆ βˆͺ π‘Š))

    β€”β€”β€”

    Proposition 96, p. 71. If 𝐢 follows 𝐴 in the transitive closure of 𝑅 and 𝐡 follows 𝐢 in 𝑅, then 𝐡 follows 𝐴 in the transitive closure of 𝑅.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐢 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐢) ; i.e. 𝐢 eventually follows 𝐴

    Hyp. ⊒ (πœ‘ β†’ 𝐢𝑅𝐡) ; 𝐡 immediately follows 𝐢

    Therefore ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐡)

    β€”β€”β€”

    Proposition 87, p. 66: If the images of both {𝐴} and π‘ˆ are subsets of π‘ˆ and 𝐢 follows 𝐴 in the transitive closure of 𝑅 and 𝐡 follows 𝐢 in 𝑅, then 𝐡 is an element of π‘ˆ.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V

    Hyp. ⊒ (πœ‘ β†’ 𝐢 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐢)

    Hyp. ⊒ (πœ‘ β†’ 𝐢𝑅𝐡)

    Hyp. ⊒ (πœ‘ β†’ (𝑅 β€œ {𝐴}) βŠ† π‘ˆ)

    Hyp. ⊒ (πœ‘ β†’ (𝑅 β€œ π‘ˆ) βŠ† π‘ˆ)

    Therefore ⊒ (πœ‘ β†’ 𝐡 ∈ π‘ˆ)

    β€”β€”β€”

    Proposition 91, p. 68. If 𝐡 follows 𝐴 in 𝑅 then 𝐡 follows 𝐴 in the transitive closure of 𝑅.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴𝑅𝐡)

    Therefore ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐡)

    β€”β€”β€”

    Proposition 97, p. 71: If 𝐴 contains all elements after those in π‘ˆ in the transitive closure of 𝑅, then the image under 𝑅 of 𝐴 is a subclass of 𝐴.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴 = ((tcβ€˜π‘…) β€œ π‘ˆ))

    Therefore ⊒ (πœ‘ β†’ (𝑅 β€œ 𝐴) βŠ† 𝐴)

    #transitiveclosure
  8. Richard Penner @[email protected] Β·

    Proposition 77, p. 62: If the images of both {𝐴} and π‘ˆ are subsets of π‘ˆ and 𝐡 follows 𝐴 in the #TransitiveClosure of 𝑅, then 𝐡 is an element of π‘ˆ.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V) ; 𝑅 is a set, which we newly require so that transitive closure may be a function. Implied, it has relation content. (tcβ€˜π‘…) is its transitive closure, the smallest relation which contains it and has the transitive property.

    Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ V) ; 𝐴 is a set.

    Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V) ; 𝐡 is a set.

    Hyp. ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐡) ; 𝐴 is related to 𝐡 by the transitive closure of 𝑅

    Hyp. ⊒ (πœ‘ β†’ (𝑅 β€œ π‘ˆ) βŠ† π‘ˆ) ; The image of class π‘ˆ is contained in π‘ˆ, which means the relation 𝑅 is hereditary in π‘ˆ

    Hyp. ⊒ (πœ‘ β†’ (𝑅 β€œ {𝐴}) βŠ† π‘ˆ) ; The image of the singleton {𝐴} is contained in π‘ˆ

    Therefore ⊒ (πœ‘ β†’ 𝐡 ∈ π‘ˆ) ; 𝐡 is an element of π‘ˆ.

    β€”β€”β€”

    Proposition 81, p. 63: If the image of π‘ˆ is a subset of π‘ˆ, 𝐴 is an element of π‘ˆ and 𝐡 follows 𝐴 in the transitive closure of 𝑅, then 𝐡 is an element of π‘ˆ.

    Hyp. ⊒ (πœ‘ β†’ 𝑅 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴 ∈ π‘ˆ) ; 𝐴 is not just a set, but an element of class π‘ˆ. This trick allows us to eliminate the last hypothesis of Proposition 77.

    Hyp. ⊒ (πœ‘ β†’ 𝐡 ∈ V)

    Hyp. ⊒ (πœ‘ β†’ 𝐴(tcβ€˜π‘…)𝐡)

    Hyp. ⊒ (πœ‘ β†’ (𝑅 β€œ π‘ˆ) βŠ† π‘ˆ)

    Therefore ⊒ (πœ‘ β†’ 𝐡 ∈ π‘ˆ)

    #transitiveclosure
  9. Richard Penner @[email protected] Β·

    Notation guide (adapted from Metamath):

    β€’ πœ‘, a metavariable standing for any logical formula, abbreviates the conjunction of all hypotheses listed for a given proposition; writing each line as ⊒ (πœ‘ β†’ …) puts the theorem in "deduction form," which can be easier to apply in #Metamath.

    β€’ ⊒ πœ‘ asserts that πœ‘ is true; the turnstile is descended from #Frege's own Urteilsstrich (judgment stroke).

    β€’ 𝐴𝑅𝐡 means the ordered pair ⟨𝐴, 𝐡⟩ is an element of 𝑅, or we could say 𝐡 immediately follows 𝐴

    β€’ 𝐡 = (π‘…β€˜π΄) means 𝐡 is the unique set such that 𝐴𝑅𝐡 is true (when such a 𝐡 exists) which means 𝑅 is function-like when restricted to operating on the singleton {𝐴}

    β€’ (𝑅”𝐴) is the image of 𝐴

    β€’ dom 𝑅 is the domain of 𝑅, the class of all sets π‘₯ such that there is a set 𝑦 that would make π‘₯𝑅𝑦 true.

    β€’ Fun 𝑅 is true when 𝑅 is function-like for all sets in its domain.

    β€’ ◑𝑅 is the converse of 𝑅 so 𝐴◑𝑅𝐡 iff 𝐡𝑅𝐴

    β€’ (tcβ€˜π‘…) is the #TransitiveClosure of 𝑅 (Metamath uses (t+β€˜π‘…) which can be awkward.) Whitehead and Russell use the term ancestral to describe how 𝐴(tcβ€˜π‘…)𝐡 means 𝐴 is some β€œancestor” of 𝐡. Alternately, we can say 𝐡 eventually follows 𝐴.

    β€’ V is the universal class, every set is a member, and only sets may be members of any class. After Frege’s later work ran into Russell’s Paradox, it was discovered that not every class {π‘₯ | πœ‘} makes sense as a set and so we need the hypothesis ⊒ (πœ‘ β†’ 𝐴 ∈ V) before we can talk about the function value of 𝐴 or the ordered pair ⟨𝐴, 𝐡⟩ being an element of 𝑅. V is not italic because it is a constant symbol, like tc, dom, and Fun.

    #transitiveclosure #frege #metamath