5
$\begingroup$

Suppose you have a particular theory (ex: $ZFC$) in which you want to prove a statement $\phi$. One can attempt to find a proof of $\phi$ that can be verified, but another tactic can be to find a proof for the existence of a proof of $\phi$

Are there any examples of such "non constructive proof of proofs" where someone proved that "a proof of $\phi$" exists but did not explicitly find that proof itself? I am curious if for certain problems this would be more tractable/efficient to compute the original proof of the sentence.

$\endgroup$
  • $\begingroup$ In which theory would that proof take place? I mean... If ZFC proves, via $\chi$, that there is a proof $\psi$ of $\phi$, then $(\chi,\phi)$ is a proof of $\phi$ in ZFC. $\endgroup$ – Stefan Mesken Jul 18 '16 at 18:59
  • $\begingroup$ @Stefan: how is a pair of proofs a proof? $\endgroup$ – Rob Arthan Jul 18 '16 at 19:25
  • 2
    $\begingroup$ @Stefan For any given $\phi$, ZFC need not prove the sentence "If ZFC proves '$\phi$', then $\phi$". If it did, ZFC would prove its own consistency. $\endgroup$ – Mike Haskel Jul 18 '16 at 21:54
  • 1
    $\begingroup$ I imagine Stefan may be informally referring to Löb's theorem. $\endgroup$ – Andrés E. Caicedo Jul 19 '16 at 0:10
  • 1
    $\begingroup$ Yeah, I thought so. Second order has a specific meaning in logic, it means that we can quantify over sets and relations (in the case of set theory that would mean classes). What you mean is "meta", proofs live in the meta theory. $\endgroup$ – Asaf Karagila Jul 19 '16 at 4:13
3
$\begingroup$

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 .

$\endgroup$
  • $\begingroup$ Interesting, but this suggests it is possible, if you fix your model of logic say $A$, consider then a bigger model $B$, $B$ can be searched for proofs of the form "$A$ contains a proof of $\phi$", and perhaps for some contrived examples where we impose specific structure on $A$ and $B$ it might be easier to find that, just not in a conventional setting such as ZFC $\endgroup$ – frogeyedpeas Jul 20 '16 at 7:17
  • $\begingroup$ The particular idea of searching $B$ for "$A$ contains a proof of $\phi$" is not something that has been found effective in experience. In general, we don't search blindly for proofs, because the search space is so large that in practice we never find the proof we want. We do sometimes show that "$A$ contains a proof of $\phi$" without constructing an explicit proof in $A$ - that is what I wanted to show in my answer. But in these cases, we already have a proof of $\phi$ in a stronger system. So we already know that $\phi$ is true, just not whether it is provable in $A$. $\endgroup$ – Carl Mummert Jul 20 '16 at 11:19
  • $\begingroup$ I see, that makes sense $\endgroup$ – frogeyedpeas Jul 20 '16 at 20:52
0
$\begingroup$

Gödel proved that theories like ZFC (or any theory with enough structure to have arithmetic, for that matter) is either complete (all statements are provable, even statements such as "ZFC proves that ZFC proves that ZFC proves that ... $\varphi$) but inconsistent (derive contradictions from tje axioms) or consistent (not-inconsistent) but incomplete (there are statements you can not prove, such as the negation of a given $\varphi$ or the statement "ZFC is consistent"). Therefore, if you ask for the general method to find a proof that a certain proof exists, then you are assuming ZFC et al to be complete. But by Gödel's theorems, that would yield your theory inconsistent and the game is over.

$\endgroup$
  • 1
    $\begingroup$ Any theory with enough structure to have arithmetic and is recursively enumerable $\endgroup$ – Stefan Mesken Jul 20 '16 at 1:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.