# 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**

### Formal system

**logical systemdeductive systemsystem of logic**

### 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.

### Index of logic articles

Proof-theoretic semantics --

### Meaning (philosophy of language)

**meaningtheory of meaningmeanings**

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