Quelklef

milk consumer

girly but not a girl

name-color: #C09


Quelklef
@Quelklef

been playing with some math notation recently

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


Quelklef
@Quelklef

turns out there is a pretty natural way modify this notation to support ∀∃-statements instead of just ∀-statements. using it, topological continuity looks like this:

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


one can read this as follows: "if you can give me the solid stuff, then i can give you the dotted stuff". give me a thing which maps under f to an element of an open set, and in response i can tell you that the preimage of that open set is also open and contains your original thing

precisely, filled bullets correspond to universal quantifiers, open circles to existential quantifiers, solid arrows to relations on the left of an implication, and dashed arrows to relations on the right of an implication. the ∀∃-sentence corresponding to the diagram is:

( ∀ solid bullets ∃ open circles ) ( IF solid-arrow stuff holds THEN dashed-arrow stuff holds )

to be clear: this means that solid bullets have switched roles from the previous notation: where before they are existentials, now they are universals

also I should address the star (⋆): a star represents a value which is uniquely induced by a ↦-relation. it gets its own symbol because even though technically it corresponds to a quantifier, knowing the value of a star gives you no new information. stars can be "ignored" when interpreting the quantification of a diagram


something neat about the above diagram is that it defines topological continuity with no "extra" variables: it says that f is continuous wrt τ, σ iff ... and then introduces no new variables


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)