<https://meet.google.com/ykg-hdam-xso>.

The name proof-theoretic semantics (shortly PTS) indicates a family of constructive approaches to meaning and to such core notions as (logical) validity and consequence stemming from Prawitz’s results in proof-theory for Gentzen’s Natural Deduction. In particular, Prawitz’s normalisation theorems imply a number of corollaries which seem to confirm Gentzen’s semantic claim that introductions determine the meaning of the logical constants. Prawitz’s normalisation theory can be hence generalised towards a full-blooded semantics based on Dummett’s fundamental assumption (if A is a theorem, then A is provable by introduction) via a concept of argumental validity inspired by the BHK-notion of proof. In later developments, valid arguments have been dropped out, and PTS has become a pure theory of consequence whose constructivist burden is pulled down to base-structures. The latter, in very much the same way as models in model-theory, determine the meaning of the non-logical dictionary, and thereby provide semantic evaluation with a “local” ground. However, unlike models in model-theory, base-structures in PTS are not sets equipped with relations and functions, but sets of axioms and rules governing deduction at the atomic level. Recent investigations into proof-theoretic completeness and incompleteness of various logics have shown sensibility to such features of atomic systems as dischargement of rules of lower complexity, or order-relations over the full systems-set. In my talk, I aim to provide a survey of the philosophical reasons, the historical development, and the technical achievements of PTS.