How many words (i.e. not "math" symbols") should I use in my proofs? ${}{}$ I must once again resort to the advice of this great community.
As I was reading about the pigeonhole principle something about its proof struck me as odd. Allow me to explain:
After reading the "The Foundations: Logic and Proofs" chapter in Rosen's "Discrete mathematics and its applications" book I was left with the feeling/notion that I can (and I ought to) describe all my proof's statements in symbols.
Yet, as you can see in the pigeonhole principle's proof:

We use a proof by contraposition. Suppose  none of the k boxes has
  more than one object. Then the total number of objects would be at
  most k. This contradicts the statement that we have k + 1 objects.

Without a doubt it has more English words than symbols. Yet the proof is actually without flaws. I struggle with the fact that I can't convert it into the A -> B format (I hope you understand what I'm trying to convey).
However, is there a way to symbolically represent what it states (as I'm trying to put it in my mind)? 
Or the only way to argue for this proof, is by using words?
And if so, is there any guide or principle that should tell us when to use words or symbols in our proofs?
 A: Natural language contains more redundancy and is therefore more robust against errors.
When you write proofs, chances are that you will sometimes make mistakes.
This is not a feature of mathematics, but of life in general.
If you mistype a character in a symbolic proof, it can become utterly undecipherable — and wrong, but that's not the biggest issue.
If people understand your story, they can reconstruct a symbolic proof from your story if they want.
If you write your proof in plain English and repeat important things, it is easier for the reader to recall past things when needed and fill in the holes when you leave them.
Natural language is redundant, and therefore messages go through better.
If you ever grade a math exam, you will learn the hard way that people will forget all kinds of silly things and write things unclearly.
A fully symbolic proof is readable only if it's completely correct, a language-oriented proof is readable if it's at least somewhat correct.
Symbolic proofs only contain the proof.
A good proof in words contains more: it describes what is going on and motivates maneuvers instead of only executing them.
This makes a difference to whoever reads your text, including yourself.
A: The advantages of the symbolic representation are that:


*

*You have a greater degree of confidence that what you're doing is actually formal logic and not wishy washy argumentation.

*You are not forgetting something.

*It's much more difficult to write ambiguously with mathematical symbols. English and pretty much all other natural languages don't have a proper way to denote parentheses. Unambiguous English is often verbose and annoying to read.


That said, it is generally easier to read natural language than mathematical symbols. Your documents should be made to optimise the reader's experience, not to impress them with your mastery of mathematical notation.
Just know that a formal proof is one written in a formal language. If you can translate a natural language proof into one written with mathematical symbols then it's okay, not the other way around. Meaning that symbolic proofs don't have to "sound right" in English, while English proofs have to be unambiguously translatable to mathematical notation.
A: I really like all the answers here but there's a point that I think is somewhat implied, but not explicitly stated in any of them. 
The symbols in mathematics are there as an extension of the language (English in this case), not a replacement of it. A statement can always be written in just words, but this is often unnecessarily verbose: "if one more than three times a real number is four, then that number must be one". Equivalently, we could also write it with just symbols (though this depends on a sufficient amount of symbols being defined), but the statement often ends up less clear and requires being deciphered: "$[(x\in\mathbb{R})\wedge (1+3x=4)] \Rightarrow(x=1)$".
If we use language, and allow the symbols to come into play only when they make the statement clearer, we can strike a good balance of readability: "if $x$ is a real number and $1+3x=4$, then $x=1$". 
Proofs are the way of communicating logical statements, so the main goal of a proof (after being correct) is to be readable. This means that, in addition to being clear and precise, the best way to present a proof is the way that will make it most understandable to your intended reader what it's saying.
A: I have a PhD in Mathematics, when I started school I always thought I wanted to use more symbols than words. However, often you cannot do this. A proof is not solving a problem, it is much more! It should certainly contain many words. When you are learning to write proofs, you should actually use more words to make sure your statements are as accurate as possible! As you grow in your mathematical backrground, you will be able to become more concise in your proofs, but this will take time. Your goal in writing a proof should not be length, but rather to explain each step with complete clarity.
A: 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$."
A: I'm going to agree with Kevin that it depends on what you're trying to do.


*

*If you're trying to work out the proof of a statement, symbols and shorthand is very handy to express your thoughts succinctly on paper, or on a board.  Then you can (hopefully) assemble them into a proof.  Symbols are also good for crystallizing a vague thought into a precise mathematical statement.

*When it's time to write it down for someone else to read, though, symbols can increase the semantic density, making it very hard to communicate effectively.  And when used incorrectly, as students often do, symbols can obscure what might be otherwise coherent arguments.  
Obligatory quote from Paul R. Halmos in How to Write Mathematics:

The best notation is
  no notation; whenever it is possible to avoid the use of a complicated alphabetic
  apparatus, avoid it. A good attitude to the preparation of written mathematical
  exposition is to pretend that it is spoken. Pretend that you are explaining the
  subject to a friend on a long walk in the woods, with no paper available; fall back
  on symbolism only when it is really necessary.

A: Don't worry, be happy. It is okay. There are symbols that can be used, but using more of them doesn't really make the logic better. $$\begin{array}{|l}\lVert C\rVert=k\\\lVert\,\bigcup_{B\in C} B\,\rVert=k+1\\\hline~\begin{array}{|l}\forall B\in C~(\lVert B\rVert\leq 1)\\\hline\lVert\,\bigcup_{B\in C}B\,\rVert \leq k\\\bot\end{array}\\\neg\forall B\in C~(\lVert B\rVert\leq 1)\\\exists B\in C~(\lVert B\rVert>1)\end{array}$$ "Given that we have a collection of boxes and the total number of items in the boxes is one more than the number of boxes, then since if each box had no more than one item inside, there could be no more items than the number of boxes, contrary to what was given, therefore there must be some box(es) in the collection with more than one item inside."
A: A lot of this also comes down to writing style. These sorts of proofs aren't just a computational exercise; they're meant to express an idea, to be read and understood, just like any prose writing in any philosophy book. Different writers will want to emphasize different parts, and the same writer may want to express the same proof differently for different audiences. Different branches of mathematics will use different symbols to different degrees.
One key difference between mathematical writing and other writing is that we've incorporated lots of symbols as a way of eliminating ambiguity and removing redundancy, because as mathematicians we are very concerned with being unambiguous, since so much of our work depends on precise definitions. But the symbols are not inherent to mathematical writing, they developed over millennia.
So the symbols aren't necessarily instead of than words, they're in addition. Symbols are only another way to express what we could already express through words and diagrams. How then should you know whether to use more symbols or fewer? The same way you would pick up any writing style: by reading lots of different examples (e.g., textbooks and papers) by different authors, by writing a lot, and by finding trusted writers (published mathematicians) to read and critique your work.
A: 
And if so, is there any guide or principle that should tell us when to use words or symbols in our proofs?

It greatly depends on what you are trying to do with your proofs.
If you "just want to do math," then you should use whatever combination of symbols and words is clearest.  You do need to make sure all of your terms are rigorously defined, but symbols can suffer that problem just as easily as words:
$$
R = \{x|x\notin x\} \\
R \in R \iff R \notin R
$$
On the other hand, there are situations around the foundations of mathematics where thinking of proofs as sequences of purely symbolic statements is useful, without regard for what they may mean in English or another language.  This is particularly important for Gödel numbering and its progeny such as the incompleteness theorems.  This does not mean that you actually have to write proofs in symbols.  It just means that, when proofs are themselves the objects of study, they are easier to reason about if they are written in a formal language. As another example, the "standard" set theory, Zermelo-Fraenkel set theory (ZFC), never defines the symbol $\in$, instead treating it as a primitive operation.
On the third hand, sometimes you may want to use an interactive proof assistant or something similar, especially for large or complex proofs which may otherwise be difficult to verify.  These systems are generally not "smart" enough to deal with natural language proofs, so you usually have to write entirely in symbols or some formal language, similar to a programming language.  Depending on the circumstances, it may or may not be useful or even feasible to prepare a human readable "translation" of such a symbolic proof.  For example, the four color theorem originally did not have a readily comprehensible human proof.
A: Here is a way to put more symbols into the proof.

Let $t$ be the total number of objects, and for $j=1,2,\ldots,k$ let $n_j$ be the number of objects in box $j$.  Suppose $\forall j\ n_j\le1$.  Then
  $$t=\sum_{j=1}^k n_j\le\sum_{j=1}^k1=k\ .$$
  This is a contradiction since $t=k+1$.  So we have $\neg(\forall j\ n_j\le1)$, that is, $\exists j\ n_j>1$.

The point is, is this better than the original?  Do you find it easier to understand and/or more convincing than the original?  If so, go for it.
As for me, I'm with @vadim123 and the comment by @Deepak.  IMHO the original is clear, understandable and convincing, and the proof I have given above is basically a waste of time.
A: Just doing to add to something that's been said probably. 
My lecturers have always said that the real aim of a proof is to convince the reader that they understand what's going on just as well as you. If you can do that using words alone, and symbols won't make it any easier, that's brilliant. If you feel your answer is entirely rigorous, and any possible question an individual has can be answered by reading the proof more carefully then you're lovely and finished. 
Symbols and equations should only be used as an extension of English prose, and if you don't need them then don't use them as an excuse for handwavery. Symbols should be the same as diagrams, something to help you explain, and rarely an excuse for an explanation.
A: For completeness, here is the theorem from Rosen's book that this question uses as an example (Section 6.2 The Pigeonhole Principle, Theorem 1):

THE PIGEONHOLE PRINCIPLE If $k$ is a positive integer and $k+1$ or
  more objects are placed into $k$ boxes, then there is at least one box
  containing two or more of the objects.

And for concreteness, here is how I would prove this.

Consider the bag (or 'multi-set', or 'set but allowing duplicates') $B$ having $k$ elements (the "boxes") whose sum (the total number of "objects") is at least $k+1$, then $%
\require{begingroup}
\begingroup
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
%$
$$\calc
    \text{max}(B)
\op\ge\hints{Dijkstra's 'generalized pigeonhole principle',}\hint{which holds for any bag of numbers}
    \text{average}(B)
\op=\hints{by the definition}\hint{-- to exploit our knowledge of sum and size}
    \text{sum}(B) / \left|B\right|
\op\ge\hint{sum is at least $k+1$, size is $k$}
    (k+1) / k
\op\gt\hint{using $k>0$}
    1
\endcalc$$
Or in words, $B$ has at least one element ("box") larger than 1 (having more than one "object").

For me, a proof like this is often much easier to follow than a natural language paragraph of text.  (I know this is a minority viewpoint and experience, but for those who often fail to understand natural language proofs, I suggest you try finding the level of symbol manipulation that helps you and your readers best.  Dijkstra's EWD1300 could be helpful for you.  He expresses the "desire to let the symbols do the work —more precisely: as much of the work as profitably possible—.")
Also, this proof was very easy to construct, given the basic $\;\text{min} \le \text{average} \le \text{max}\;$ principle (which I learned from EWD980 and EWD1094): at every step there is really only one sensible thing to do.
$%
\endgroup
%$
