The standard way to prove the Pigeonhole Principle that, putting $n+1$ pigeons into $n$ pigeonholes necessitates the existence of at least one pigeonhole with at least 2 pigeons is by contradiction. Namely, that if it is false that there is at least one pigeonhole in which there are at least two pigeons, then every pigeonhole has at most one pigeon, so there are at most $n$ pigeons.
Can proof by contradiction be avoided?
Yes, you can use proof by contrapositive instead, which looks similar to but does not actually require contradiction. We might as well prove the general form: if at least $mn + 1$ pigeons are sorted into $n$ holes then at least one hole contains at least $m + 1$ pigeons.
The contrapositive is: if all $n$ holes contain at most $m$ pigeons then there are at most $mn$ pigeons. But this is clear, we just add up the numbers of pigeons in the holes. (Note that we need to say "at least $mn + 1$ pigeons" and not "$mn + 1$ pigeons" to get this to work.)
It's frustratingly common that people use proof by contradiction when a proof by contrapositive would suffice and it's worth knowing how to spot the difference. There is a real difference: at every point in a proof by contrapositive you are writing down a true statement. In a proof by contradiction you know that you're going to eventually write down a false statement and you're waiting to see when it happens. It's a lot easier to make a mistake that way because intermediate steps in a proof by contradiction can't be inspected for validity! If you make a mistake in a proof by contradiction you just think you're done. This is part of how cranks keep coming up with 1-page proofs of Fermat's last theorem and so forth.
Below are two formalized (in Agda) proofs of a version of the pigeonhole principle. The way I've stated the principle is thus:
Suppose you have a list of natural numbers. Then if the sum of the numbers (number of pigeons) is greater than the length of the list (number of holes), the list has an element that is greater than 1 (hole has more than 1 pigeon).
First I have a couple simple proofs common to both:
lift : ∀{m : ℕ} {ms}
→ Σ[ n ∈ ℕ ] (n ∈ ms) × (1 < n)
→ Σ[ n ∈ ℕ ] (n ∈ m ∷ ms) × (1 < n)
lift (n , n∈ms , 1<n) = (n , there n∈ms , 1<n)
test : (n : ℕ) → (n ≤ 1) ⊎ (1 < n)
test 0 = inj₁ z≤n
test 1 = inj₁ ≤-refl
test (suc (suc n)) = inj₂ (m≤m+n 2 n)
Here is a proof that first proves the 'negative' version of the theorem:
down : ∀{m ms}
→ (∀ n → n ∈ (m ∷ ms) → n ≤ 1)
→ ∀ n → n ∈ ms → n ≤ 1
down all n n∈ms = all n (there n∈ms)
negative : (l : List ℕ)
→ (∀ n → n ∈ l → n ≤ 1)
→ sum l ≤ length l
negative [] all = ≤-refl
negative (n ∷ ns) all with test n
... | inj₁ n≤1 = +-mono-≤ n≤1 (negative ns (down all))
... | inj₂ 1<n = ⊥-elim (<⇒≱ 1<n (all n (here refl)))
up : ∀{m ms}
→ m ≤ 1
→ (∀ n → n ∈ ms → n ≤ 1)
→ ∀ n → n ∈ m ∷ ms → n ≤ 1
up m≤1 all n (here refl) = m≤1
up m≤1 all n (there n∈ms) = all n n∈ms
search : (l : List ℕ)
→ ¬ (∀ n → n ∈ l → n ≤ 1)
→ Σ[ n ∈ ℕ ] (n ∈ l) × (1 < n)
search [] ¬all = ⊥-elim (¬all λ _ ())
search (n ∷ ns) ¬all with test n
... | inj₁ n≤1 = lift (search ns (¬all ∘ up n≤1))
... | inj₂ 1<n = n , here refl , 1<n
positive : (l : List ℕ)
→ length l < sum l
→ Σ[ n ∈ ℕ ] (n ∈ l) × (1 < n)
positive l l<s = search l λ all → <⇒≱ l<s (negative l all)
I tried using an actual classical principle instead of search, but it actually ended up longer.
Here is the direct version (note, there's an omitted case for the empty list in the proof, because the computer can tell that $\mathsf{length}\ l < \mathsf{sum}\ l$ is impossible for the empty list):
cancel : ∀{i j k l} → k ≤ i → i + j < k + l → j < l
cancel {i} k≤i i+j<k+l =
+-cancelˡ-< i (<-transˡ i+j<k+l (+-monoˡ-≤ _ k≤i))
positive : (l : List ℕ)
→ length l < sum l
→ Σ[ n ∈ ℕ ] (n ∈ l) × 1 < n
positive (n ∷ ns) l<s with test n
... | inj₂ 1<n = (n , here refl , 1<n)
... | inj₁ n≤1 = lift (positive ns (cancel n≤1 l<s))
As you can see, the proof of the negative statement is structurally almost the same as the direct proof of the positive statement, because they both just do induction on the list. Proving the negative version first just led to extra work deriving the actual desired statement afterwards (which itself is about as long as the direct proof).
In cases like this—decidable propositions about finitely many numbers—procedures like $\mathsf{search}$ allow proof-by-contradiction to be used constructively. You can either look at this as classical logic being justified, or adding no essential power in those cases.
However, it's also not necessarily the case that proof-by-contradiction makes your proofs any easier/shorter. Frequently mathematicians use such proofs out of habit, rather than because they are necessary or (by any measure) beneficial. You could assume that you'd already proved the negative statement, I suppose, but you could just as well have already proved the pigeonhole principle and derive the negative statement from it.
Here is the complete file containing the proofs.
There are versions of the pigeonhole principle where the direct proof is much more difficult than the one here. However, the reason those are difficult has to do with manipulating functions between finite types, which is the analogue of $\mathsf{cancel}$. It's possible the indirect proof could be easier in that case, but the analogues of facts about ordering in it are also going to be more difficult to prove.
The principle is easy to prove by induction.
The claim holds for $n = 1$: in that case you have $2$ pigeons in the unique pigeonhole. Suppose that the claim holds for $n$, and consider $n+2$ pigeons in $n+1$ pigeonholes. Then either there are at least $2$ pigeons in the pigeonhole number $n+1$, or there is at most $1$ pigeon in the pigeonhole number $n+1$. In the latter case, there are least $n+1$ pigeons in the pigeonholes with numbers $1$ to $n$. By the inductive hypothesis, one of these pigeonholes must contain at least $2$ pigeons.
