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?
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.
$\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$).
$\endgroup$
Commented
Jun 9, 2011 at 10:21
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
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?
