Diagonalt lemma - Diagonal lemma

I matematisk logik fastställer det diagonala lemmet (även känt som diagonaliseringslemma , självreferenslemma eller fixpunktens teorem ) existensen av självrefererande meningar i vissa formella teorier om de naturliga siffrorna - specifikt de teorier som är starka nog för att representera alla beräknbara funktioner . De meningar vars existens är säkrad av det diagonala lemmet kan sedan i sin tur användas för att bevisa grundläggande begränsande resultat som Gödels ofullständighetsteorems och Tarskis odefinieringssats .

Bakgrund

Låt vara en uppsättning naturliga tal . En teori T representerar den beräkningsbar funktion om det finns en "kurva" predikat på språket i T så att för varje , T bevisar ${\ displaystyle \ mathbb {N}}$ ${\ displaystyle f: \ mathbb {N} \ rightarrow \ mathbb {N}}$ ${\ displaystyle \ Gamma _ {f} (x, y)}$ ${\ displaystyle x \ in \ mathbb {N}}$

{\ displaystyle \ forall y \ quad \ left ({} ^ {\ circ} f (x) = y \ Leftrightarrow \ Gamma _ {f} ({} ^ {\ circ} x, y) \ höger)}

.

Här är siffran som motsvarar det naturliga talet , som definieras som den slutna termen 1+ ··· +1 ( enor), och är siffran som motsvarar . ${\ displaystyle {} ^ {\ circ} x}$ ${\ displaystyle x}$ ${\ displaystyle x}$ ${\ displaystyle {} ^ {\ circ} f (x)}$ ${\ displaystyle f (x)}$

Den fixpunktssatsen kräver också att det finns ett systematiskt sätt att tilldela varje formel θ ett naturligt tal # ( θ ) kallas dess Gödel nummer . Formler kan sedan representeras inom teorin med siffrorna som motsvarar deras Gödel-nummer. Till exempel representeras θ av ° # ( θ )

Det diagonala lemmaet gäller teorier som kan representera alla primitiva rekursiva funktioner . Sådana teorier inkluderar Peano-aritmetik och den svagare Robinson-aritmetiken . Ett vanligt uttalande av lemma (som ges nedan) gör det starkare antagandet att teorin kan representera alla beräkningsbara funktioner .

Uttalande av lemma

Låt T vara en första ordningsteori på aritmetikens språk och som kan representera alla beräkningsbara funktioner . Låt F vara en formel på språket med en fri variabel, sedan:

Lemma - Det finns en mening så att är bevisas i T . ${\ displaystyle \ psi}$ ${\ displaystyle \ psi \ iff F (^ {\ circ} \ # (\ psi))}$

Intuitivt är en självrefererande mening att säga att har egenskapen F . Meningen kan också ses som en fast punkt i operationen som tilldelar meningen till varje formel . Meningen konstrueras i beviset är inte bokstavligen densamma som , men är bevisligen motsvarar den i teorin T . ${\ displaystyle \ psi}$ ${\ displaystyle \ psi}$ ${\ displaystyle \ psi}$ ${\ displaystyle \ theta}$ ${\ displaystyle F (^ {\ circ} \ # (\ theta))}$ ${\ displaystyle \ psi}$ ${\ displaystyle F (^ {\ circ} \ # (\ psi))}$

Bevis

Låt f : N → N vara den funktion som definieras av:

f (# ( θ )) = # ( θ (° # ( θ )))

för varje T- formel θ i en fri variabel, och f ( n ) = 0 annars. Funktionen f är beräkningsbar, så det finns en formel Γ _f representerar f i T . Sålunda för varje formel θ , t bevisar

(∀ y ) [Γ _f (° # ( θ ), y ) ↔ y = ° f (# ( θ ))],

det vill säga

(∀ y ) [Γ _f (° # ( θ ), y ) ↔ y = ° # ( θ (° # ( θ )))].

Definiera nu formeln β ( z ) som:

β ( z ) = (∀ y ) [Γ _f ( z , y ) → F ( y )].

Sedan bevisar T

β (° # ( θ )) ↔ (∀ y ) [ y = ° # ( θ (° # ( θ ))) → F ( y )],

det vill säga

β (° # ( θ )) ↔ F (° # ( θ (° # ( θ )))).

Ta nu θ = β och ψ = β (° # ( β )), och föregående mening skrivs om till ψ ↔ F (° # ( ψ )), vilket är det önskade resultatet.

(Samma argument i olika termer ges i [Raatikainen (2015a)].)

Historia

Lemmet kallas "diagonalt" eftersom det liknar Cantors diagonala argument . Termerna "fixpunktssatsen" eller "fast punkt" visas inte i Kurt Gödel 's 1931 artikeln eller i Alfred Tarski : s 1936 artikeln .

Rudolf Carnap (1934) var den första som bevisade det allmänna självreferenslemmaet , som säger att för vilken formel F som helst i en teori T som uppfyller vissa villkor finns det en formel ψ så att ψ ↔ F (° # ( ψ )) är bevisas i T . Carnaps arbete formulerades på ett annat språk, eftersom begreppet beräknbara funktioner ännu inte utvecklades 1934. Mendelson (1997, s. 204) anser att Carnap var den första som påstod att något liknande det diagonala lemmet var implicit i Gödels resonemang. Gödel var medveten om Carnaps arbete 1937.

Det diagonala lemmet är nära besläktat med Kleenes rekursionssats i beräkbarhetsteorin , och deras respektive bevis är likartade.

Se även

Anteckningar

Referenser

George Boolos and Richard Jeffrey , 1989. Computability and Logic , 3rd ed. Cambridge University Press. ISBN 0-521-38026-X ISBN 0-521-38923-2
Rudolf Carnap , 1934. Logische Syntax der Sprache . (Engelsk översättning: 2003. The Logical Syntax of Language . Open Court Publishing.)
Haim Gaifman , 2006. ' Naming and Diagonalization: From Cantor to Gödel to Kleene '. Logic Journal of the IGPL, 14: 709–728.
Hinman, Peter, 2005. Grundläggande för matematisk logik . AK Peters. ISBN 1-56881-262-0
Mendelson, Elliott , 1997. Introduction to Mathematical Logic , 4th ed. Chapman & Hall.
Panu Raatikainen, 2015a. Diagonaliseringslemma . I Stanford Encyclopedia of Philosophy , red. Zalta. Tillägg till Raatikainen (2015b).
Panu Raatikainen, 2015b. Gödel's ofullständighetssatser . I Stanford Encyclopedia of Philosophy , red. Zalta.
Raymond Smullyan , 1991. Gödel's Incompleteness Theorems . Oxford Univ. Tryck.
Raymond Smullyan, 1994. Diagonalisering och självreferens . Oxford Univ. Tryck.
Alfred Tarski (1936). "Der Wahrheitsbegriff in den formalisierten Sprachen" (PDF) . Studia Philosophica . 1 : 261–405. Arkiverad från originalet (PDF) den 9 januari 2014 . Hämtad 26 juni 2013 . CS1 maint: avskräckt parameter ( länk )
- Alfred Tarski , tr. JH Woodger, 1983. "Sanningskonceptet i formaliserade språk". Engelsk översättning av Tarskis artikel från 1936 . I A. Tarski, red. J. Corcoran, 1983, Logik, semantik, metamatematik , Hackett.

Languages

In other projects