View source for Proof-theoretic semantics

{{Short description|Approach to the semantics of logic}}
{{No footnotes|date=June 2021}}
'''Proof-theoretic semantics''' is a branch of [[proof theory]] and an approach to the [[Formal semantics (logic)|semantics of logic]] that attempts to locate the meaning of [[proposition]]s and [[logical connective]]s not in terms of [[Interpretation (logic)|interpretation]]s, as in [[Alfred Tarski|Tarski]]an approaches to semantics, but in the role that the proposition or logical connective plays within a [[Formal system|system of inference]].

==Overview==

[[Gerhard Gentzen]] is the founder of proof-theoretic semantics, providing the formal basis for it in his account of [[cut-elimination]] for the [[sequent calculus]], and some provocative philosophical remarks about locating the meaning of logical connectives in their [[Natural_deduction#Introduction_and_elimination|introduction rule]]s within [[natural deduction]]. The history of proof-theoretic semantics since then has been devoted to exploring the consequences of these ideas.{{Citation needed|date=December 2014}}

[[Dag Prawitz]] extended Gentzen's notion of [[analytic proof]] to [[natural deduction]], and suggested that the value of a proof in natural deduction may be understood as its normal form.{{Citation needed|date=March 2019}}  This idea lies at the basis of the [[Curry&ndash;Howard isomorphism]], and of [[intuitionistic type theory]].  His [[inversion principle]] lies at the heart of most modern accounts of proof-theoretic semantics.

[[Michael Dummett]] introduced the very fundamental idea of [[logical harmony]], building on a suggestion of [[Nuel Belnap]].  In brief, a [[formal language|language]], which is understood to be associated with certain patterns of inference, has logical harmony if it is always possible to recover analytic proofs from arbitrary demonstrations, as can be shown for the sequent calculus by means of cut-elimination theorems and for natural deduction by means of normalisation theorems.  A language that lacks logical harmony will suffer from the existence of incoherent forms of inference: it will likely be inconsistent.

The term "proof-theoretic semantics" was coined by Peter Schroeder-Heister, who first mentioned it in a lecture in 1985, and in print in 1991.<ref>{{Citation |last=Schroeder-Heister |first=Peter |title=Proof-Theoretic Semantics: An Autobiographical Survey |date=2024 |work=Peter Schroeder-Heister on Proof-Theoretic Semantics |pages=1–51 |editor-last=Piecha |editor-first=Thomas |url=https://doi.org/10.1007/978-3-031-50981-0_1 |access-date=2025-09-10 |place=Cham |publisher=Springer Nature Switzerland |language=en |doi=10.1007/978-3-031-50981-0_1 |isbn=978-3-031-50981-0 |editor2-last=Wehmeier |editor2-first=Kai F.|doi-access=free }}</ref><ref>{{Citation |last=Schroeder-Heister |first=Peter |title=Proof-Theoretic Semantics |date=2024 |work=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/sum2024/entries/proof-theoretic-semantics/ |access-date=2025-09-10 |edition=Summer 2024 |publisher=Metaphysics Research Lab, Stanford University |editor2-last=Nodelman |editor2-first=Uri}}</ref>

==See also==

* [[Inferential role semantics]]
* [[Truth-conditional semantics]]

==References==
{{reflist}}

==Further reading==
* [http://plato.stanford.edu/entries/proof-theoretic-semantics/ Proof-Theoretic Semantics], at the [[Stanford Encyclopedia of Philosophy]]
* [http://www.iep.utm.edu/l/logcon-d.htm Logical Consequence, Deductive-Theoretic Conceptions], at the [[Internet Encyclopedia of Philosophy]].
* [[Nissim Francez]], "On a Distinction of Two Facets of Meaning and its Role in Proof-theoretic Semantics", ''[[Logica Universalis]]'' 9, 2015. {{doi|10.1007/s11787-015-0118-8}}
* Thomas Piecha, Peter Schroeder-Heister (eds), [https://link.springer.com/book/10.1007%2F978-3-319-22686-6 "Advances in Proof-Theoretic Semantics"], Trends in Logic 43, Springer, 2016.

==External links==

*[https://web.archive.org/web/20090415110223/http://arche-wiki.st-and.ac.uk/~ahwiki/bin/view/Arche/ProofTheoreticSemantics Arché Bibliography on Proof-Theoretic Semantics.]
*[https://sites.google.com/view/ptsnetwork Proof-Theoretic Semantics Network]

[[Category:Mathematical logic]]
[[Category:Philosophical logic]]
[[Category:Proof theory]]
[[Category:Semantics]]