Impossibility of certain methods of proof?

Whether you can prove a given theorem "using" a particular proof strategy is kind of a slippery concept. If you have at least one proof, then it is always possible to disguise the proof such that it looks -- at least at first glance -- like the concluding step is a proof by contradiction, an induction, etc. In order to make the question interesting, you'd need first to provide a definition that could distinguish "disguises" from "real uses" of the proof technique in an objective way, and finding such a definition is very hard. Some attempts at this do exist, under the name of relevance logics, but they are not part of the mathematical mainstream and mostly considered a specialist tool for use in machine learning and related disciplines.

However, it is much more fruitful to approach the question from the opposite direction. Instead of asking "is it possible to prove my theorem with such-and-such technique?", you can ask "is it possible to prove my theorem without ever using such-and-such technique?". That's a qualitatively different question, because there are usually many different steps in a proof, and while it is fairly easy to shove more techniques into the proof, it is a different matter to remove a particular techniques from it completely.

For example it can make lots of sense to ask: Can such-and-such theorem be proved without ever using proof by contradiction to prove a positive statement? Or: can such-and-such theorem be proved without using the Axiom of Choice? Of course one still needs to be fairly specific about which other techniques are available; there are possible proof strategies that can be used as drop-in replacements for proof-of-a-positive-statement-by-contradiction, and if you're not excluding those too, you're back to a non-interesting question. Also, you'd want to specify that you don't want simply to apply another theorem which is itself proved by contradiction, or explicitly specify that such and such theorems may be assumed without worrying about how they were proved (thus effectively declaring them to be axioms for the purpose at hand).


In formal logic there exists no bound on the number of proofs for any given statement, in principle. A (formal) proof gets defined basically as a sequence of logical formulas (wffs) such that each formula comes as permissible to the proof system involved. There exists no part of the definition of a proof such that it prohibits repeating formulas ad nauseum, or writing proofs with loops in say a natural deduction system where you introduce and discharge the same hypothesis over and over again in the same way, nor prohibiting the use of proof by contradiction in proving that (p->p). So, there does exist an infinity of proofs... even in classical propositional logic.

No proof methods, by which I interpret here as rules of inference, can get eliminated either. Proofs can use rules of inference to infer formulas which we don't end up using to infer the conclusion. Those formulas not used to infer the conclusion still exist within the sequence of the proof, and thus still qualify as part of the proof. This entails that every single rule of inference for the system can ultimately get used in a proof of some conclusion if desired. To perhaps make this clearer, say we want to prove that (p->p) in a natural deduction framework for classical propositional logic, and precede as follows:

1 | p assumption
2 | (p v p) 1 disjunction introduction
3 (p->p) 1-1 conditional introudction

Since a formal proof consists of a sequence, and the sequence

[p, (p v p), (p->p)]-1

differs from

[p, (p->p)]-2

we have two different proofs there. If we could rule out disjunction introduction as a permissible rule for proving that (p->p), then we would have to rule out proof 1 above. But, it does satisfy the definition of a proof, so we can't rule it out disjunction introduction for proving that (p->p). Since the use of disjunction introduction here ultimately could work just like any other rule of inference of the proof system involved, all rules of inference not only can, but do appear in at least one proof of every theorem of classical propositional logic. Actually, if you combine that with the idea in the first paragraph, there exist an infinity of proofs of every theorem of classical propositional logic using every rule of inference of the proof system... so long as the number of rules of inference is finite.

So to this "However if we are interested not in the most straightforward proof of a statement but rather all possible proofs, is it possible to eliminate proofs via particular methods, or to put a bound on the number of possible proofs for a given statement?" I answer "no, and no."

"It is easy to prove the value of the above sum using mathematical induction, but can it be proved in any other way, say via contradiction?" yes.

"Is it ever the case that certain statements cannot be verified using particular lines of proof (contrapositive, contradiction, etc.)?" no.

"How does one go about proving that a particular method of proof cannot be used to prove a particular statement?" You can't do this under usual definitions of a formal proof at least, for a system with valid rules of inference. All methods can always get used somewhere in a proof of any given theorem. If they couldn't get used somewhere in some proof, such rules of inference wouldn't come as valid in the first place. If the rules of inference used aren't valid in the first place, then such a proof system isn't sound. Thus, you could start with a classically true premise and infer classically false conclusions from such a premise.

"Often one will begin employing a particular method and find it not to work or make sense, but how can one (or can one) actually prove that it cannot be used?"

You can't do it.