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)


Quelklef
@Quelklef

further, you can actually manage alternating quantifiers in some cases, but it's not necessarily readable...

here's epsilon-delta. lim_(x → x₀) f(x) = L iff


as a reminder, epsilon-delta in traditional form is this:

lim_(x → x₀) f(x) = L iff (∀ε > 0)(∃δ > 0)(∀x)( x ∈ B_δ(x₀) ⇒ f(x) ∈ B_ε(L) )

here by Bₐ(z) i mean the open ball of size a around z; that is, the interval (z - a, z + a)

ok, so how does the diagram given correspond to this sentence? let's first give the bullets some variable names

a by-the-books reading of this diagram wants to start with "for all ε and x such that ..." since both ε and x are solid bullets. but if we try to finish that sentence we'll fail, since x is constrained by the requirement x ∈ B_δ(x₀) which references the as-of-yet unquantified variable δ

so since x is constrained by δ, then it must be that δ is quantified above x. if we allow for that variable swap then our sentence instead starts with "for all ε such that ... exists δ such that ... forall x ..." which matches up with what epsilon-delta does actually say

there's some worries to be had regarding allowing quantifier swaps. originally we knew order of quantifiers because it was always ∀∃, by definition. but if we allow quantifier swaps now order of quantifiers could be ambiguous!

one resolution to this is as follows: you are allowed to apply only the minimal set of quantifier swaps needed to ensure that all variables are able to reference variables which constrain them. (as we did with the above diagram)

if we really wanted to adopt this convention we'd have to prove some level of coherence, that either (a) whenever swapping is required there is only one minimal set of valid swaps; or (b) there are multiple, but they produce equivalent sentences. idk if this is actually true or not. at least for the above diagram nothing bad happens!


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)

in reply to @Quelklef's post:

i am sold on "given solid, i can give you dotted" as a good way to parse, and the new stuff allowing foralls. i am not sold on the resolution rules and getting rid of variable names.

(weird take incoming): as a programmer, variable names give math some "type safety" in the sense that u generally know what a symbol should be given the context of the proof. i liked your final diagram more because of that.

having named variables could also allow you to explicitly define quantifier order in an auxiliary diagram, bypassing the ambiguity problem? idk that may not be a great solution, def less elegant

yeah, the alternating quantifiers is kinda awkward, using scope to disambiguate is even more awkward (but very neat!), and explicitly defining order is still pretty awkward

i feel like alternating quantifiers is just too complex for the medium. when reading a chain of alternating quantifiers, each quantifier introduces a new "layer" to the diagram. by this i mean that when considering the outermost quantifier you only have to grok the relations regarding the quantified variables, then with the next quantifier you have to grok those and the relations regarding the newly quantified variables, on and on until the whole diagram is included. with the solid/dotted syntax it's quick to visually split the diagram into the two layers "solid" and "solid and dotted" and go from there. but perhaps more layers is just too much to remain readable, except maybe in simple cases or if some kind of interactivity/animation is introduced (eg slider for which layers are shown)