How to formalize this simple problem in logic? I want to translate this problem with a simple logical expression. 
Say that my system only accepts tuples of strings $(s=s_1...s_n$, $t=t_1...t_n)$ where $s_i$ and $t_i \in \{0, 1, 2\}$, that are such that TWO constraints are satisfied: 


*

*only one pair of characters (say pair $k$) in the two strings differs 

*this pair is such that $s_k = 0$ and $t_k \in \{1, 2\}$
For instance, given $s = 001$ only $t = 101 | 011 | 201 | 021$ are valid. $t=111$ is not valid because multiple characters differ. This violates constraint 1. $t=002$ is not valid, because the pair that differs violates constraint 2.
So may I say: my system accepts only strings that are such that $\exists ! \; k | \;s_k \neq t_k, s_k = 0, t_k \in \{1,2\}$? Is this a complete formulation? If not, what am I missing? Thank you. 
 A: This may not be the answer you hoped for, but I found something really cool which is quite relevant to the question.
A Cayley Table can be used to represent this problem.
Here's the Cayley Table for $\mathbb{Z}_{3}$ under the ^ (power) operator. You can generate some Cayley Tables here.

Look familiar? We can definitely see some sort of pattern here.
So how can we use this?
Well, simply, this table can show us where there is a difference in the represented string (in integer form, at least).
As you may have noticed, this table is not symmetrical. This means that the direction in which we apply the operator matters to us - which is exactly what we need.
So, say we have $s=001$ and $t=101$. We can apply the operator to every corresponding position. Then we find:
$001$
$101$
.......
$011$ 
It told us exactly where the difference is. Thus, my hypothesis is that, if your set consists of tuples with $n$ elements, we should find exactly $n-1$ ones. No more, no less. Furthermore, if a two appears, the tuples are invalid.
However! With this Cayley table, the hypothesis fails. That is when we evaluate $1$^$2$ we get $1$. We want this to be two since it should tell us that an invalid difference has been detected.
For example, if $s = 0111$ and $t=1112$:
$0111$
$1112$
......
$0111$
This gives us the expected number of ones, yet is invalid.
We need a new Cayley table to fix this.

I found this one to work quite well. Let's define the operator as $?$. Now you should find that everything works out quite well. If we find exactly $n-1$ ones, we have a valid pair.
Please note that I haven't proved this in any way. It just seems to work (I'll probably win an award for this statement). If you find a contradiction anywhere, please let me know.
In a slightly more logical form as you asked for:
\begin{align}
S := \{\vec{s}&=[s_{1}, ... , s_{n}], \vec{t} = [t_{1}, ... , t_{n}]\}, \  s_{i},t_{i} \in \mathbb{Z}_{3}  \\
Let \ a?b &=  \left\{
  \begin{array}{@{}ll@{}}
    a \hat{} b, & \text{if}\ a\neq 1 \wedge b\neq 2 \\
    2, & \text{otherwise} 
  \end{array}\right. \\
Let \ f(x) &:= \mathbb{Z}_{3} \to \mathbb{Z} \tag{Just to convert} \\
then \ c &= \sum_{i=1}^{n} \left( f(s_{i}?t_{i}) \ mod \, 2 \right) \\
S \ \text{is valid iff} \ c &= n-1
\end{align}
Or if you prefer (let's ignore that the vector's elements are in $\mathbb{Z}_{3}$ for a second):
\begin{equation}
 \exists_{S} \left[ \left[ S=\{\vec{s}=[s_{1}...s_{n}], \vec{t} = [t_{1}... t_{n}]\}   \right] \Rightarrow \left[ \left[ \sum_{i=1}^{n} \left( (s_{i} ? t_{i} \right)mod \, 2) = n-1 \right] \Rightarrow \left[S \ \text{is valid} \right] \right] \right]
\end{equation}
