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? ๐ฅบ
