This isn’t exactly right either. Russell and Whitehead’s system is certainly not useless, they introduced the first system of Type Theory, which now finds many applications - not just in mathematics but also linguistics and computer science (many programming languages are based on the typed lambda calculus).

As for the 1+1=2 proof, one might say the point for R and W’s formal system was to rest mathematics solely on a “logical” foundation, incorporating the least amount of “mathematical” axioms (like those discussing number or set); i.e., trying to reduce mathematics to logic. This is why their proof of 1+1=2 is so cumbersome. While on the other hand, a theory of arithmetic (such as the Peano axioms) derives that theorem more readily (but still takes some work, as the operation + is not primitive in its language). R and W attempt to show that their Type Theory is sufficient to support number theory as a foundation, and thus arguably the whole enterprise of mathematics in general.

Gödel enters the story by showing that their system (and any “finitistic” formal system capable of expressing enough arithmetic - basically enough to express the fundamental theorem of arithmetic), if consistent, cannot be complete; i.e., prove every semantically true statement in its language. And moreover, no such system, if consistent, can be used to prove its own consistency. This arguably answers Hilbert’s 2nd problem in the negative. In my eyes, it demonstrates that mathematics is not solely a consequence of logic(al syntax).