In proof theory, the Gödel–Gentzen negative translation is a method for embedding classical first-order logic into intuitionistic first-order logic. It is one of a number of double-negation translations that are of importance to the metatheory of intuitionistic logic. It is named after logicians Kurt Gödel and Gerhard Gentzen.
| Property | Value |
|---|
| dbpprop:abstract
|
- In proof theory, the Gödel–Gentzen negative translation is a method for embedding classical first-order logic into intuitionistic first-order logic. It is one of a number of double-negation translations that are of importance to the metatheory of intuitionistic logic. It is named after logicians Kurt Gödel and Gerhard Gentzen.
|
| dbpprop:date
| |
| dbpprop:discuss
|
- Talk:Gödel–Gentzen negative translation
|
| dbpprop:reference
| |
| dbpprop:wikiPageUsesTemplate
| |
| rdfs:comment
|
- In proof theory, the Gödel–Gentzen negative translation is a method for embedding classical first-order logic into intuitionistic first-order logic. It is one of a number of double-negation translations that are of importance to the metatheory of intuitionistic logic. It is named after logicians Kurt Gödel and Gerhard Gentzen.
|
| rdfs:label
|
- Gödel–Gentzen negative translation
|
| owl:sameAs
| |
| skos:subject
| |
| foaf:page
| |
| is dbpprop:redirect
of | |
![[RDF Data]](/statics/sw-cube.png)
