Proof-theoretic semantics
 | This article includes a improve this article by introducing more precise citations. (June 2021) ) |
Proof-theoretic semantics is an approach to the
semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within a system of inference
.
Overview
cut-elimination for the sequent calculus, and some provocative philosophical remarks about locating the meaning of logical connectives in their introduction rules within natural deduction. The history of proof-theoretic semantics since then has been devoted to exploring the consequences of these ideas.[citation needed
]
Curry–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 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.
See also
References
- Proof-Theoretic Semantics, at the Stanford Encyclopedia of Philosophy
- Logical Consequence, Deductive-Theoretic Conceptions, at the Internet Encyclopedia of Philosophy.
- Thomas Piecha, Peter Schroeder-Heister (eds), "Advances in Proof-Theoretic Semantics", Trends in Logic 43, Springer, 2016.
External links
| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory |
| ||||||||
| Computability theory | |||||||||
| Related | |||||||||
 | This logic-related article is a stub. You can help Wikipedia by expanding it. |