This page is dedicated to my IVC Fellowship Project The Hilbertian Roots of Proof-Theoretic Semantics. The project (March 1st - August 30th 2024) was carried out at the Institut Wiener Kreis of the University of Vienna (some project-related publications and talks came after the end of the fellowship).
Proof-theoretic semantics, a constructive semantics generalising Prawitz's normalisation results for Natural Deduction, is often said to stem from Gentzen's general proof theory, as opposed to Hilbert's reductive proof theory. While Hilbert was interested in reducing derivability outcomes in certains systems to derivability outcomes in some ground systems, Gentzen wanted to study proofs in themselves, and thus to explore the structural properties which the epistemic power of deduction may come from.
It is certainly true that proof-theoretic semantics is in line with Gentzen's project of a general proof theory, as opposed to Hilbert's reductive one. But this does not exclude that other aspects of Hilbert's programme may have influenced proof-theoretic semantics (possibly via indirect influences on Gentzen himself). I aim at illuminating this sometimes overlooked Hilbertian influences by taking into account three features of proof-theoretic semantics. first, the role attributed by the latter to reduction procedures for eliminating arbitrary elimination inferences, in such a way that the reduction process be effective, or even decidable; second, the idea that the meaning of the (non-logica) terminology of one's language can be given axiomatically via atomic theories which constitute models that the validity of proof-structures can be locally evaluated over; and third, the tenet that valid proof-structures must reduce to primitive meaning-giving forms, in such a way as to eliminate non-primitive, meaning-given components.
* = invited
May 2025* PhilMatMed 2025 at the Aix-Marseille University. "Normalisation et sémantique des preuves. Vers une interpretation Hilbertienne de la proof-theoretic semantics"
February 2025* 5th Symposium on Proof-Theoretic Semantics at the Institute of Philosophy of the University of London. "From normalisation to proof-theoretic semantics: the semantic role of harmony, atomic bases and reductions".
January 2025* Logic in Bochum Colloquia at the Ruhr University of Bochum. "From normalisation to proof-theoretic semantics: the semantic role of harmony, atomic bases and reductions".
June 2024 Institute of the Vienna Circle Seminar at the University of Vienna. "Sundholm's semantics: logical atavism and the nature of proofs".
May 2024 Logik Café at the University of Wien. "Some issues in proof-theoretic semantics from a historical point of view".