What is the notation for: for every element of a set of 2-tuples, the second element in each tuple is unique? I have a set of 2-tuples, A, and I want to state that every tuple in A has a unique second element. In other words, for every pair of elements i and j from A, where i is not equal to j, the second element of tuple i does not equal the second element of tuple j.
Also, what is the name of the logic(?) used to make such statements?
 A: As Carl remarks in comments, your formulation in the question is perfectly all right. However, if you have a good reason to want to write it down symbolically (and "because that is more mathematical" is not a good reason; it is false), then you can just do it part for part:
For every pair of elements $i$ and $j$ from $A$ ($\forall i,j\in A$) where $i$ is not equal to $j$ ($i\ne j$) it holds that ($\Rightarrow)$ the second element of the pair $i$ ($\pi_2(i)$) does not equal ($\ne$) the second element of pair $j$ ($\pi_2(j)$):
$$ \forall i,j\in A: i\ne j\Rightarrow \pi_2(i)\ne \pi_2(j)$$
where $\pi_2$ is the second projection function. If you don't want to use the $\pi_2$, you can write
$$ \forall \langle a,b\rangle, \langle c,d\rangle\in A: \langle a,b\rangle\ne\langle c,d\rangle\Rightarrow b\ne d$$
or a bit shorter as
$$ \forall \langle a,b\rangle, \langle c,d\rangle\in A: b=d\Rightarrow a=c$$
If you're in a completely formal setting where you can't quantify over patterns such as $\langle a,b\rangle$, you'll need to do something like
$$ \forall a,b,x: \langle a,x\rangle\in A\land \langle b,x\rangle\in A\Rightarrow a=b$$
Since quantifiers are involved here, the logic is (first-order) predicate calculus.
By the way, the usual name for a 2-tuple, except (possibly) when you're speaking to machines instead of to people, is an ordered pair.
