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?

  • 2
    $\begingroup$ Sure. For certain statements, you can even prove them by showing that there is no proof of their negation. $\endgroup$ Jan 14, 2013 at 6:52
  • 10
    $\begingroup$ @AndresCaicedo not true. If you know you can't disprove something, then it's consistent, not proven. AC and ~AC are both consistent with ZF $\endgroup$ Jan 14, 2013 at 6:54
  • 3
    $\begingroup$ I'm wondering how would you non-constructively prove that a proof exists. The proof of a proof would then count as a proof of the original concept. $\endgroup$ Jan 14, 2013 at 6:57
  • 2
    $\begingroup$ @Jan Dvorak I understand your point The interesting question is "Are there any known theorems that use this proof-strategy in their proof"? $\endgroup$
    – Amr
    Jan 14, 2013 at 7:03
  • 5
    $\begingroup$ @JanDvorak I am well aware of these issues, of course. The statement I wrote can be made precise, and the precise versions are true. For example, it is a theorem of ZF that any $\Pi^0_1$ statement about the natural numbers that is not refutable in PA is true. $\endgroup$ Jan 14, 2013 at 7:05

2 Answers 2


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$?
  • $\begingroup$ Good answer! Also, if we were to name this proof technique, what do you think would be appropriate? $\endgroup$ Jan 14, 2013 at 18:04
  • $\begingroup$ (I've moved a comment answering the follow-up question above to the body of the answer, and added some references.) $\endgroup$ Sep 24, 2013 at 15:41
  • $\begingroup$ A sort of 'flip' of this, of course (and one catch with the purported approach to e.g. Goldbach, which Andres is certainly well aware of), is that there is (almost certainly) no statement $\phi$ for which we can prove that e.g. PA doesn't prove $\phi$! This is because if PA is inconsistent then it proves everything, so proving that there's a statement that PA doesn't prove is tantamount to a proof of the consistency of PA, and as such (by Godel) is impossible within PA itself unless the theory is inconsistent. (Note: this doesn't rule out proofs from outside PA,a la Goodstein...) $\endgroup$ Sep 24, 2013 at 16:04
  • $\begingroup$ @StevenStadnicki: Hmm you should have said "there is (almost certainly) no statement $φ$ for which we can prove within PA that PA doesn't prove $φ$" just so that people don't misunderstand. $\endgroup$
    – user21820
    Feb 8, 2016 at 3:39

I'd say the model-theoretic proof of the Ax-Grothendieck theorem falls into this category. There may be other ways of proving it, but this is the only proof I saw in grad school, and it's pretty natural if you know model theory.

The theorem states that for any polynomial map $f:\mathbb{C}^n \to\mathbb{C}^n$, if $f$ is injective (one-to-one), then it is surjective (onto). The theorem uses several results in model theory, and the argument goes roughly as follows.

Let $ACL_p$ denote the theory of algebraically closed fields of characteristic $p$. $ACL_0$ is axiomatized by the axioms of an algebraically closed field and the axiom scheme $\psi_2, \psi_3, \psi_4,\ldots$, where $\psi_k$ is the statement "for all $x \neq 0$, $k x \neq 0$". Note that all $\psi_k$ are also proved by $ACL_p$, if $p$ does not divide $k$.

  1. The theorem is true in $ACL_p$, $p>0$. This can be easily shown by contradiction: assume a counter example, then take the finite field generated by the elements in the counter-example, call that finite field $F_0$. Since $F_0^n\subseteq F^n$ is finite, and the map is injective, it must be surjective as well.
  2. The theory of algebraically closed fields in characteristic $p$ is complete (i.e. the standard axioms prove or disprove all statements expressible in the first order language of rings).
  3. For each degree $d$ and dimension $n$, restrict Ax-Grothendieck to a statement $\phi_{d,n}$, which is expressible as a statement in the first order language of rings. Then $\phi_{d,n}$ is provable in $ACL_p$ for all characteristics $p > 0$.
  4. Assume the $\phi_{d,n}$ is false for $p=0$. Then by completeness, there is a proof $P$ of $\neg \phi_{d,n}$ in $ALC_0$. By the finiteness of proofs, there exists a finite subset of axioms for $ACL_0$ which are used in this proof. If none of the $\psi_k$ are used $P$, then $\neg \phi_{d,n}$ is true of all algebraically closed fields, which cannot be the case by (2). Let $k_0,\ldots, k_m$ be the collection of indices of $\psi_k$ used in $P$. Pick a prime $p_0$ which does not divide any of $k_0,\ldots,k_m$. Then all of the axioms used in $P$ are also true of $ACL_{p_0}$. Thus $ACL_{p_0}$ also proves $\neg \phi_{d,n}$, also contradicting (2). Contradiction. Therefore there is a proof of $\phi_{d,n}$ in $ACL_0$.

So the proof is actually along the lines of "for each degree $d$ and dimension $n$ there is a proof of the Ax-Grothendieck theorem restricted to that degree and dimension." What any of those proofs are, I have no clue.

  • $\begingroup$ Hi. Do you see how to extend the argument to prove that the inverse should also be polynomial? $\endgroup$ Jan 18, 2013 at 21:09
  • 1
    $\begingroup$ See also: terrytao.wordpress.com/2009/03/07/… $\endgroup$ Jan 18, 2013 at 21:10
  • 2
    $\begingroup$ Not off the top of my head. I'm guessing it goes something like this: Since every function on finite fields is a polynomial function, there should be an upper bound $U(n, d, p)$ on the degree of the inverse for every $n$. If that function can be made independent of $p$, then just use "$\phi_{d,n}$ AND there is a polynomial of degree at most $U(n,d)$ which is an inverse of $f$" instead of just $\phi_{d,n}$. The proof would go the same. I don't know how to make the upper bound on the degree independent of $p$, however. (Is it possible?) $\endgroup$ Jan 18, 2013 at 23:44
  • $\begingroup$ Rudin's proof seems more powerful than the model-theory proof above, and it elucidates better why the theorem is true. Still, this is a standard proof which directly addresses the original question. $\endgroup$ Jan 18, 2013 at 23:51
  • $\begingroup$ @RecursivelyIronic: I've always heard it the other way around, that the logical nature is the key reason for the theorem. Can you point out what exactly in Rudin's proof seems more fundamental than the facts used in this proof? $\endgroup$
    – user21820
    Feb 8, 2016 at 3:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .