For example, let's say that Goldbach's conjecture turns out to be unprovable. This would mean that a program cannot devise a way to check whether any counterexample exists. This seems to mean that there in fact is no counterexample - as we can develop a program that checks until some particular number, then if it stops, then write a program that starts from that number to some number and so on. This is all finite. If an even integer that cannot be represented by the sum of two primes is found, then the process would be finite.
This all seems for me to imply that a theorem is in fact true - but I am not sure if this is right reasoning.
My intention when I wrote "unprovable" was independent. That's my mistake.
OK. So, let's say Goldbach's conjecture is independent of PA, but we prove Goldbach's conjecture in a stronger (informally, more powerful) theory (I guess there are many...). This would mean (correct me if I am wrong here) that we select one model of PA, let's say standard one, and then prove that the conjecture is true in that model using a more powerful theory.
So as Asaf says, ZFC has no one standard model - so is that the reason why consistency of continuum hypothesis cannot be settled, while other theorems that relate to PA technically can be settled as true or not in particular model?
I know that continuum hypothesis can be settled in an extension of ZFC (as either true or false for a particular model of ZFC, and it would depend on different kinds of extension) - so a better rephrase of the edit above would be: can there be any statement of PA that cannot be proven true or false for a particular model of PA using a more powerful theory? And can anyone tell me more about