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.

20more comments