This looks more complex than it needs to be. We can just merge those two IFF soundnesses at the top and remove transitive implications and we are left with a straight line with a couple bifurcations to cul de sacs.

Also… I only know constructive logics and abstract interpretation with Galois connections… Where do they fit in this? 🥺

Any nerds able to give us the TL;DR on what this actually means?

There’s no allowing for Unspecial Soundness.

Or where most fun knowledge resides: Unspecial Unsoundness.

Special unsoundness