Quelklef

milk consumer

girly but not a girl

name-color: #C09


been playing with some math notation recently

a function f is surjective iff for every y ∈ cod(f) we have


bullets signify values that we haven't given a name to; a diagram with a bullet corresponds to an existential formula. arrows signify relations. the ↦ arrow is used for functions, so x ↦f y means f(x) = y

a function f is injective iff for every distinct x, y ∈ dom(f) we have

i like these diagrams. they're neat. and fun. also, in some cases i think they can really help clarity. i have a proof thats ~1 paragraph in traditional style and ~2 lines with diagrams

given a relation ⇝ ⊆ A², its transitive closure is the relation R so that xRy iff

writing conditions this way feels almost akin to doing point-free programming. eg eliminating variable names, exposing underlying structure

a function f : (X, τ) → (Y, σ) between topological spaces is continuous iff for every x ∈ X and f(x) ∋ V ∈ σ we have

(edit: this is not the definition of continuity, oops)

it's tempting to want to fit entire sentences into a diagram, including e.g. alternating quantifiers. i don't know of a good way to do it though. im sticking to existentials only for now

we say two categories C and D are equivalent iff

one interesting thing i have done is use double-struck arrows for implication and dotted arrows for implied arrows. for instance an order (A, ≤) is dense iff for all a, b ∈ A we have

here's a proof that ⊆ is transitive:

finally, a larger proof. take two relations over a set A and call them ↪ and ↠. assume that ↠ is transitive and assume that if A ↠ B ↪ C then

now define a relation R so that xRy iff x ↪ • ↪ • ↪ ⋯ ↪ • ↠ y. then R is transitive:

writing this proof (and problem statement!) in traditional style would require the works, including explicit invocation of induction. but with a diagram? blam, boom, ur done

in fairness the proof does lack clarity, like where/how precisely we use our assumptions

(btw, this seemingly-contrived setup actually comes from an organic scenario!)


You must log in to comment.

in reply to @Quelklef's post:

interesting. impenetrable insofar as i haven't made the mapping from diagrams to formulas clear? or just fundamentally more difficult to read than text?

some feel obtuse for me, like the density one, but others really do feel more evocative to me, like the category equivalence once and the final proof

now that i am more awake and taking a second read i am starting to see the beauty in them. one component of a fully-fledged proof (after you do all the appropriate quantification at the beginning), and especially in the case of the last one, even more readable than text. establishing the initial conceptual understanding of how to read was the only tricky part

how palatable is the idea of incorporating semantic color? like, first-order implications (do not know the standard lexicon well enough sorry in advance) being a different color from existentials, etc. i know there are accessibility/rigor issues potential, in addition to just being another potentially unhelpful, overcomplicating visual mechanic, but i'd still be tempted.

making implications a different color from everything else is an interesting idea. there's already no ambiguity regarding implications (if it's an arrow between dots, it's a relation; if it's between arrows, it's an implication), but color could maybe help with visual fidelity? like emphasizing/de-emphasizing certain parts of the diagram

i also once had a diagram include red and blue arrows so that i could refer in some text to "the red arrows" and "the blue arrows"

i'd worry about color as part of the syntax both for accessibility and visual noise concerns, as you mention, but also because color is arbitrary. if, for instance, we want to distinguish universals and existentials by color, which should be what color? color doesn't have strong associations (to me, at least)

but yeah i think color could be used to great effect, if done wisely (as it is with all notation!) :3

i suppose 'arbitrary' is a concept we keep running into because like, hmm. what you choose to show is also in some sense arbitrary? if i'm speaking nonsense let me know but—there are a large quantity of implications you could show from any given relation, so you've already stated your purpose by choice of implications, so also color-coding them potentially based on your intent seems fully inline compatible philosophically? of course with all the caveats in mind.

and yeah, i think it would be a case of 'experiment and eventually a consensus forms, or some sort of key is in order', though maybe if you need a key, you've violated the very purpose of these sorts of diagrams. i dunno!

i guess im saying that it depends on the way the color coding is done. saying "in the above diagram, the red implications come from theorem X and the yellow from theorem Y", that seems like a nice use of color. but if you say, for instance, that across all diagrams implications proceed in the order red, yellow, blue, green, orange, then i have concerns

(this is what i meant by saying i was worried about color being a part of the "syntax" as opposed to being used in an ad-hoc manner)