most recent 30 from http://mathoverflow.net 2013-05-21T16:58:29Z http://mathoverflow.net/feeds/question/67271 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/67271/are-there-examples-of-nonconstructive-metaproofs David Diamondstone 2011-06-08T15:30:43Z 2011-06-08T16:37:24Z

<p>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?</p> <p>Conversely, is it possible to prove a meta-metatheorem saying that any metaproof can be used to find a proof?</p>

http://mathoverflow.net/questions/67271/are-there-examples-of-nonconstructive-metaproofs/67272#67272 David Harris 2011-06-08T15:48:21Z 2011-06-08T16:37:24Z

<p>If the proof system is recursively axiomatizable, this situation cannot occur.</p> <p>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.</p> <p>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 \} $$</p> <p>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</p>

http://mathoverflow.net/questions/67271/are-there-examples-of-nonconstructive-metaproofs/67273#67273 Emil Jeřábek 2011-06-08T15:58:47Z 2011-06-08T15:58:47Z

<p>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.</p> <p>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.</p>

http://mathoverflow.net/questions/67271/are-there-examples-of-nonconstructive-metaproofs/67279#67279 Noah 2011-06-08T16:19:09Z 2011-06-08T16:19:09Z

<p>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? </p>