In logic, it is said that each sentence in a (consistent) theory is either true or false in a given model. Checking the truth of a sentence in a finite model amounts essentially to finite enumeration so there's no problem. But how can we know, as seems to be taken for granted, that this dichotomy (i.e., that exactly one of the sentences $\phi$ and $\neg\phi$ is true) also always holds true a priori, when we move to infinite models?
Since the dichotomy says its either true or false, I'm curious whether we can say that a sentence in a model must be provably true or false in principle, even if we cannot (yet) prove it (Think of the Goldbach conjecture in the standard number theory model), or could there be sentences for which no such proof can be found/constructed? (Proof here is to be understood in the broad sense, and need not be a formal one within the theory.)
Edit with regard to @Carl Mummert 's answer: Please note the final sentence (boldface). Maybe I was taking the concept of a proof a little beyond its usual meaning in logic. When you say proof you meant a formal proof in a theory T. But say, the Godel sentence, although its truth in the standard model is unprovable in PA, Godel still determined (proved), in effect, its truth for the standard model, didn't he? For that matter, we can say the truth of a sentence $\phi$ in model $M$ is an intrinsic property. The problem with $Th(M)$ is, of course, that it may not be a decidable theory, in the sense that one cannot hope to find a formal system allowing a systematic way to determine true/false of every $\phi$ in $M$. But this by no means has any bearing on whether true/false of any given $\phi$ in $M$ can still be determined. Can we always, in principle, determine true/false of any given $\phi$ in $M$, or there could be some sentences whose true/false can in no way be known?
