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?
Best Answer
The usual way that we prove that each sentence $\phi$ is either true or false in a model $M$ is by induction on the structure of $\phi$. So we prove it first for the case where $\phi$ is an atomic formula, then we prove that the property is preserved when we build more complicated sentences with logical connectives and quantifiers.
However, if we say that a sentence is provably true we mean that there is some theory $T$ such that the sentence is provable in $T$. The theory is often part of the context of an argument. Usually, because of the incompleteness theorem, the theory $T$ will not be able to prove true every sentence that happens to hold in some arbitrary model of $T$. So for example, there are sentences of arithmetic (with quantifiers) that are true in the standard natural numbers, but are not provably true in Peano arithmetic. It is the case that every sentence in that language is either true or false in the standard model of arithmetic, but it is not the case that every sentence is provably true or provably false in Peano arithmetic.
There is a standard triviality that forces us to worry about the theory $T$. If we take a sentence $\phi$ that is true in some (at least one) model $M$, then there is a consistent theory in which $\phi$ is provably true: the theory consisting of all sentences that are true in $M$. Therefore, we see that the property of being "provably true" is really a relationship between a sentence and a theory, rather than an intrinsic property of a sentence itself.