If the atomic sentences of S have a finitistic meaning, which is the case, for instance, when they are decidable, then so have all sentences of S built up by truth-functional connectives and quantifiers restricted to finite domains.
Quantifiers over infinite domains can be looked upon in two ways. One of them may be hinted at as follows. Let x range over the natural numbers, and let A(x) be a formula such that A(n) expresses a finitary proposition for every number n. Then a sentence ∀xA(x) expresses a transfinite proposition, if it is understood as a kind of infinite conjunction which is true when all of the infinitely many sentences A(n), where n is a natural number, hold.
Similarly, a sentence ∃xA(x) expresses a transfinite proposition, if it is understood as a kind of infinite disjunction which is true when, of all the infinitely many sentences A(n), where n is a natural number, there is one that holds. There is a certain ambiguity here, however, depending on what is meant by ‘all’ and ‘there is one’. To indicate the transfinite interpretation one should also add that the sentences are understood in such a way that it is determined, regardless of whether this can be proved or not, whether all of the sentences A(n) hold or there is some one that does not hold.
If instead an assertion of ∀xA(x) is understood as asserting that there is a method which, given a specific natural number n, yields a proof of A(n), then we have to do with a finitary proposition. Similarly, we have a case of a finitary proposition, when to assert ∃xA(x) is the same as to assert that A(n) can be proved for some natural number n.
It is to be noted that the ‘statement’ “In the real part of mathematics, either in the real part of S or in some extension of it, that for each A ∈ R, if ⌈S A, then A is true” is a universal sentence. Hence, the possibility of giving a finitary interpretation of the universal quantifier is a prerequisite for Hilbert’s program. Does the possibility of interpreting the quantifiers in a finitary way also mean that one may hope for a solution of the problem stated in the above ‘statement’ when all quantified sentences interpreted in that way are included in R?
A little reflection shows that the answer is no, but that R may always be taken as closed under universal quantification. For it can be seen (uniformly in A) that if we have established the ‘statement’ when R contains all instances of a sentence ∀xA(x), then the ‘statement’ also holds for R+ = R U {∀xA(x)}. To see this let ∀xA(x) be a formula provable in S whose instances belong to R, and let a method be given which applied to any formula in R and a proof of it in S yields a proof of its truth. We want to show that ∀xA(x) is true when interpreted in a finitistic way, i.e. that we have a method which applied to any natural number n yields a proof of A(n). The existence of such a method is obvious, because, from the proof given of ∀xA(x), we get a proof of A(n), for any n, and hence by specialization of the given method, we have a method which yields the required proof of the truth of A(n), for any n.
Having included universal sentences ∀xA(x) in R such that all A(n) are decidable, it is easy to see that one cannot in general also let existentially quantified sentences be included in R, if the ‘statement’ is still to be possible. For let S contain classical logic and assume that R contains undecidable sentences ∀xA(x) with A(n) decidable; by Gödel’s theorem there are such sentences if S is sufficiently rich. Then one cannot allow R to be closed under existential quantification. In particular, one cannot allow formulas ∃y(∀xA(x) V ¬ A(y)) to belong to R ∀ A: the formulas are provable in S but all of them cannot be expected to be true when interpreted in a finitistic way, because then, for any A, we would get a proof of ∀xA(x) V ¬ A(n) for some n, which would let us decide ∀xA(x).
In accordance with these observations, the line between real and ideal propositions was drawn in Hilbert’s program in such a way as to include among the real ones decidable propositions and universal generalizations of them but nothing more; in other words, the set R in the ‘statement’ is to consist of atomic sentences (assuming that they are decidable), sentences obtained from them by using truth-functional connectives, and finally universal generalizations of such sentences.
Given that R is determined in this way and that the atomic sentences in the language of S are decidable and provable in S if true (and hence that the same holds for truth-functional compounds of atomic sentences in S), which is normally the case, the consistency of S is easily seen to imply the statement in the ‘statement’ as follows. Assume consistency and let A be a sentence without quantifiers that is provable in S. Then A must be true, because, if it were not, then ¬ A would be true and hence provable in S by the assumption made about S, contradicting the consistency. Furthermore, a sentence ∀xA(x) provable in S must also be true, because there is a method such that for any given natural number n, the method yields a proof of A(n). By applying the decision method to A(n); by the consistency and the assumption on S, it must yield a proof of A(n) and not of ¬A(n).
AltExploit 