Proof-theoretic semantics

Proof-theoretic
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 the system of inference.wikipedia
28 Related Articles

Semantics of logic

formal semanticssemanticslogical semantics
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 the system of inference.
Proof-theoretic semantics associates the meaning of propositions with the roles that they can play in inferences. Gerhard Gentzen, Dag Prawitz and Michael Dummett are generally seen as the founders of this approach; it is heavily influenced by Ludwig Wittgenstein's later philosophy, especially his aphorism "meaning is use".

Gerhard Gentzen

GentzenDr Gerhard GentzenGentzen, Gerhard
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 introduction rules within natural deduction.
His cut-elimination theorem is the cornerstone of proof-theoretic semantics, and some philosophical remarks in his "Investigations into Logical Deduction", together with Ludwig Wittgenstein's later work, constitute the starting point for inferential role semantics.

Cut-elimination theorem

cut eliminationcut-eliminationcut-free
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 introduction rules within natural deduction.
Normally also the system has, at least in first order logic, the subformula property, an important property in several approaches to proof-theoretic semantics.

Analytic proof

analytic calculi
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.
* Proof-theoretic semantics

Inferential role semantics

inferentialismconceptual role semanticssemantic inferentialism
Inferential role semantics
The approach is related to accounts of proof-theoretic semantics in the semantics of logic which associate meaning with the reasoning process.

Truth-conditional semantics

truthtruth conditioningtruth-conditional theory of meaning
Truth-conditional semantics
Dummett further argues that a theory based on inference, such as Proof-theoretic semantics, provides a better foundation for this model than truth-conditional semantics does.

Logical connective

logical operatorconnectivesconnective
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 the system of inference.

Interpretation (logic)

interpretationinterpretationsinterpreted
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 the system of inference.

Alfred Tarski

TarskiTarski, AlfredTarskian
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 the system of inference.

Formal system

logical systemdeductive systemsystem of logic
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 the system of inference.

Sequent calculus

sequent calculiLJLK
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 introduction rules within natural deduction.

Natural deduction

Deductionelimination ruleintroduction rule
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 introduction rules within natural deduction. 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.

Dag Prawitz

PrawitzPrawitz, Dag
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.

Intuitionistic type theory

constructive type theoryintensional type theoryidentity type
This idea lies at the basis of the Curry–Howard isomorphism, and of intuitionistic type theory.

Michael Dummett

DummettDummett, MichaelSir Michael Dummett
Michael Dummett introduced the very fundamental idea of logical harmony, building on a suggestion of Nuel Belnap.

Logical harmony

harmonyTonk
Michael Dummett introduced the very fundamental idea of logical harmony, building on a suggestion of Nuel Belnap.

Nuel Belnap

BelnapBelnap, NuelBelnap, N.
Michael Dummett introduced the very fundamental idea of logical harmony, building on a suggestion of Nuel Belnap.

Stanford Encyclopedia of Philosophy

The Stanford Encyclopedia of PhilosophySEPStanford Encyclopedia
Proof-Theoretic Semantics, at the Stanford Encyclopedia of Philosophy

Internet Encyclopedia of Philosophy

IEPThe Internet Encyclopedia Of Philosophy
Logical Consequence, Deductive-Theoretic Conceptions, at the Internet Encyclopedia of Philosophy.

Logica Universalis

Nissim Francez, "On a Distinction of Two Facets of Meaning and its Role in Proof-theoretic Semantics", Logica Universalis 9, 2015.

Logic

logicianlogicallogics
Modern semantics also admits rival approaches, such as the proof-theoretic semantics that associates the meaning of propositions with the roles that they can play in inferences, an approach that ultimately derives from the work of Gerhard Gentzen on structural proof theory and is heavily influenced by Ludwig Wittgenstein's later philosophy, especially his aphorism "meaning is use".

Per Martin-Löf

Martin-LöfMartin-Löf, Per
However, this system turned out to be inconsistent due to Girard's paradox which was discovered by Girard when studying System U, an inconsistent extension of System F. This experience led Per Martin-Löf to develop the philosophical foundations of type theory, his meaning explanation, a form of proof-theoretic semantics, which justifies predicative type theory as presented in his 1984 Bibliopolis book, and extended in a number of increasingly philosophical texts, such as his influential On the Meanings of the Logical Constants and the Justifications of the Logical Laws.

Principle of explosion

ex falso quodlibetexplosionabsurdity constant
Proof-theoretic paraconsistent logics usually deny the validity of one of the steps necessary for deriving an explosion, typically including disjunctive syllogism, disjunction introduction, and reductio ad absurdum.

Meaning (philosophy of language)

meaningtheory of meaningmeanings
He leverages work done in proof-theoretic semantics to provide a kind of inferential role semantics, where: