Gro-Tsen (temp account)

I don't know who needs to hear this, but my Bluesky account https://bsky.app/profile/gro-tsen.bsky.social is now bridged to Mastodon under the name @gro-tsen.bsky.social (so you can follow my Bluesky activity by following this user on Mastodon — and I don't know what happens if you reply on Mastodon).

Actual bridge link is here: https://fed.brid.gy/bsky/gro-tsen.bsky.social

@andrejbauer@mathstodon.xyz @jeanas@mastodon.abou-samra.fr I think the K₃ formula I quote at @gro_tsen_test@mastodon.sdf.org is actually more relevant, because it seems to be exact same reasoning, and, perhaps more importantly, the K₃ formula, just like Andrej's, is valid in Medvedev's logic of finite problems (equivalently, in the topos of simplicial sets), whereas Plisko's formula that I copied on my blog (which is “L” in Skvortsov's survey) is *not*: it requires a more delicate reasoning with Kleene's fixed point theorem.