Some issues in proof-theoretic semantics from a historical point of view

Im Logik-Café werden Themen aus den Bereichen Philosophische Logik und Formale Epistemologie behandelt. Die Treffen sind informell, alle Interessierten sind jederzeit herzlich eingeladen.

Finden Sie hier alle Talks unserer IVC Fellows beim Logik Café. Eine vollständige Liste aller weiteren Vorträge ist auf der Website des Logik Cafés zu finden.

Date: 13/05/2024

Time: 16h45

Venue: New Institute Building (NIG), Universitätsstraße 7, 1010 Wien, HS 2H

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.