# Impossibility of certain methods of proof?

There are many methods available for proving a given statement: direct proof, proof by induction, proof by contrapositive, proof by contradiction, etc. In some cases there is an obvious method that should be employed, such as using induction to prove that $\displaystyle\sum_{i=0}^n i=\dfrac{n(n+1)}{2}$. 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?

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? Starting off with "Suppose that the value of the sum does not equal..." does not seem very promising. Of course I am not asking specifically about this example, and alternate proofs of this equality are not relevant here.

So my questions are:

Is it ever the case that certain statements cannot be verified using particular lines of proof (contrapositive, contradiction, etc.)? Of course, induction is not suitable for many proofs, but this seems to be somewhat of a special case, being built on a theorem and not basic logic, such as with contradiction, etc.

How does one go about proving that a particular method of proof cannot be used to prove a particular statement? 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?

As asked in the first paragraph, is it possible to bound the number of possible proofs or methods of proof for a given statement?

If either of my tags are inappropriate, feel free to change them. I am not not well-versed in either area and that is partly why I'm interested in this question.

-
Before one can count or classify proofs one needs a precise notion of equality. Do you have one? – Bill Dubuque Jun 11 '12 at 1:00
The question of whether you need proof by contradiction to prove something is addressed to some extent in intuitionistic logic (en.wikipedia.org/wiki/Intuitionistic_logic), in which the law of the excluded middle does not necessarily hold. A closely related proof strategy, however, is intuitionistically valid: math.andrej.com/2010/03/29/… – Qiaochu Yuan Jun 11 '12 at 1:04

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 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.

-
Is there any hope for a cleaner answer (not that I don't like this answer) if I reword to something like "Can every true statement be proved by employing a single logical statement (such as $p \Rightarrow \neg p$), for all such statements?" Is there any way to formally take all proofs and sort of 'mod out' a particular logical statement that is superfluous, such as $p \vee p$ in your example? Again, I know nothing of this sort of thing, but am curious. – Alex Petzke Jun 11 '12 at 13:44
@AlexPetzke I don't know if I understand this question exactly ""Can every true statement be proved by employing a single logical statement (such as p⇒¬p), for all such statements?"" I don't know of any way to formally "mod out" all superfluous statements. How does one formally determine if something is superfluous or not? Though we might share a common intuition about such a concept as superfluity, that doesn't mean we have a formal, precise definition of superfluity. You basically will run into the problem of defining a concept like "essence" in a formal, precise way. – Doug Spoonwood Jun 11 '12 at 18:53
There's clearly more to this than I am aware of (not at all surprisingly). Thanks for the detailed answer. – Alex Petzke Jun 11 '12 at 21:51

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).

-

Here's an example of a result saying that a given result cannot be proven in a given way:

Dirichlet's Theorem states that for integers $m,n$ where $\gcd(m,n)=1$, there are infinitely many primes $p\equiv m\mbox{ mod } n$. Some particular instances can be proved similarly to Euclid's proof of the infinitude of primes. For instance, let $m=3,n=4$ and $p_1,p_2,\ldots,p_n$ be primes congruent to $3\mbox{ mod }4$. Then $p=4p_1\ldots p_n-1$ is an integer that is $3\mbox{ mod }4$, but has none of the $p_i$ as a factor. So either $p$ is prime or has a prime factor not a $p_i$, and one of those must be $3\mbox{ mod }4$.

Other cases (such as primes $1\mbox{ mod }4$) are harder, but their proofs have the same punchline, and one naturally asks if every case has such a proof.

In 1912, Schur proved that such a proof is possible for primes congruent to $m\mbox{ mod }n$ if $m^2\equiv 1\mbox{ mod }n$ and in 1988 Murty proved that this condition is necessary, after equating the existence of a Euclidean-style proof with the existence of a certain type of polynomial.

A link to a SE question with some links is here and I think one of the better expositions linked is this one.

-
I don't see how what you're written here implies anything about an impossibility of a proof by a certain method. Also, the proofs you've referred to consist of informal proofs. I suspect you may have also misunderstood what it means for a condition to come as necessary, since if B is a necessary condition of A, then (A->B). That doesn't mean that if you have A, and if B is a necessary condition of A, you will necessarily have B, since not all logical systems have modus ponens as a rule of inference. – Doug Spoonwood Jun 12 '12 at 16:07
@DougSpoonwood Yes, it is about informal proofs. The OP didn't seem only interested in formal logic so this seemed like something of interest (and since it is informal we definitely have modus ponens). And the result says that for integers $m,n$ where $m^2$ isn't congruent to $1\mbox{ mod }n$, there can be no Euclidean-style proof. – Francis Adams Jun 12 '12 at 16:34
I disagree that since it is informal we definitely have modus ponens. If the person we try to the communicate the proof accepts modus ponens, then we have it, if they don't accept it, we don't have it. If one has three truth values in informal logic with semantics such that (t->u)=t, (t->t)=t, (t->f)=f, (f->t)=t where t indicates truth, "u" a third truth value, and "f" falsity, then "->" qualifies as a logical implication operation, and modus ponens fails. – Doug Spoonwood Jun 12 '12 at 17:39
I guess by informal proof I was thinking of proofs in natural language that use standard assumptions of logic and set theory used in typical mathematical practice. Sorry for being unclear. – Francis Adams Jun 12 '12 at 19:41