About Cook–Levin theorem I want to check whether I understand the Cook-Levin theorem fully (using the Travelling Salesman Problem as an example).
Given a weighted graph $G$ and an number $L$, the a Travelling Salesman Problem (TSP) is the problem of finding a tour of length at most $L$.
As TSP is in $\mathcal{NP}$ there exists a non-deterministic polynomial time Turing Machine $M$ that can decides the problem; given a graph $G$ and length $L$:
$$
M(G,L) = \left\{
\begin{array}{ll}
1\text{ if there exists a tour in }G\text{ of length at most }L\\
0\text{ otherwise}
\end{array}
\right.
$$
By the Cook-Levin theorem, such a decider $M$ can be transformed into a Boolean formula that is true if and only if $M$ accepts on $(G,L)$. Let the transformation from the Cook-Levin theorem proof be $R$.

Question 1: Given two  deciders $x$ and $y$, if $R(x) = R(y)$ is same Boolean expression, i.e. $x$ and $y$ are transformed into same Boolean formula, What can we say about $x$ and $y$? Are they equivalent?

Also,

Question 2: Is $R$ invertible? Can a Boolean expression be converted to a decider?

 A: Question 1: If two Turing Machines map to the same formula, then yes, they are equivalent - they produce the same output given the same input.
Question 2: Yes, there is at least one proof of the Cook-Levin theorem that would allow in principle the production of an inverse mapping $R^{-1}$, as the variables of the formula explicitly specify the states of the Turing Machine and the transition function. However we can't take any Boolean formula and produce a Turing Machine, all we can say is that $M = R^{-1}(R(M))$.
Now some extra notes and caveats: the Cook-Levin Theorem is not strictly one theorem, both Cook and Levin produced results that are equivalent to what we now call the Cook-Levin theorem. It happens that Garey and Johnson (in: Computers and Intractability) give a reduction that allows the answers I gave above, but this may not be true for all proofs.
Moreover, the reductions that we use routinely for NP-completeness proofs certainly do not satisfy such properties, in particular many source instances can map to a single target instance thus we cannot construct any inverse function nor can we necessarily say anything particular about the source instances.
