Antonio Piccolomini d'Aragona
March 01, until August 31, 2024
Affiliation: DISPOC, University of Siena, Siena, Italy
Research for a study about:
The Hilbertian roots of proof-theoretic semantics
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 certain 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-logical) 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.
Lecture
Some issues in proof-theoretic semantics from a historical point of view
Logik Café Lecture
Date: May 13, 2024
Time: 16h45 - 18h15
Meetings are usually held on Mondays from 16:45 to 18:15 in Raum 2H (D0224), 2. floor Department of Philosophy
Abstract:
Proof-theoretic semantics (PTS) is a constructive semantics first put forward by Dag Prawitz in some papers from the 1970s. Historically, it originates from a number of sources, including intuitionism, finitism/formalism, Dummett's anti-realist verificationism, and Gentzen's proof-theory. The latter source is especially relevant when PTS is conceived of as a sort of semantic generalisation of Prawitz's normalisation theory for Natural Deduction leading, via Prawitz's inversion principle, from Gentzen's idea that introductions define the meaning of the logical constants, to Dummett's fundamental assumption about provability by introduction. Prawitz understood PTS as a framework where what we evaluate is, not truth of formulas over given domains, but validity of arguments over given atomic theories. Such an evaluation is carried out by decorating generalised eliminations with constructive procedures for removing "arbitrary" detours, similar to standard reductions at play in normalisation proofs for specific logical calculi. A relation of (logical) consequence can be then extracted, by saying that A is a consequence of B (over an atomic theory) iff there is an argument D and a set of reductions J such that D is valid (over B) when decorated with the elements of J. In the current mainstream approach to PTS, however, we no longer have arguments and reductions, and all the constructivist burden is put on atomic theories, out of which (logical) consequence is defined outright. This strategy, whose origins can be traced back to works by Schroeder-Heister in the 2000s, has yielded many significant advancements, including many (in)completeness results for various logics relative to variants of PTS. In my talk I aim to reconstruct the reasons and the effects of the shift in PTS from Prawitz's original approach with arguments and reductions to contemporary approaches where the focus is on atomic bases only.