Eliezer, I'm thinking of applying this to conversations between humans constructing particular arguments, not to building AI. I'm hoping it will avoid the particular sloppiness of proving one thing and taking it to have proven another, similar sounding thing. If we conflate things, we should make it explicit.

It's true that defining Y as X won't match X->Y where X is false and Y is true, but that's also the case where, given X->Y, you can't prove X from Y or Y from X. So X->Y wouldn't (or shouldn't!) be used in a proof in such a case.

If there is no element in our model for which X is true and Y is false, should we conclude \z.X(z)->Y(z) and use that as a premise in further reasoning? "If z is a raven then z is red." is true for everything if you have no ravens.