Symposium on Proof-theoretic Semantics

Proof-theoretic semantics is an approach to meaning in which the central notion is proof rather than truth. Proof-theoretic semantics holds that the meaning of a logical constant is determined not by its truth conditions but by the rules that govern its use in inference. It belongs to the broader tradition of inferentialism, on which the meaning of an expression is constituted by its use, and in particular by the inferences in which it figures.

Its most specific source is Gentzen’s remark that the introduction rules of natural deduction act as definitions of the logical constants, while the elimination rules are consequences of those definitions. Prawitz made this precise with an inversion principle, and developed the notion of proof-theoretic validity: a closed argument is valid when it reduces to a canonical one, ending in an introduction rule, and an open argument is valid when every closed instance of it is. Dummett placed the programme within the theory of meaning and gave the name harmony to the required balance between introduction and elimination rules. The term “proof-theoretic semantics” itself was proposed by Schroeder-Heister, whose work on higher-level rules and definitional reflection extended the approach beyond the logical constants.

Current research ranges from base-extension semantics and other forms of sentence-based semantics, through questions of completeness such as Prawitz’s conjecture, to bilateralism and the treatment of denial, substructural and modal logics, categorial proof theory and the identity of proofs. There are applications in computer science, for instance to logic programming and to proof search. For a fuller survey, see the entry Proof-Theoretic Semantics in the Stanford Encyclopedia of Philosophy.

The series gathers researchers working on the foundations, ramifications, and open problems of this programme, in logic, philosophy, and computer science. It is meant for logicians, philosophers and computer scientists at every stage, from doctoral students to established researchers, and for colleagues in neighbouring fields who want to learn about the area. The programme is by invitation and attendance is free; to take part in the next meeting, email the organizers.

Six meetings have been held since 2022, in London, Prague, and Leuven, some of them alongside TABLEAUX and ESSLLI. The series is part of the Proof-theoretic Semantics Network.