How many degrees of freedom do you have in which comment you post? Do highly upvoted comments boost a video's reach? Do you have an example of a comment that was useful in the way Community Notes are on X?

I am giving an example of something I can do "for any x" but not "for all x". In the first case, the x is given in a fully constructed, reified form, and I can look at its internals to build a bespoke response. In the second case, I would have to give a general procedure that can work with all x while interacting with the x only by means of its external interface.

foo :: $(Int\to \perp )\to \perp$
foo f = f 4

Look, there's an integer! It's right there, "4". Apparently $Int$ is inhabited.

bar :: $\left(\right(a\to \perp )\to \perp )\to a$
bar fo = ???

There's nothing in particular to be done with fo... if we had something of type $a\to \perp$ to give fo, we would be open for business, but we don't know enough about $a$ to make this any easier than coming up with a value of type $\perp$, which is a non-starter.

If you write me a function of type $(a\to \perp )\to \perp$, I can point out the place in its source code where you included a value of type $a$, but I can't write a function of type $\left(\right(a\to \perp )\to \perp )\to a$.

I can come-up-with-math-to-model any problem, but I can't come-up-with-math-to-model all problems, by diagonalization.

During a call with Justin Shovelain we came up with an unstable example: Whether the largest human is male is ~discontinuous around a 50% estimate of whether a random man is larger than a random woman.

He's trying to tend a garden that an invasive species has just been introduced to. It'll be easier if we use class signaling as described by Scott Alexander to distinguish ourselves.

It was previously strong_disjunction(a->b,b->a) instead of weak_conjunction(a->b,b->a) :P.

(I wonder how one decides whether to use weak or strong conjunction there...)

The definition of <-> in terms of previous can't be right, that's always 1 regardless of a and b. Also you missed the $v$s in the formula for <->.

(Also it's kinda iffy that weak disjunction is a stronger statement than strong disjunction...)

The story of 1/2, 1/4, ... could be continued immediately to the infinite case, right? (And all the way up the ordinal ladder.)