Did I translate this correctly?
No. The oddness needs to be quantified too.
You want $\forall n~\big(\exists k~(n=2k+1)~\to~\exists k~\exists l~(n=k^2-l^2)\big)$
It might be helpful to emphasise that the existance establishing oddness is distinct from the existances establishing sum-of-squares.
$$\forall n~\big(\exists k~(n=2k+1)~\to~\exists a~\exists b~(n=a^2-b^2)\big)$$
In my initial universal quantifier, I sometimes see people write $∀n∈S P(n)$. Is this just another way of specifying the domain so I don't have to say what the domain is after writing everything down in symbols? A kind of shorthand?
You may wish to explicitly indicate the domain of the discussion.
$$\forall n\in\Bbb Z~\big(\exists k\in\Bbb Z~(n=2k+1)~\to~\exists a\in\Bbb Z~\exists b\in\Bbb Z~(n=a^2-b^2)\big)$$
As you see, this can clutter the statement when every entity is drawn from the same domain. So if you have established in accompanying text that is the implicit domain is the Integers, there is no need to explicitly indicate it in the statement.
In the book I use they'll nest quantifiers explicitly like $∃k~∃l~Q(k,l)$. In my translation I did what I've seen elsewhere which is to do $∃~k,l~Q(k,l)$ is this okay?
It is a style choice. I prefer explictly quantifying each variable, but again, abbreviating things can reduce clutter
And if the answer to Question 2 above was that using the $∈$ shorthand is acceptable, then I'm guessing I could also write this as $∃~k,l~∈S~Q(k,l)$.
It ... is accepted, as long as you take care to avoid ambiguity.
I know to begin working on a universally quantified statement I can invoke universal instantiation. My book defines this as $∀x~P(x)~∴~P(c)$. It then goes on with an example of a formal proof using this on the form $∀x~(P(x)⟹Q(x))~∴~P(a)⟹Q(a)$. How are they applying Universal Instantiation across the $⟹$, when the definition only has a single predicate $P(x)$? Is it that they've set $P(x)$ to mean $P(x)⟹Q(x)$?
Yes, you substitute $c$ for $x$ everywhere in the scope of the quantification. Here that is $(P(x)\to Q(x))$. In Universal Elimination (or Instantiation) you are deducing that if something is true about the universal bound variable $x$, then it will be true for an unbound variable $c$. (Or $a$ or whatever.)
Finally, for direct proof we assume the antecedent is true and try to deduce the consequent. But, doesn't this create the same problem as above? Begging the question that is. Say I have $∀x(P(x)⟹Q(x))$. Then I use direct proof to assume $P(x)$ is true. Well wouldn't I use Universal instantiation here and have
$P(a)$, then using Universal Modus Ponens I could automatically infer
$Q(a)$ is true?
No. If $∀x~(P(x)\to Q(x))$ is what you are trying to prove, then you don't have it. You cannot assert that a conclusion is proven inside its own proof.
Your argument should go: Let $a$ be an arbitrary term. Assume $P(a)$ and derive $Q(a)$ by some valid logic. Thus deducing that $P(a)\to Q(a)$, and since $a$ is arbitrary therefore, by Universal Generalisation, $\forall x~(P(x)\to Q(x))$.
In this case:
Let $m$ be an arbitrary integer, and assume there exists some integer $c$ such that $m=2c+1$. Since for any $c$, $(c+1)^2=c^2+2c+1$ thus $m=(c+1)^2-c^2$.
Therefore: If an integer is odd, then it is the difference of the squares for two integers.
$$\def\fitch#1#2{\begin{array}{|l}#1 \\\hline #2\end{array}}
\fitch{}{\fitch{[m]}{\fitch{\exists k~(m=2k+1)}{\fitch{[b]~m=2b+1}{\fitch{[a]~ b+1}{a^2=b^2+2b+1\\a^2=b^2+m\\m=a^2-b^2\\\exists l~(m=a^2-l^2)\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~(m=2k+1)\to\exists k~\exists l~(m=k^2-l^2)}\\\forall n~(\exists k~(n=2k+1)\to\exists k~\exists l~(n=k^2-l^2))}$$
Time out ... that's enough for now ... maybe more to come later ...
Best Answer
Your plan is exactly backwards.
All proofs should be readable as English prose, i.e. sentences arranged into paragraphs. Symbols may be used as needed, but they need to be human-readable. If you've defined enough symbols, you can write parts of the proof entirely in symbols, provided that they can be parsed back into English.
For example, $$\forall\ x\in\mathbb{R}, \exists\ y\in \mathbb{Z}: x\ge y$$ reads as "For all real numbers $x$, there is an integer $y$, such that $x$ is greater than or equal to $y$."