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.
Lecture
Sundholm's Semantics: Logical Atavism and the Nature of Proofs
Philosophy of Science Colloquium TALK
Date: 20/06/2024
Time: 16h45
Venue: New Institute Building (NIG), Universitätsstraße 7, 1010 Wien, HS 3F
Abstract:
I aim at providing an overview of some of Sundholm's observations on the philosophy and history of logic, which I overall refer to as Sundholm's semantics. In the reconstruction I propose, the latter is based on two main tenets, namely, that we had better jettison the object-language/meta-language distinction, and that the careful meaning-explanation which formalisms must come with render the axioms and rules of inference evident. The first tenet goes hand in hand with the detection of what Sundholm call the Bolzano reductions, namely, two methodological tenets according to which, first, correctness of assertions is reduced to propositional truth and, second, inferential validity is reduced to logical consequence. In Sundholm's opinion, these Bolzano reductions hide crucial epistemic and pragmatic aspects of logic, when compared to what is the case in "atavistic" approaches like Frege's, where formalisms are indeed understood as meaningful languages. Thus, Sundholm's semantics does not consist in a meta-linguistic attribution of meaning to uninterpreted sets of strings, but in an issuing of the intended meaning of contentual formalism, including semantic values for derivations. The latter are dealt with by Sundholm through a distinction between proof-objects and proof-acts, which Sundholm himself had put stressed in the context of his early discussion of BHK-semantics. When cast as a constructive reading of the so-called truth-maker principle, via a Martin-Löfian rendering of assertions as existence of proof(-object)s for given propositions, the proof-object/proof-act distinction leads to a fresh semantic account of Gentzen's 1932 and 1936 versions of Natural Deduction, as well as to doubts regarding their often asserted meta-theoretical equivalence.