If we want to have new symbols in our language, which are definitional abbreviations for strings of symbols already in our language's alphabet, do we have to add them to that alphabet?
For example, when writing down the alphabet for the language of set theory, then if we take ${\land}$ and ${\lnot}$ as primitives, do we have to write ${\implies}$ in the language's alphabet, considering that $a{\implies}b$ is the same thing as ${\lnot}(a{\land}{\lnot}b)$?
If yes, why yes? If not, why not?
On
The concepts of Formal system and Formal languae are needed in order to specify in a totally unambiguous manner the syntactical behaviour od a system or theory.
In principle, they may be used in a fully automatic way by a machine or computer.
Abbreviations are useful in order to improve human readibility of formulae and theorems.
For automatic processes, the issue of improving readibility is pointless: thus, abbreviations are useless.
From a "logical point of view", definitional abbreviations are not part of the alphabet, simply because they introduce new symbols that are not part of the original stock of symbols: the primitive ones.
It depends, but basically, yes you do. If you are going to have a formal definition of the syntax of a theory, you can't omit some of the symbols you want to use in the theory. If you did, then obviously any expression using symbols outside of the specified alphabet wouldn't even be syntax, let alone well-formed.
The only reason I say it depends is that you can view a definition of that form as defining a new theory that, by definition, is interpretable into the old theory in a sound and complete manner. In particular, it is a conservative extension, and in particular, an extension by definition.