A finitistic point of view: Herbrand

Herbrand said that his goal was to make the work of Löwenheim and Skolem rigorous [from the finitistic point of view]. In essence he introduced a proof system so that one had a notion of derivation (essentially that of Hilbert and Ackermann), and he described the countermodel procedure, in his own language, and showed that a first-order statement was derivable iff the attempt to build a countermodel failed at some finite stage. Furthermore there was an effective procedure to go from the knowledge that the countermodel failed at the stage to a derivation of the statement. Thus we see that Herbrand has come up with a version of the Löwenheim-Skolem theorem that does not mention infinite models.

References

1

J. Herbrand, Recherches sur la théorie de la demonstration. Thesis, 1930, Paris. [transl. in From Frege to Gödel, van Heijenoort, Harvard Univ. Press, 1971.]