logic formalizing: The multiplication of every two positive numbers is also positive EDITED THE QUESTION WITH THE RIGHT SIGNS
I have to formalize the expression: &quot;The multiplication of every two positive numbers is also positive&quot; which I think is:
$$\forall a \forall b(ab&gt;0 \to \left((a&gt;0) \land (b&gt;0)\right))$$
but I have to choose between two options:

$\forall a \forall b(ab \le 0  \to \left((a&gt;0) \to (b
\le 0))\right)$

$\forall a \forall b (\left((a&gt;0) \land (b&lt;0)\right) \land ab&lt;0))$


which one is more correct?
One (probably the most straighforward) correct logic expression can be: $$\forall a \forall b(((a\gt 0)\land (b\gt 0))\rightarrow ab \gt0) \tag 1$$
We shall compare others with this one to check their validity.
The expression $\forall a \forall b(ab\gt 0\rightarrow((a\gt 0)\land(b\gt 0)))$ means that if the product of two numbers is positive, then both of them are positive. This is the converse of what was asked. So, it's incorrect.
In option $2$, $\forall a \forall b (\left((a&gt;0) \land (b&gt;0)\right) \land ab&lt;0))$ means that the all two numbers are positive and their product is negative. This is clearly incorrect. Thus, it doesn't generalize the statement either.
In option $1$,  $\forall a \forall b(ab\le 0  \to \left((a\gt0) \to (b\le 0))\right)$ is correct. It can be modified into $\forall a \forall b(ab\le 0  \to \left((a\le0) \lor (b\le 0))\right)$ which the contrapositive of $(1)$.
Thus, option $1$ is correct.
This “∀∀(&gt;0→((&gt;0)∨(&gt;0)))” formalizes that if the product of two numbers a, b is positive then one of them is positive. This is simply false (as long as you include negative numbers in your universe)
I don’t see how 2. or 3. formalizes that the product of two positive numbers is positive. The easiest way to do it is $\forall a \forall b (a &gt; 0 \land b &gt; 0 \implies ab &gt; 0)$