Paul Hertz’s Systems of Propositions and The Origins of Proof Theory

Javier Legris

The mathematician and physicist Paul Hertz (1881-1940) wrote during the 1920s a series of papers on logic that influenced the development of proof theory and, particularly, Gentzen’s work. This paper aims to examine in detail Hertz’s logical theory placing it in the context of Hilbert’s metamathematical program and remarking its influence in Gentzens sequent calculus. Hertz‘s original interest was focused on the formal properties of axiom systems and his goal consisted in developing reduction methods for axiomatic systems from which some sort of minimal and independent system could be obtained. His research led him to the idea of Satzsystem (system of propositions), undoubtedly his main contribution to mathematical logic. With this kind of systems Hertz wanted to solve the problem of the deductive closure of formal theories, which was formulated in Hilberts program. In Hertzs sense, a proposition, related to a basic domain of elements, is an expression of the form

(1) a ⟶ b,

(2) a1, a2, ..., an ⟶ b.

Hertz proposed different interpretations to them, depending on the nature of the basic domain (events or predicates). He established a minimal set of rules for closed system of propositions, which are an antecedent of the structural rules in Gentzens sequent calculus. It must be stressed that Hertzs approach should be characterized as finitistic. He considered the case of an inference system (Schlusssystem) consisting in proofs for a system of proposition through these rules. In the paper Hertz‘s notions of closed system and normal proof are analyzed. Then, the way from Hertz’s propositions to Gentzen’s sequents is also traced and, finally, the idea of reducing logical constants to certain deduction rules is also taken into account and compared with the structural approach due to Gentzen.

Address: Universidad de Buenos Aires and Conicet (Argentina), Buenos Aires, Argentina

E-mail: jlegris@mail.retina.ar