Dubbelnegerande översättning

I bevisteorin , en disciplin inom matematisk logik , är dubbelnegationsöversättning , ibland kallad negativ översättning , ett allmänt tillvägagångssätt för att bädda in klassisk logik i intuitionistisk logik, typiskt genom att översätta formler till formler som är klassiskt likvärdiga men intuitionistiskt olikvärdiga. Särskilda exempel på dubbelnegationsöversättning inkluderar Glivenkos översättning för propositionell logik , och Gödel–Gentzen-översättningen och Kurodas översättning för första ordningens logik .

Propositionell logik

Den enklaste dubbelnegationsöversättningen att beskriva kommer från Glivenkos teorem , bevisad av Valery Glivenko 1929. Den mappar varje klassisk formel φ till dess dubbla negation ¬¬φ.

Glivenkos sats säger:

Om φ är en propositionell formel, så är φ en klassisk tautologi om och endast om ¬¬φ är en intuitionistisk tautologi.

Glivenkos sats antyder det mer allmänna uttalandet:

Om T är en uppsättning satsformler och φ en satsformel, så är T ⊢ φ i klassisk logik om och endast om T ⊢ ¬¬φ i intuitionistisk logik.

I synnerhet är en uppsättning propositionella formler intuitionistiskt konsekvent om och bara om den är klassiskt tillfredsställande.

Första ordningens logik

Gödel –Gentzen-översättningen (uppkallad efter Kurt Gödel och Gerhard Gentzen ) associerar med varje formel φ i ett första ordningens språk en annan formel φ ^N , som definieras induktivt:

Om φ är atomär, så är φ ^{N ¬¬φ}
(φ ∧ θ) ^N är φ ^N ∧ θ ^N
(φ ∨ θ) ^N är ¬(¬φ ^N ∧ ¬θ ^N )
(φ → θ) ^N är φ ^N → θ ^N
(¬φ) ^N är ¬φ ^N
(∀ x φ) ^N är ∀ x φ ^N
(∃ x φ) ^N är ¬∀ x ¬φ ^N

Denna översättning har egenskapen att φ ^N är klassiskt ekvivalent med φ. Den fundamentala sundhetssatsen (Avigad och Feferman 1998, s. 342; Buss 1998 s. 66) säger:

Om T är en uppsättning axiom och φ är en formel, så ^bevisar T φ med klassisk logik om och endast om TN bevisar φ ^N med intuitionistisk logik.

Här består T ^N av dubbelnegationsöversättningarna av formlerna i T .

En mening φ kanske inte antyder dess negativa översättning φ ^N i intuitionistisk första ordningens logik. Troelstra och van Dalen (1988, kap. 2, avsnitt 3) ger en beskrivning (på grund av Leivant) av formler som antyder deras Gödel–Gentzen-översättning.

Varianter

Det finns flera alternativa definitioner av den negativa översättningen. De är alla bevisligen likvärdiga i intuitionistisk logik, men kan vara lättare att tillämpa i särskilda sammanhang.

En möjlighet är att ändra klausulerna för disjunktion och existentiell kvantifierare till

(φ ∨ θ) ^N är ¬¬(φ ^N ∨ θ ^N )
(∃ x φ) ^N är ¬¬∃ x φ ^N

Sedan kan översättningen kortfattat beskrivas som: prefix ¬¬ till varje atomformel, disjunktion och existentiell kvantifierare.

En annan möjlighet (känd som Kurodas översättning) är att konstruera φ ^N från φ genom att sätta ¬¬ före hela formeln och efter varje universell kvantifierare . Lägg märke till att detta reduceras till den enkla ¬¬φ-översättningen om φ är propositionell.

Det är också möjligt att definiera φ ^N genom att sätta prefixet ¬¬ före varje delformel av φ, som gjorts av Kolmogorov . En sådan översättning är den logiska motsvarigheten till översättningen av funktionella programmeringsspråk i linje med Curry-Howard - korrespondensen mellan korrektur och program.

Resultat

Dubbelnegationsöversättningen användes av Gödel (1933) för att studera sambandet mellan klassiska och intuitionistiska teorier om de naturliga talen ("aritmetik"). Han får följande resultat:

Om en formel φ är bevisbar från axiomen för Peano-aritmetiken så är φ ^N bevisbar från axiomen för Heyting-aritmetiken .

Detta resultat visar att om Heyting-arithmetiken är konsekvent så är Peano-aritmetiken det också. Detta beror på att en motsägelsefull formel θ ∧ ¬θ tolkas som θ ^N ∧ ¬θ ^N , vilket fortfarande är motsägelsefullt. Dessutom är beviset på sambandet helt konstruktivt, vilket ger ett sätt att omvandla ett bevis på θ ∧ ¬θ i Peano-aritmetik till ett bevis på θ ^N ∧ ¬θ ^N i Heyting-arithmetik. (Genom att kombinera dubbelnegationsöversättningen med Friedman-översättningen är det faktiskt möjligt att bevisa att Peano-arithmetik är ⁰ Π ₂ - konservativ över Heyting-aritmetik.)

Propositionsmappingen av φ till ¬¬φ sträcker sig inte till en sund översättning av första ordningens logik, eftersom det så kallade dubbelnegationsskiftet

∀ x ¬¬φ( x ) → ¬¬∀ x φ( x )

är inte ett teorem för intuitionistisk predikatlogik. Detta förklarar varför φ ^N måste definieras på ett mer komplicerat sätt i första ordningens fall.

Se även

Dialektisk tolkning

J. Avigad och S. Feferman (1998), "Gödels funktionella ("Dialectica") tolkning", Handbook of Proof Theory , S. Buss, red., Elsevier. ISBN 0-444-89840-9
S. Buss (1998), "Introduction to Proof Theory", Handbook of Proof Theory , S. Buss, red., Elsevier. ISBN 0-444-89840-9
G. Gentzen (1936), "Die Widerspruchfreiheit der reinen Zahlentheorie", Mathematische Annalen , v. 112, s. 493–565 (tyska). Omtryckt i engelsk översättning som "The consistency of aritmetic" i The collected papers of Gerhard Gentzen, ME Szabo, ed.
V. Glivenko (1929), Sur quelques points de la logique de M. Brouwer , Bull. Soc. Matematik. Belg. 15, 183-188
K. Gödel (1933), "Zur intuitionistischen Arithmetik und Zahlentheorie", Ergebnisse eines mathematischen Kolloquiums , v. 4, s. 34–38 (tyska). Omtryckt i engelsk översättning som "On intuitionistic aritmetic and number theory" i The Undecidable , M. Davis, ed., s. 75–81.
AN Kolmogorov (1925), "O principe tertium non datur" (ryska). Omtryckt i engelsk översättning som "On the princip of the excluded middle" i From Frege to Gödel , van Heijenoort, ed., s. 414–447.
AS Troelstra (1977), "Aspects of Constructive Mathematics", Handbook of Mathematical Logic , J. Barwise , red., North-Holland. ISBN 0-7204-2285-X
AS Troelstra och D. van Dalen (1988), Constructivism in Mathematics. An Introduction , volymerna 121, 123 av Studies in Logic and the Foundations of Mathematics , North–Holland.

externa länkar

" Intuitionistisk logik ", Stanford Encyclopedia of Philosophy.