Has anyone ever studied which proof types are feasible for which theorems in mathematics? If not, why not?

Question

For instance, when asked to prove that sqrt(2) is irrational, we go straight for the proof by contradiction where we assume it’s equal to a/b in lowest terms and end up with a and b not being in lowest terms. On the other hand, the proof of some other theorem might always be done directly, or happen to be feasible using multiple proof types. If it hasn't already been done, could studying which proof types are feasible for which theorems in mathematics ever have any practical use, or would this just not be useful information to look into?

Answer 1

As pointed out by user509184 in a comment, reverse mathematics is exactly the study of which foundational systems can prove a theorem of interest. Historically, this has focused on systems of arithmetic, in particular systems weaker than PA and systems stronger than PA but not going beyond HOA (higher-order arithmetic). For some philosophical remarks on this, read this post. Note that the "Big Five Systems" here are all classical systems, due to the undeniable extent of real-world applications of (classical) real analysis, which also explains why a lot of the theorems investigated in reverse mathematics are related to logic or real analysis. In particular, it has been consensus among expert logicians for a long time that PA actually holds a special place; it can be conservatively extended to a system called ACA0 that so far is capable of proving correctness of every application of mathematics to the real world (excluding insubstantial consequences of the incompleteness theorems such as the fact that a program searching for a PA-proof of "0=1" will never halt).

It may not be obvious how the above answers your question, but in fact it has very important implications for applied mathematics. It implies that we ought to expect to be able to prove any practically useful real-world fact that can be mathematically stated using ACA0.

Now you also asked about proof techniques. Firstly you have a misconception about the proof that √2 is irrational; by definition of "irrational" you have no choice but to prove a contradiction under the assumption that √2 is rational! Such analysis of proof techniques can be done in some other cases too. But for reasons related to the incompleteness theorem, it is not possible to systematically determine whether a statement can be proven or not. And even if a statement is guaranteed to be provable, it is usually also hard to efficiently find a proof. For example, every first-order statement about ⟨ℝ,0,1,+,·,<⟩ can be either proven or disproven within the FOL theory RCF, but the shortest proof length may be doubly-exponential in the length of the statement! So there is a fundamental limit to the efficiency of proofs or disproofs of first-order statements about real numbers.

See also this post about why mathematics in general is inherently hard, which also implies hardness of figuring out which proof techniques/tactics are useful for a given theorem. Note that one must be careful in talking about known provable statements, because the trivial algorithmic procedure that searches through all proofs in length-lexicographic order will find a proof if it exists.

In an orthogonal direction, there is the BHK interpretation for IFOL (intuitionistic FOL), which implies that any theorem that cannot be witnessed by a computable function necessarily cannot be proven within IFOL from any axioms that have computable witness functions. And since the only difference between IFOL and FOL (in suitable axiomatizations) is either ¬¬-elimination or LEM, you know immediately that to prove these theorems you have to use one of these.