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 two bifurcations.

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