Double left-right arrow meaning While reading Hilbert's Tenth Problem (English version of a talk by Y. Matiyasevich) 
at page 3 I found:
...On the other hand let
$$D(x_1,...,x_m) = 0 \quad (3)$$
be an arbitrary Diophantine equation; suppose that we are looking for its solutions in integers $x_1,...,x_m$. Consider another equation:
$$D(p_1 \Leftrightarrow q_1, ..., p_m \Leftrightarrow q_1) \quad (4)$$
It is clear that any solution of equation (4) in natural numbers $p_1,...,p_m,q_1,...,q_m$ yelds the solution: $x_1 = p_1 \Leftrightarrow q_1, ..., x_m = p_m \Leftrightarrow q_m,$ of equation (3) in integers $x_1,...,x_m$ ...
What is the meaning of the operator $\Leftrightarrow$? Is it a standard notation?
NOTE: the "standard" way to show that a Diophantine equation with integer solutions has a corresponding equivalent Diophantine equation with natural solutions is to use the equation:
$$\prod D( \pm x_1, ..., \pm x_m ) = 0$$
 A: In number theory and in integer programming there are several standard ways of moving from equations solvable in integers to equations solvable in natural numbers.
One way is to replace each integer variable $x_i$ by a difference of a pair of fresh variables $p_i$ and $q_i$ ranging over natural numbers $p_i - q_i$. That is each occurrence of $x_i$ is replaced by $p_i - q_i$. That is what is done in the paper. This works well in particular in linear integer programming problems since the new equations are also linear.
Another way is the one in the original post. That is replace the equation 
$$
  D(x_1,...,x_m)=0, x_i \in \mathbb{Z}
$$
by a disjunction of equations 
$$
  D((-1)^{\alpha_1} q_1,..., (-1)^{\alpha_m} q_m)=0, q_i \in \mathbb{N}
$$
for all possible combinations of $\alpha_1,...,\alpha_m\in \{0,1\}$, that is 
$$
  \Pi_{\bar\alpha\in \{0,1\}^m}\; D((-1)^{\alpha_1} q_1,..., (-1)^{\alpha_m} q_m)=0.
$$
It is also clear that if the original equation has an integral solution, than one of the multipliers of the product would also turn to zero by the corresponding choice of $q_i$ and vice versa.
Here the $p \Leftrightarrow q$ symbol is just a strange font substitution for $p - q$ and does not have any special meaning.
A: The double arrow symbolizes logical equality.
