Modulo/Congruent theorem into symbolic/predicate notation

Question

For a positive integer $n$, two numbers $a$ and $b$ are said to be congruent modulo n, if $(a-b)$ is some integer multiple of $n$, or mathematically:

$\hspace{15em} a=kn+b$

I am assuming that this can be represented symbolically as:

$\hspace{13em} \forall a \ \forall b \ \forall n \ \exists k, a=kn+b $

Say the following theorem holds:

$\hspace{10em} \ \ k\cdot n|(a-b) \wedge l\cdot n|(c-d) \implies \ q \cdot n|((ax + c) - (bx +d)) $

Is the following symbolic notation an accurate description of the above theorem, particularly the quantifiers and their placement in the statement.

$ \forall n \ \forall a \ \forall b \ \forall c \ \forall d \\ \Big( (\exists k , a=kn +b) \wedge \ (\exists r , c=ln +d) \Big)\implies \bigg( (\exists x , (ax + c) = q\ \cdot n + (bx+ d) ) \bigg) $

Answer 1

a = b ( mod n) is much different than that for all a,b,n thing.

No. kn|(a - b) is not that confusion of variables:
exists k with a = kn + b.

Answer 2

"$a$ is congruent to $b$ mod $n$" is a three-place predicate. We might write it $a\equiv_n b$ with the three places being $(\__1)\equiv_{(\__3)}(\__2)$. In "$a$ is congruent to $b$ mod $n$" or $a\equiv_n b$, $a$, $b$ and $n$ are free variables. Saying $\forall a,b,n.a\equiv_n b$ produces a proposition (a closed predicate, i.e. a predicate with no free variables). This is a formula that can be assigned a truth value, which would be clearly false in this case as not every number is congruent to every other number mod any number. Instead what we have is the definition of the three-place predicate $$a\equiv_n b\ :\!\!\iff \exists k\in\mathbb Z.a=kn+b$$

The colon indicates that this is the defining equivalence for $a\equiv_n b$.

If you think of a predicate as a truth valued function, then the free variables (in this case $a$, $b$, and $n$) are the parameters of the function. Yet another perspective on this is that we can rename bound (e.g. quantified) variables while we can't rename free variables. So $\exists k\in\mathbb Z. a=kn+b$ is the same as $\exists m\in\mathbb Z.a=mn+b$ but is not the same as $\exists k\in\mathbb Z.x=kn+b$.

Theorem's are propositions which means it needs to not have any free variables (though there is often a convention of universally quantifying all free variables). Your "theorem" has many free variables, and it is unclear how you intend to quantify them. The "universally quantify all free variables" would not produce the formula you state at the end. You also seem to have some confusion on how to relate $a\equiv_n b$ and divisibility. You can prove (given a definition of $|$) that $a\equiv_n b \iff n|(a-b)$. There is no need to add these $k$s and $l$s etc.