There’s no allowing for Unspecial Soundness.

Or where most fun knowledge resides: Unspecial Unsoundness.

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? 🥺