# Use of undecidability

Suppose someone proved that the Goldbach conjecture was undecidable in an axiomatic system that is consistent as far as we know. Then in some sense we know that Goldbach conjecture must be "true", because if we could find a counter-example, then we could prove it false, and it wouldn't be undecidable.

How widely accepted is this kind of "proof"? I don't have very much experience, but outside of set theory and logic, I have rarely seen anybody specify in what axiomatic system they are working in.

For instance, would such a proof be accepted in

• The Putnam exam?
• Science?
• Engineering?
• General Mathematics (e.g. the Monthly)?
-
Outside of set theory and logic, unless otherwise stated, it is usually understood that people work with ZF, possibly with choice. So nobody bothers to specify this explicitly. –  Srivatsan Jan 31 '12 at 22:05
"Engineering"? I am not aware of engineers being concerned about proofs of formal mathematical statements at all, let alone one whether a given argument is an acceptable proof or not... –  Arturo Magidin Jan 31 '12 at 22:05
@math4tots: If you could prove that Goldbach's conjecture is independent of PA in ZFC, then that would in fact be a proof that Goldbach's conjecture is true in ZFC. Since most mathematicians don't work in pure PA (where would the "true" real numbers be, for a start?), this would certainly be considered a valid proof. For more discussion on the specific case of Goldbach, see this MO question. –  Zhen Lin Jan 31 '12 at 22:24
Consistent "as far as we know"? If you could prove that Goldbach (or any other statement that can be expressed in the system) is unprovable in a given system, that would prove that the system is consistent, because from a contradiction you can prove anything. –  Robert Israel Jan 31 '12 at 22:44
Note that the hypothesized proof would be essentially isomorphic to the usual argument that Gödel's undecidable sentence is in fact true for the standard integers -- and nobody seem to take issue with that conclusion in particular. –  Henning Makholm Feb 1 '12 at 2:02

We do not know it in some sense, but taking Platonic stance we actually know it for sure. Assume that there exists a totality of standard natural numbers, say $\mathfrak{N}$. Suppose $\varphi$ is the Goldbach conjecture, which is $\Pi_1$ sentence (begins with a universal unbounded quantifier followed be a formula expressing recursive property or realtion). Finally suppose that you managed to show that neither $PA\vdash\varphi$ nor $PA\vdash\neg\varphi$ (where $PA$ is first-order Peano arithmetic).
However, as a Platonist I believe that either $\varphi$ is true about $\mathfrak{N}$ or it is false about it. Assume it is false, which entails that its negation must be true. But $\neg\varphi$ is equivalent to a $\Sigma_1$ formula (truly) asserting existence of a natural number which is not a sum of two primes: $\exists_x\psi(x)$. Take this (standard) number, say $n$, and substitute $\overline{n}$ for $x$ to obtain $\psi(\overline{n})$ which asserts a recursive property of $n$. From representability of recursive properties you obtain that $PA\vdash\psi(\overline{n})$, so $PA\vdash\exists_x\psi(x)$, so $PA\vdash\neg\varphi$, contrary to the fact that $\varphi$ is undecidable. (The mehtod described applies to all $\Pi_1$ sentences and uses so called $\Sigma_1$ completeness of $PA$)
Of course the hard part is proving undecidability of $\varphi$, and as it was said by Robert Israel in the comments above, this would probably be a longer way than challenging Goldbach conjecture directly. Moreover being Platonist is not enough as well, since you must engage some (stronger than $PA$) theory in which you can carry a proof of independence of $\varphi$.
Thus reception of a proof of this kind would probably rely on nature of methods applied in showing undecidability of the conjecture. Last but not least, constructivists could attack the assumption about definite truth value of the conjecture or (maybe even more likely) the part in which one infers existence of $n$ from a premiss saying: not every natural number... .