home.social
Sign in Create account

#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] Β·

    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