Meta proof-searching

It has not turned out to be very helpful to prove that specific theorems are provable indirectly, when no actual proof of the theorem was previously known.

There are two settings in mathematical logic, however, where we do show indirectly that particular theorems are provable in particular systems or in particular ways. The difference is that, when we work with particular theorems in these settings, we already know (or assume) the theorems are provable in general, and we are just worried with the specific form of a proof.

The first setting is related to cut elimination. Certain kinds of formal proofs are called "cut free"; these are of a particularly simple form. A general theorem shows that, in many systems, if a theorem is provable then it is provable via a cut free proof. This theorem is effective - there is a procedure to create a cut free formal proof from an arbitrary formal proof. But the size of the cut free proof is often much, much larger than the size of the original proof. So we rarely work with cut-free proofs explicitly. They are used primarily as hypothetical objects.

The second setting is related to showing that particular theorems are provable in weak systems. Sometimes, it can be shown that if a theorem of some particular syntactic form is provable in a stronger system $S$, then it is also provable in a weaker system $W$. These are called "conservation results".

For example, a $\Pi^0_2$ theorem that is provable in the system $\mathsf{WKL}_0$ of second-order arithmetic is also provable in the system $\mathsf{PRA}$ of first-order primitive recursive arithmetic. It is much, much easier to work in $\mathsf{WKL}_0$ than $\mathsf{PRA}$. For example, Kikuchi and Tanaka (1994) showed that certain versions of the incompleteness theorem are provable in $\mathsf{PRA}$ by showing that the theorems are provable in $\mathsf{WKL}_0$, where they can use much more general methods. This only gives a theoretical provability result – no actual proof in $\mathsf{PRA}$ is constructed. In principle, the conservation result gives a method to turn a formal proof in $\mathsf{WKL}_0$ into a formal proof in $\mathsf{PRA}$, but the theoretical provability is of primary interest, not the actual formal proof.

Many conservation results are known. Another example is Shoenfield's absoluteness theorem, which is often used to show that particular results are theoretically provable in ZF set theory, based on the syntactic form of the theorem and the provability of the theorem in ZFC. This allows us to show that some theorems of particular syntactic forms are provable without the axiom of choice based on their provability in ZFC with the axiom of choice .