Is it possible to prove a mathematical statement by proving that a proof exists?

I’m sure there are easy ways of proving things using, well… any other method besides this!
But still, I’m curious to know whether it would be acceptable/if it has been done before?


There is a disappointing way of answering your question affirmatively: If \phi is a statement such that First order Peano Arithmetic \mathsf{PA} proves “\phi is provable”, then in fact \mathsf{PA} also proves \phi. You can replace here \mathsf{PA} with \mathsf{ZF} (Zermelo Fraenkel set theory) or your usual or favorite first order formalization of mathematics. In a sense, this is exactly what you were asking: If we can prove that there is a proof, then there is a proof. On the other hand, this is actually unsatisfactory because there are no known natural examples of statements \phi for which it is actually easier to prove that there is a proof rather than actually finding it.

(The above has a neat formal counterpart, Löb’s theorem, that states that if \mathsf{PA} can prove “If \phi is provable, then \phi“, then in fact \mathsf{PA} can prove \phi.)

There are other ways of answering affirmatively your question. For example, it is a theorem of \mathsf{ZF} that if \phi is a \Pi^0_1 statement and \mathsf{PA} does not prove its negation, then \phi is true. To be \Pi^0_1 means that \phi is of the form “For all natural numbers n, R(n)“, where R is a recursive statement (that is, there is an algorithm that, for each input n, returns in a finite amount of time whether R(n) is true or false). Many natural and interesting statements are \Pi^0_1: The Riemann hypothesis, the Goldbach conjecture, etc. It would be fantastic to verify some such \phi this way. On the other hand, there is no scenario for achieving anything like this.

The key to the results above is that \mathsf{PA}, and \mathsf{ZF}, and any reasonable formalization of mathematics, are arithmetically sound, meaning that their theorems about natural numbers are actually true in the standard model of arithmetic. The first paragraph is a consequence of arithmetic soundness. The third paragraph is a consequence of the fact that \mathsf{PA} proves all true \Sigma^0_1-statements. (Much less than \mathsf{PA} suffices here, usually one refers to Robinson’s arithmetic Q.) I do not recall whether this property has a standard name.

Here are two related posts on MO:

  1. \mathrm{Provable}(P)\Rightarrow \mathrm{provable}(\mathrm{provable}(P))?
  2. When does ZFC \vdash\ ‘ ZFC \vdash \varphi\ ‘ imply ZFC \vdash \varphi?

Source : Link , Question Author : chubbycantorset , Answer Author : Community

Leave a Comment