> ~(Hs->Ms) <=> Hs->~Ms [...] this is contingent [...] Though technically this is a false statement It's just not provable. The webapp can give the example of

> ~(Hs->Ms) <=> Hs->~Ms [...] this is contingent [...] Though technically this is a false statement It's just not provable. The webapp can give the example of a world with a single object that is neither H nor M (in which case the statement is false). With some thought, I found a world where the statement is true: a single object that is H but not M. If the statement were false, then this second world couldn't exist. That said, while "logical equivalence" can mean the biconditional, as it does in the webapp, you are probably meaning logical equivalence at a level just outside individual worlds. Godel's completeness theorem is about the equivalence between whether a statement is true in all words and whether there is a proof of that statement. The earlier example illustrates that just because something's not provable doesn't mean it's false.