## Are there examples of nonconstructive metaproofs?

### Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

This came up in a question on the xkcd forums. Is it possible to have a nonconstructive metaproof, i.e. a proof that there exists a proof in some formal system which does not construct said proof? Are there any known examples, preferably with some well-known formal system like PA?

Conversely, is it possible to prove a meta-metatheorem saying that any metaproof can be used to find a proof?

-

7
Sure. Metatheorem: any question I get on my homework has a proof. Metaproof: suppose otherwise. Then it would not be on my homework. – Qiaochu Yuan Jun 8 2011 at 16:01
Isn't there a story where a famous mathematician was assigned an open problem as homework by a devious professor, and ended up solving it? – David Diamondstone Jun 8 2011 at 16:03

5
@Qiaochu: you are very optimistic about the infallibility of your teacher. – Emil Jeřábek Jun 8 2011 at 16:03
Isn't there some question on how to show intuitionistically that Kripke models are complete for first-order intuitionistic (single-sorted) theories. Isn't the usual proof classical? – Andrej Bauer Jun 8 2011 at 16:34

1
Another example is completeness of Grothendieck toposes for higher-order intiotionistic logic. I think the proof is classical, and it's not clear how to make it intuitionistic. – Andrej Bauer Jun 8 2011 at 16:35
show 1 more comment

## 3 Answers

In theory, David’s answer is correct. Nevertheless, in practice it is perfectly possible to prove the existence of a proof non-constructively (such as by manipulating models and then appealing to the completeness theorem) where no one has a clue how to actually find the proof.

One example which springs to mind is Jacobson’s theorem: if $R$ is a ring such that for every $a\in R$ there exists an integer $n > 1$ such that $a=a^n$, then $R$ is commutative. By completeness of equational logic, this implies that for any $n > 1$, there exists an equational derivation of $xy=yx$ from the axioms of rings and $x^n=x$. Already finding such derivation for $n=3$ is a nontrivial exercise; explicit derivations are known for some $n$, but not in general.

-
Great answer. But I would still be interested in more examples, if anyone has some more. – David Diamondstone Jun 8 2011 at 19:19

2
Do you have your quantifiers in the right order in that statement? There are two closely related theorems of Jacobson that look like this and I'm not sure which one you mean. – Qiaochu Yuan Jun 8 2011 at 21:49
The quantifiers in the assumption of Jacobson’s theorem I have in mind are `$\forall a\in R\,\exists n > 1\,a^n=a$`. However, in order to express this in equational logic, the exponent has to be fixed, hence we only consider the corollary of the theorem with the stronger assumption `$\exists n\,\forall a\,a^n=a$` (more precisely, for each particular constant $n$, we consider the theorem with assumption `$\forall a\,a^n=a$`). – Emil Jeřábek Jun 9 2011 at 10:21

### You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.

If the proof system is recursively axiomatizable, this situation cannot occur.

If there exists a proof of $\Theta$, there exists an algorithm to find that proof. Namely, search the recursively enumerable set of deductions until you find a proof of $\Theta$. This must terminate, as we have proved that $\Theta$ is provable.

If the proof system is NOT recursive, then this may be possible. Consider the following set of axioms $\Sigma$ in the signature of arithmetic. Let $A$ be an infinite set which does not contain any infinite r.e. set. Define $$\Sigma = \{ (\bar k = \bar k) \wedge \sigma \mid k \in A, k > \ulcorner \sigma \urcorner, \mathfrak N \models \sigma \}$$

Now, note that any sentence provable in $Th(\cal N)$ is provable is in $\Sigma$. However, there is no algorithm to transform produce such proofs from $\Sigma$. To do so would require enumerating arbitrarily large elements of $A$, which is impossible

-
This can hardly be seen as a constructive proof, as the "constructive" part is entirely divorced from the "proof" part. – David Diamondstone Jun 8 2011 at 16:05
You are implicitly using Markov principle, I think. – Andrej Bauer Jun 8 2011 at 16:33
I don't know that this addresses the spirit of the question. This algorithm guarantees that it can find a proof but it does not guarantee that this will happen before I die or that the proof can be made short enough for me to finish reading it before I die, yet it is still possible that I can prove by other means that a proof exists in perhaps 10 minutes. – Qiaochu Yuan Jun 8 2011 at 16:47

1
There's a stronger form of this assertion. If the proof system is recursive, the statement "T proves $\phi$" is itself a $\Sigma_1$ statement, so if the non-constructive proof itself takes place in a "reasonable" system, it is possible to extract an explicit witness, which would be a direct proof. – Henry Towsner Jun 8 2011 at 17:58

What about examples from nonstandard analysis? By the transfer principle, given a proof of $\phi$ in nonstandard analysis, we know there exists a proof of $\phi$ using only standard techniques; but there is in general no nice way to extract the standard proof from the nonstandard proof, and if I recall correctly there are theorems which have a known nonstandard proof with no known standard proof. Would this count as a non-constructive metaproof?

-

1
One can go from nonstandard proof to standard proof using ultrapowers. It is just that such a proof may not be as "elegant". – Gerald Edgar Jun 8 2011 at 16:28
If we're talking about proofs in formal systems of nonstandard analysis, there are general methods for extracting the standard proof from it. For instance, "Weak theories of nonstandard arithmetic and analysis" by Jeremy Avigad. – Henry Towsner Jun 8 2011 at 17:55
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 24, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.938130259513855, "perplexity_flag": "head"}