"Strange" proofs of existence theorems This question isn't related to any specific research.  I've been thinking a bit about how existence theorems are generally proven, and I've identified three broad categories: constructive proofs, proofs involving contradiction/contrapositive, and proofs involving the axiom of choice.
I'm convinced that there must be some existence theorem that can be proven without any of these techniques (and I'm fairly confident that I've probably encountered some myself in the past haha), but I can't come up with any examples at the moment.  Can anyone else come up with one?  I'd also like to stipulate the following conditions:


*

*The proof can't piggyback on another existence theorem whose proof involves one of the above-mentioned devices.

*It has to be a theorem of ZF - no exotic and "high power" axioms allowed!


Now for the interesting question: is there any existence theorem (again in ZF) such that every one of its proofs is of this type?  Has anyone investigated something like this?  If so, what results exist?
Edit:
This issue came up a few times in the comments: here I use "constructive" in its weaker sense (i.e. a constructive proof is merely one that constructs an object and shows that it satisfies the required properties).  The stronger sense - that the proof may not use the law of excluded middle or involve any infinite objects - is not what I'm invoking.
 A: How do you classify the proof that Chomp is a first player win?  It's nonconstructive.  It uses excluded middle, but it isn't a proof by contradiction.
A: There are probabilistic proofs of existence. Do they fall into one of your three categories?
For example, prove the existence of a real number that is normal in all bases: To do it, we show that "almost all" real numbers (according to Lebesgue measure) have that property.  Therefore at least one real number has the property.  And the point is: this "almost all" proof is easier than constructing an explicit example.
See some nice examples due to Erdős in the cited Wikipedia page which use only finite probability spaces.  If we show that a probability is ${} > 0$, then the set is not empty.
A: There are many existence proofs that are "constructive" in the weak sense that they show that if you perform some kind of exhaustive search for the object then the search will always succeed, but are "nonconstructive" in the sense that they do not describe an explicit example of the object in question, and typically the exhaustive search is infeasible in practice.  Probabilistic proofs, mentioned in another answer, are an example, but there are others.


*

*Counting arguments.  Others have mentioned some of these; another example is the proof of the existence of a bijection between the set of conjugacy classes of a finite group and the set of non-isomorphic irreducible finite-dimensional complex representations of the group.  This is usually proved by showing that irreducible characters form a basis for class functions, which is a dimension-counting argument.  But the proof does not yield an explicit bijection and in general there is no canonical bijection.

*Pigeonhole arguments.  One lesser-known example that I like arises in the proof of Rota's Basis Conjecture in the cases where the Alon–Tarsi conjecture is known.  The conclusion is that a certain arrangement of vectors in a matrix must exist, but a key step in the argument is that a sum of exponentially many determinants is nonzero, and so at least one of the determinants must be nonzero.  The proof does not yield a feasible algorithm for the desired arrangement.

*Parity arguments.  Any finite graph has an even number of odd-degree nodes. This can be used to prove, for example, that a graph whose vertices all have odd degree must have an even number of Hamiltonian cycles.  So if you are given one Hamiltonian cycle, the theorem tells you there is another one, but does not give you an efficient way of finding another one.
There are several other types of nonconstructive arguments known, e.g., using the combinatorial Nullstellensatz, or fixed-point theorems.  See for example Noga Alon's paper on nonconstructive proofs in combinatorics.  For one final example, I like the paper by Belkale and Brosnan that disproves a conjecture of Kontsevich that certain functions associated with finite graphs are always polynomials.  Their proof shows that the space spanned by all such functions is much larger than the space of polynomials, but it does not yield an explicit graph whose function is not a polynomial.  An explicit counterexample was not obtained until much later by Brown and Schnetz.
A: There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$ is rational. The proof considers two cases: $\sqrt{2}^\sqrt{2}$ is irrational, or it is rational. In either case we can find such $a$, $b$. Then it applies the law of excluded middle to say one of these cases in fact holds. You can see a discussion of the proof here: http://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/.
You mentioned “proof by contradiction” in your question, but to me this application of the law of the excluded middle is conceptually different than proof by contradiction.
(By the way, as discussed in that blog post, this is certainly not a serious application of the law of excluded middle because there are other ways to prove the result in question. But it is a cute proof.)
EDIT: I believe there might be more serious proofs along these lines in number theory, that go something like “either the Riemann hypothesis holds, or it doesn’t. In the first case...; in the second case...” Or the same but with “Siegel zero existing.” But I don’t know a particular example off the top of my head.
A: C. De Lellis & L. Székelyhidi proved the existence of weird solution of the Euler solutions for an incompressible perfect fluid. These solutions violate the conservation of energy in an arbitrary way.  The proof, based on so-called "convex integration" uses in a crucial way Baire's category theorem. Notice that the result does not depend upon the axiom of choice. Whether the proof is constructive depends on how much you consider Baire as a constructive argument.
A: This is the strangest existence proof I know; it is a nonconstructive proof that there exists a proof of a certain statement. In other words, we prove the statement by proving that a proof exists.
I'm thinking of Lob's theorem. The Godel sentence is a number-theoretic assertion $G$ which informally says of itself that it cannot be proven in Peano Arithmetic (PA). Godel showed that if PA is $\omega$-consistent, then $G$ is true but there is no proof of $G$ in PA.
The Lob sentence $L$ is the analogous assertion which informally says of itself that it can be proven in PA. Is it true or false?
It is true. For suppose $L$ cannot be proven in PA. Then the system PA' = PA + $\neg L$ is consistent. But it is clear, and can be proven in PA, that if $L$ is provable in PA then $L$ is true. Since PA' assumes $\neg L$, we can therefore prove in PA' that $L$ is not provable in PA. Thus we can prove in PA' that PA + $\neg L$, i.e., PA' itself, is consistent. By Godel's second incompleteness theorem this is impossible, since we already knew that PA' is consistent (a consistent theory cannot prove its own consistency). Therefore the assumption that $L$ is not provable in PA leads to a contradiction, and we conclude that $L$ is provable in PA.
It's crazy because we know there is a proof of $L$ in PA but we don't know what that proof is!
So what is this mysterious proof of $L$? It is the argument I just gave, which can be formalized in PA.
That is the most bizarre existence proof I know.
A: Many existence proofs in analysis / probability follow this line of argument: 
1. Construct a family of objects that approximately satisfy some desired property.
2. Show that the family is precompact.
3. Show that every accumulation point must satisfy the desired property.
I suppose that to some extent this would often count as a constructive proof since in many cases one can impose additional constraints until the possible limits are reduced to a single point, but this may require some non-trivial amount of work...
A: While an informal interpretation of the question seems more appropriate, a formal one is possible, too. We then enter the realm of constructive reverse mathematics.
It is (reasonably) clear what it means that a theorem has a constructive proof.
"All proofs of the theorem make use of contradiction" can be formalized as "the theorem implies some form of double-negation elimination over a weak base system (eg BISH)."
Thus, every non-constructive theorem that does not imply a form of DNE would count as an example.
Famous examples here would be weak Konigs Lemma (every infinite binary tree has an infinite path) and the intermediate value theorem.
Looking at eg the proof of the latter via bisection, we see a hybrid between constructive proof and proof by contradiction. We expect bisection to work, and then see that it can only fail if we hit upon a root one of the midpoints.
A: I would call the proof for the existence of the limit $0$ of the Goodstein sequence pretty weird: it uses infinite ordinals, but the sequence itself is within $\mathbb{N}$. In Peano artithmetic, Goodstein's theorem is unprovable.
