Impossible to prove vs neither true nor false
First off I am not a logician, so I probably won't use the correct terms. Sorry !
I have heard, like most mathematicians, about questions like the continuum hypothesis, or the independance of the axiom of choice from ZF. These statements (continuum hypothesis or axiom of choice) were referred to as "neither true nor false", because you could add them or their negation to form two different sets of axioms that would be equally self-consistent.
On the other hand, I have also heard about statements that "were true but could not be proven", i.e. could not be proven in a finite number of applications of axioms. For instance, it could be that the Goldbach conjecture is true, but that there is no other way to "prove" it than to verify it for all integers, which is not really a proof of course.
Is that distinction correct ? (and what is the real terminology?) I fail to understand what the problem would be, for example, if you were to add the negation of a "true but impossible to prove" statement as an axiom. There would be a contradiction, but you could never find it, so...
Solution 1:
First we need to assert the general framework. We have a language with relation symbols and function symbols and constants, etc. With this language we can write sentences and formulas.
We say that $T$ is a theory if it is a collection of sentences in a certain language, often we require that $T$ is consistent.
If $T$ is a first-order theory, whatever that means, then we can apply Goedel's completeness theorem and we know that $T$ is consistent if and only if it has a model, that is an interpretation of the language in such way that all the sentences in $T$ are true in a specific interpretation.
The same theorem also tells us that if we have some sentence $\varphi$ in the same language, then $T\cup\{\varphi\}$ is consistent if and only if it has a model. We go further to notice that if we can prove $\varphi$ from $T$ then $\varphi$ is true in every model of $T$.
On the other hand we know that if $T$ is consistent it cannot prove a contradiction. In particular if it proves $\varphi$ it cannot prove $\lnot\varphi$, and if both $T\cup\{\varphi\}$ and $T\cup\{\lnot\varphi\}$ are consistent then neither $\varphi$ nor $\lnot\varphi$ can be proved from $T$.
When we say that CH is unprovable from ZFC we mean that there exists a model of ZFC+CH and there exists a model of ZFC+$\lnot$CH [1]. Similarly AC with ZF, there are models of ZF+AC and models of ZF+$\lnot$AC.
Now we can consider a specific model of $T$. In such model there are things which are true, for example in a given model of ZF the axiom of choice is either true or false, and similarly the continuum hypothesis. Both these assertions are true (or false) in a given model, but cannot be proved from ZF itself.
Some theories, like Peano Axioms treated as the theory of the natural numbers, have a canonical model. It is possible that the Goldbach conjecture is true in the canonical model, and therefore we can regard it as true in some aspects, but the sentence itself is false in a different, non-canonical model. This would cause the Goldbach conjecture to become unprovable from PA, while still being true in the canonical model.
Footnotes:
- Of course this is all relative to the consistency of ZFC, namely we have to assume that ZFC is consistent to begin with, but if it is then both ZFC+CH and ZFC+$\lnot$CH are consistent as well.