I don't understand this stuff. I admit is frankly. This is not a solution, nor marked as such (those tricky symbols, Mr. Brantley...) But this is interesting reading for those smart enough to potentially solve this one.

 

Kurt Godel was a tremendous physical specimen, with the muscles and endurance of an Olympic athlete. He got that way by spending his entire life running furiously to catch up with the Greeks.

 

 

 

Godel's work really goes all the way back to Greek geometry. Euclid showed that in geometry a few statements, called axioms, could be made at the start and a vast system of sophisticated proofs derived from them. Axioms are ideas which are too obvious to be proven. They just seem as if they must be true. An example is the idea that you can add one to any number and get a bigger number. When a system needs as many axioms as number theory does, doubts begin to arise. How do we know that the axioms aren't contradictory? ....

(a)  Goldbach's Conjecture is of the form  Ax Q(x), where any individual Q(k) is easily computable (decidable): given an even number, there are only finitely many possible sums  p+q  to try out.   (Incidentally, Goedel's [sic]  G  and statements  "S is consistent"  are of this form too).

b)  If  Ax Q(x) is false (in N), then it is decidable... by a pretty simple theory too, a weak fragment of Peano Arithmetic.  That is because if Ex ~Q(x) holds then ~Q(k) holds for some k; so one tries out one k after another, in sequence, and in finitely many steps one finds the appropriate k and establishes  ~Q(k).

c)  Any proof of  "X is undecidable in theory S"  is in particular a proof that  S  is consistent.  That is because an inconsistent theory proves every statement; if there is one thing S doesn't prove, S is consistent.

So suppose that working in mathematics (as formalized by ZF, say) one proves that G.C. is undecidable from PA.  (Unlikely... but conceivable). By (c), that proof shows PA is consistent.  No big deal; PA _is_ consistent, as it has a model, N.  But by (b), the proof also shows that G.C. is true! Nothing paradoxical here; this just explains why people are not trying to show G.C. undecidable from PA: they know (or ought to know!) that this implies
a proof of G.C. outright.  If they cannot do the latter, it's no use attempting the former.

How about working in PA and trying to prove G.C. undecidable from PA? That's a fool's errand: it would be a proof, in PA, that PA is consistent; by Goedel [sic], this would only be possible if PA were inconsistent.

What about working in ZF and trying to prove G.C. undecidable from ZF... which is, I believe, what you are envisioning above?  First of all, it cannot be done unless ZF is inconsistent, since it amounts to a proof in ZF that ZF is consistent.  Well, let us say you do believe ZF (mathematics!) is consistent, and you are willing to add Consis(ZF) to your hypotheses (ZF).
It is still the case that proving G.C. undecidable from ZF would imply G.C. itself, by (b).  It would be implicit in the proof, if you like.

So again... unless if you can prove G.C. in ZF + Consis(ZF), don't
bother with stronger statements like G.C. being undecidable in PA, or in ZF!

Footnote, to avoid mix-ups:  there is no "undecidable"...  there is
only "undecidable in S".