[FOM] CH and mathematics

[Timothy Y. Chow]

Vaughan Pratt wrote:

>Why not Goldbach's Conjecture (GC), or Twin Primes?  These are definite
>questions that may turn out not to be knowable at all.

While they may *turn out* to be unknowable, we we currently don't have as 
much evidence for their unknowability as the other proposed examples.

>While on this topic, does Peano Arithmetic admit any notion of forcing 
>analogous to that for ZFC?

Yes, it does.  As Ali Enayat reminded me recently, this is explained in 
"Computability and Logic" by Boolos-Jeffrey[-Burgess] among other places.

However, your other comments don't seem to have much to do with forcing 
per se; they would apply equally to any other technique for proving 
consistency results.

>Is there an argument showing that GC can't be forced false in PA without 
>settling GC?

What you mean to ask is if it is known how to infer either GC or ~GC from 
"PA doesn't prove GC."  It isn't; as you point out, PA could fail to prove 
GC either because GC is false, or because it's true but not provable in PA.

>If so then this would seem an easier goal than trying to decide GC.

Is your "easier goal" here the goal of proving that "GC is unprovable in 
PA"?  This doesn't seem to be any easier to me.  For starters, to prove 
such a thing, it has to be true, and the truth of "GC is unprovable in PA" 
seems rather doubtful---for GC to be false, or for GC to be true but 
unprovable in PA, would be quite startling, much more startling than a 
proof of GC itself.  Secondly, nobody has any idea how to prove that a 
"natural" statement like GC is unprovable, even in systems much weaker 
than PA.

Tim