Richard Zach – The Decision Problem and the Development of Metalogic
The Montreal Inter-University Workshop on the History and Philosophyof Mathematics presents:
The Decision Problem and the Development of Metalogic
Richard Zach (University of Calgary, Department of Philosophy)
In parallel with their work on proof theory in the 1920s and early
1930s, Hilbert and his collaborators and students—in particular, Ackermann, Behmann, Bernays, and Schönfinkel—did substantial work towards a positive solution for the decision problem. This begins with an unpublished talk by Behmann in 1921 in which the term "Entscheidungsproblem" first appears, and continues until the early 1930s with a number of published as well as unpublished contributions.
Approaches to the decision problem evolved significantly during this time, from a purely algebraic approach in the style of Schröderian algebra of logic to relatively modern proofs which establish the finite controllability of certain prefix classes of formulas. This evolution goes hand-in-hand with an evolution of attendant concepts, in particular, semantic concepts such as satisfiability. An analysis of this work sheds light on the development of the semantics of first-order logic in the 1920s, on changing views as to what constitutes a "decision procedure," and on the connection between the decision problem and the consistency problem.
For more information, please contact:
Gregory Lavers (Concordia), Mathieu Marion (UQÀM),
Jean-Pierre Marquis (UdM), Dirk Schlimm (McGill).