Proof Theoretic Semantics

Lecture series at MGS2025 by David Pym http://www0.cs.ucl.ac.uk/staff/D.Pym/current.html

Connects with Philosophy of Language and with Natural Language Semantics.

Definition Logical realization of inferentialism: Inferentialism - metaphysical position that says that we want to interpret only in terms of how objects are used not their underlying semantics.

Group: https://sites.google.com/view/ptsnetwork/pts-seminar

Model Theoretic Semantics

• fails to introduce a truly meaningful semantics.

Truth

Categorical Truth - true without any assumptions

Logical Consequence

Tennant - enatilment and proofs. 1979 $⊢$ relies on valid argument. So what is a valid argument?

Prwitz Natural Deduction a proof-theoretical semantics 1971.

Girard Proofs and types

Gentzen proposed that introduction rules are the definition of the operator and elimination are just using them, others have suggested that it worked the other way around. they are actually interchangable.

Axiom

Meaning as Use

Wittgenstien, Brandom, Bou

operational semantics -

Consequence Proof-theoretic Validity

Canonical Proof --- check

${\varphi }_i{\models }_{⟨J,S⟩}\psi$ iff there is a proof that takes each ${\varphi }_i$ as arguments and conludes a $\psi$ - which is defined interm of existance proofs.

To deal with $\Rightarrow$ we can’t have a fixed base $S$, we need to look at every possible extension. However we can restrict the set S to only be those required by the justification ot simplify things.

Realizer takes us from premise to conclusion — need not be a real proof.

Transformational view of consequence for classical logic, the thransomission of truth between concepts through how you can change them from one form to the other.

Definitional reflection Disjunciton of implications — definitions (which is precisely a logic program) Sets up a system to show us the relation between different systems of implications. So eg. disjunction elim comes from the definitional rules of

Reductive Logic Tactical Proof Logic programming

Modal Logics Substructural Logics Resource Semantics Modelling

Shorthand:

Term	Abbreviation
Proof-Theoretic Validity	P-tV
Base-Extension Semantics	B-eS
Proof Theoretic Semantics	P-tS