                                              Notes prepared by
                                                 Stanley Burris
                                                   July 3, 2001

A finitistic point of view: Herbrand

Jacques Herbrand (1908–1931)

1930 - Research on the Theory of Demonstration.

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 k^{th} 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.]