home.social
Sign in Create account

#frege β€” Public Fediverse posts

Live and recent posts from across the Fediverse tagged #frege, 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] Β·

    Begriffsschrift (1879), is one of the first manuscripts on #SymbolicLogic. As such, it literally invents a new language to describe the subjects the author, #GottlobFrege, wants to introduce. And this notation is very unlike what we see in math before or after this.

    So I will list some theorems adapted (by me, circa 2020) from #Frege with proper set-theoretical bounds.

    #SetTheory #Logic #Metamath

    #metamath #logic #settheory #frege #gottlobfrege #symboliclogic
  6. :rss: Hacker News @[email protected] Β·

    Bertrand Russell: Why I Am Not a Christian (1927)
    users.drew.edu/~jlenz/whynot.h
    #ycombinator #Bertrand_Russell #philosophy #essays #articles #books #Russell #Bertrand_Russell_Society #Wittgenstein #Carnap #Frege #G_E_Moore #Gottlob_Frege #Ludwig_Wittgenstein #Rudolf_Carnap #Bertrand_Russell_Society_Quarterly #Analytic_Philosophy #Early_Analytic_Philosophy #History_of_Analytic_Philosophy #History_of_Early_Analytic_Philosophy

    #ycombinator #bertrand_russell #philosophy #essays #articles #books
  7. Friedrich Wilhelm Grafe @[email protected] Β·

    @ereliuer_eteer

    @philosophy
    @philosophie
    #philosophy

    It was #Kant suggesting that, where the #mathematician starts, #philosopher 's work is already done [Über die Deutlichkeit der GrundsÀtze... §1...]

    Of course in a formal system, say #FOL, #identity is simply the strictest equivalence relation, the unit classes of the domain being its equivalence classes. And yes, this is really elementary stuff, high school level, if you like. And no, that's not, why #philosophers at least since #Leibniz (and in a sense since #Parmenides), and more recently #Frege made a case for it.

    Typically math philosophical issues with identity from my point of view do include the question of indiscernibles, the sense of an identity statement wrt. redundance, the relation status of identity, ... open list

    #philosophy #mathematician #philosopher #fol #identity #philosophers