My Discrete Mathematics textbook translates the statement "Every real number except zero has multiplicative inverse" to $$\forall{x}{({(x\neq0)} \rightarrow{\exists{y}{(xy=1)}})}.\tag1$$ I noticed that the above translation is correct if and only if you interpret the original English statement as not specifying whether zero has multiplicative inverse. That is, all numbers have inverses except zero for which zero may or may not have an inverse. (This is evident from the truth table in which if $x$ was equal to zero then whether $x$ has an inverse or not the statement evaluates to true in both cases.) In the same vein, I can say that "Every real number greater than 7 has a multiplicative inverse" translates to $$\forall{x}{({(x>7)} \rightarrow{\exists{y}{(xy=1)}})};$$ this statement doesn't mean that only real numbers greater than $7$ have a multiplicative inverse.
However, if you interpret the original English statement as "Every real number except zero has multiplicative inverse while zero does not have a multiplicative inverse", then this translates to $$\forall{x}{({(x\neq0)} \leftrightarrow{\exists{y}{(xy=1)}})}.\tag2$$
My professor translated the original sentence the same way the book did. So, I asked whether he assumed that zero has multiplicative inverse, and he answered with a yes because we know that zero does not have a multiplicative inverse. I then explained what I wrote above, but I couldn't get my point across, and he insisted that his translation was correct.
Is what I wrote above correct, or is the first translation indeed the only correct one? Is "Every real number except zero has multiplicative inverse" ambiguous or is $(1)$ or $(2)$ its correct logical equivalent?
If you can establish that $\forall x . x \cdot 0 = 0$, then that already implies $\forall x \bigg( x \ne 0 \leftarrow \bigg(\exists y. xy=1\bigg) \bigg) $ . So the $\leftarrow$ direction of the $\iff$ is usually already redundant. But it isn't wrong, so all that is left is style.
And as a general point of style and usefulness, search for assumptions that are as weak as possible but still strong enough to be sufficient. Aim for conclusions that are as strong as possible, but weak enough to still be correct.
The set of natural numbers that is divisible by 6 is a strict subset of those that are divisible by 2. So $6|x$ is a strictly stronger claim than $2|x$. If I tell you $6|x$ then I have told you "more information" than if I have only told you $2|x$. On the other hand, if I say "I will let you out of jail if you find me an $x$ divisible by 6", then I am asking more of you than the other jailer who would release you for only finding and even $x$.
Strong/weak is a strictly partial order. For the two statements $x > 1000$ as well as $x \text{ is even}$, neither is stronger or weaker than the other. The set of numbers satisfying the first is neither a superset nor a subset of the second.
If you are offering the theorem $X \to Y$ to the world: If $X$ is too strong, no one can ever use it. If $Y$ is too weak, there is no reason to use it. An example of a very useless theorem would be $z = 178462827 \implies z = z$. Who cares about $178462827$? That is too strong of a requirement. And $z=z$ is such a weak claim that is always true. Not helpful.
Implications $X \to Y$ are 3 parts: the assumption $X$, the conclusion $Y$, and the implication $X \to Y$. When you offer a theorem, you want to offer the strongest not-wrong version of the theorem. An implication is strengthened by weakening the conclusion. An implication is strengthened by strengthening the conclusion.
The weakest possible implication is $\text{false implies true}$. It is so weak that it manifests both meanings of "vacuously true".
Now as a disclaimer, there is some cheating going on here, because every mathematical theorem when written out with all of the assumptions that goes into it is a tautology, so in that context every mathematical theorem is technically equally strong. So if you wanted to get into formal logic, all this only applies to domain specific way theorems are presented, not to the entire tautological version of theorems.
Correct.