Introduction to Proof-theoretic Semantics

ESSLLI 2025 · Taught with Tao Gu

A five-day introductory course on proof-theoretic semantics (P-tS): an inferentialist alternative to the model-theoretic tradition, on which the meaning of a logical expression is constituted by the rules governing its use in proof rather than by reference to truth conditions in a model. The course was designed for graduate students, young researchers, and other non-specialists with a working knowledge of logic, and does not presuppose prior exposure to P-tS.

Across five lectures, the course develops the subject from first principles: proof theory and the shift from denotational to inferential semantics; Prawitz's theory of proof-theoretic validity; Sandqvist's base-extension semantics for classical and intuitionistic logic, and its connections to resolution calculi and logic programming; base-extension semantics for classical logic set against Kripke's model-theoretic semantics, and its extension to modal logic; and its extension to substructural logics, illustrated through intuitionistic multiplicative linear logic and inferentialist resource semantics.

Lecture Slides

  • Lecture 1: General Proof Theory
    What logic is, natural deduction and proof theory, and the shift from denotationalism to inferentialism as a theory of meaning.
  • Lecture 2: Proof-theoretic Validity
    Prawitz's normalization theorem and the analysis of proof-theoretic validity, including Prawitz's Conjecture.
  • Lecture 3: Base-extension Semantics
    Sandqvist's base-extension semantics for classical and intuitionistic propositional logic, and its connections to resolution calculi and logic programming.
  • Lecture 4: Classical Logic & Kripke Semantics
    Base-extension semantics for classical logic set against Kripke's model-theoretic semantics, and its extension to modal and intuitionistic logic.
  • Lecture 5: Substructural Logic
    Base-extension semantics for substructural logics, with intuitionistic multiplicative linear logic as a case study, and its application to inferentialist resource semantics.