Hilbert's plan for understanding the concept of infinity required the elimination of non‐finitist machinery from proofs of finitist assertions. The failure of the original plan leads to a hierarchy of progressively less elementary, but still constructive methods instead of finitist ones . A mathematical proof of this failure requires a definition of « finitist ».—The paper sketches the three principal methods for the syntactic analysis of non‐constructive mathematics, the resulting consistency proofs and constructive interpretations, modelled on Herbrand's theorem, and their (...) mathematical and logical consequences. A characterization of finitist proofs is sketched. A remark on the completeness of the predicate calculus concludes the paper. Throughout open problems and alternative approaches are emphasized.ZusammenfassungHilbert sah das Verstehen des Begriffs des Unendlichen in der Eliminierung nichtfiniter Methoden aus Beweisen finiter Sätze. Das Versagen dieses Unternehmens führt zu einer Hierarchic progressiv weniger elementarer, aber noch konstruktiver Methoden, statt der finiten . Ein Unmöglichkeitsbeweis des ursprünglichen Planes setzt eine Definition von « finit » voraus.—Die drei wichtigsten Methoden der syntaktischen Analyse nichtkonstruktiver mathematischer Theorien, die daraus gewonnenen Widerspruchsfreiheitsbeweise and konstruktiven Interpretationen and deren mathematische and logische Anwendungen werden besprochen. Eine Prazisierung des Begriffs « finit » wird skizziert. Eine Bemerkung zur Vollstandigkeit des engeren Funktionenkalküls beschliesst die Abhandlung.—Oflene Fragen and komplementare Fragestellungen werden betont. (shrink)

We consider a seemingly popular justification (we call it the Re-flexivity Defense) for the third derivability condition of the Hilbert-Bernays-Löb generalization of Godel's Second Incompleteness Theorem (G2). We argue that (i) in certain settings (rouglily, those where the representing theory of an arithmetization is allowed to be a proper subtheory of the represented theory), use of the Reflexivity Defense to justify the tliird condition induces a fourth condition, and that (ii) the justification of this fourth condition faces serious obstacles. We (...) conclude that, in the types of settings mentioned, the Reflexivity Defense does not justify the usual ‘reading’ of G2—namely, that the consistency of the represented theory is not provable in the representing theory. (shrink)