Twierdzenie Tarskiego o niedefiniowalności - Tarski's undefinability theorem

Twierdzenie Tarskiego o niedefiniowalności , stwierdzone i udowodnione przez Alfreda Tarskiego w 1933 roku, jest ważnym ograniczającym rezultatem logiki matematycznej , podstaw matematyki i semantyki formalnej . Nieformalnie twierdzenie stwierdza, że prawdy arytmetycznej nie można zdefiniować w arytmetyce .

Twierdzenie to stosuje się bardziej ogólnie do każdego wystarczająco silnego systemu formalnego , pokazując, że prawdy w standardowym modelu systemu nie można zdefiniować w systemie.

Historia

W 1931 Kurt Gödel opublikował twierdzenia o niezupełności , które częściowo udowodnił, pokazując, jak przedstawiać składnię logiki formalnej w arytmetyce pierwszego rzędu . Każdemu wyrażeniu formalnego języka arytmetyki przypisywana jest odrębna liczba. Ta procedura jest znana jako numeracja Gödla , kodowanie i, bardziej ogólnie, jako arytmetyzacja. W szczególności różne zestawy wyrażeń są kodowane jako zestawy liczb. Dla różnych właściwości składniowych (takich jak bycie formułą , bycie zdaniem itp.) zbiory te są obliczalne . Co więcej, każdy obliczalny zbiór liczb można zdefiniować za pomocą jakiegoś wzoru arytmetycznego. Na przykład w języku arytmetyki istnieją formuły definiujące zbiór kodów dla zdań arytmetycznych i dla zdań arytmetycznych dowodzalnych.

Twierdzenie o niedefiniowalności pokazuje, że tego kodowania nie można wykonać dla pojęć semantycznych , takich jak prawda. Pokazuje, że żaden wystarczająco bogaty interpretowany język nie może reprezentować własnej semantyki. W konsekwencji każdy metajęzyk zdolny do wyrażenia semantyki jakiegoś języka przedmiotowego musi mieć moc ekspresyjną przewyższającą moc języka przedmiotowego. Metajęzyk zawiera pierwotne pojęcia, aksjomaty i reguły nieobecne w języku przedmiotowym, tak że istnieją twierdzenia, które można udowodnić w metajęzyku, których nie można udowodnić w języku przedmiotowym.

Twierdzenie o niedefiniowalności umownie przypisuje się Alfredowi Tarskiemu . Gödel odkrył również twierdzenie o niedefiniowalności w 1930, udowadniając swoje twierdzenia o niezupełności opublikowane w 1931, a na długo przed publikacją w 1933 pracy Tarskiego (Murawski 1998). Chociaż Gödel nigdy nie opublikował niczego związanego z jego niezależnym odkryciem niedefiniowalności, opisał to w liście z 1931 roku do Johna von Neumanna . Tarski uzyskał niemal wszystkie wyniki jego 1933 monografii „ pojęcie Prawdy wag Językach Nauk Dedukcyjnych ” ( „ pojęcia prawdy w językach nauk dedukcyjnych ”) między 1929 i 1931, i mówił o nich do polskich odbiorców. Jednak, jak podkreślił w artykule, twierdzenie o niedefiniowalności było jedynym wynikiem, którego wcześniej nie uzyskał. Zgodnie z przypisem do twierdzenia o niedefiniowalności (Twierdzenie I) z monografii z 1933 r. twierdzenie i szkic dowodu zostały dodane do monografii dopiero po przesłaniu rękopisu do drukarni w 1931 r. Tarski podaje tam, że gdy przedstawił w treści swojej monografii do Warszawskiej Akademii Nauk w dniu 21 marca 1931 r. wypowiedział w tym miejscu tylko niektóre przypuszczenia, oparte częściowo na własnych badaniach, a częściowo na krótkim raporcie Gödla na temat twierdzeń o niezupełności "Einige metamathematische Resultate über Entscheidungsdefinitheit und Wiperspruchsfreiheit ”, Akademie der Wissenschaften w Wiedniu, 1930.

Komunikat

Najpierw podamy uproszczoną wersję twierdzenia Tarskiego, a następnie podamy i udowodnimy w następnej sekcji twierdzenie, które Tarski udowodnił w 1933 roku. Niech L będzie językiem arytmetyki pierwszego rzędu , a N będzie standardową strukturą dla L . Tak więc ( L , N ) jest „interpretowanym językiem arytmetyki pierwszego rzędu”. Każda formuła x w L ma liczbę Gödla g ( x ). Niech T oznacza zbiór L- formuł prawdziwych w N , a T * zbiór liczb Gödla dla formuł w T . Poniższe twierdzenie odpowiada na pytanie: Czy T * można zdefiniować wzorem arytmetyki pierwszego rzędu?

Twierdzenie Tarskiego o niedefiniowalności : Nie ma formuły L Prawda ( n ), która definiuje T *. Oznacza to, że nie ma L -formula prawdziwego ( N ) w taki sposób, że dla każdego L -formula A , prawda ( g ( )) ↔ ładowni.

Nieformalnie twierdzenie mówi, że przy pewnej formalnej arytmetyce pojęcie prawdy w tej arytmetyce nie jest definiowalne za pomocą wyrazistych środków, które daje ta arytmetyka. Oznacza to poważne ograniczenie zakresu „autoreprezentacji”. Możliwe jest zdefiniowanie formuły True ( n ) o rozszerzeniu T * , ale tylko na podstawie metajęzyka , którego siła wyrazu wykracza poza L . Na przykład predykat prawdy dla arytmetyki pierwszego rzędu można zdefiniować w arytmetyce drugiego rzędu . Formuła ta byłaby jednak w stanie zdefiniować predykat prawdziwościowy tylko dla formuł w oryginalnym języku L . Zdefiniowanie predykatu prawdy dla metajęzyka wymagałoby jeszcze wyższego metajęzyka i tak dalej.

Twierdzenie to jest następstwem twierdzenia Posta o hierarchii arytmetycznej , udowodnionego kilka lat po Tarskim (1933). Dowód semantyczny twierdzenia Tarskiego z twierdzenia Posta uzyskuje się przez reductio ad absurdum w następujący sposób. Zakładając, T * jest arytmetycznie definiowane, jest liczbą naturalną, n , takich, że t * jest definiowane przez wzór na poziomie w hierarchii arytmetycznej . Jednak T * jest -trudny dla wszystkich k . W ten sposób hierarchia arytmetyczna załamuje się na poziomie n , przecząc twierdzeniu Posta.

Ogólna forma

Tarski udowodnił twierdzenie silniejsze od powyższego, używając całkowicie syntaktycznej metody. Wynikające z tego twierdzenie stosuje się do dowolnego języka formalnego z negacją i wystarczającą zdolnością do samoodniesienia , jaką posiada lemat diagonalny . Arytmetyka pierwszego rzędu spełnia te warunki wstępne, ale twierdzenie dotyczy znacznie bardziej ogólnych systemów formalnych.

Twierdzenie Tarskiego o niedefiniowalności (forma ogólna) : Niech ( L , N ) będzie dowolnym interpretowanym językiem formalnym, który zawiera negację i ma numerację Gödla g ( x ) taką, że dla każdej formuły L A ( x ) istnieje formuła B taka, że B ↔ A ( g ( B )) zachodzi w N . Niech T * będzie zbiorem liczb Gödla dla L- formuły prawdziwej w N . Wtedy nie ma formuły L True ( n ), która definiuje T *. Oznacza to, że nie ma formuły L True ( n ) w taki sposób , że dla każdej formuły L A , True ( g ( A )) ↔ A sama jest prawdziwa w N .

Dowodem twierdzenia Tarskiego o niedefiniowalności w tej postaci jest ponownie reductio ad absurdum . Załóżmy, że formuła L True ( n ) definiuje T *. W szczególności, jeśli A jest formułą arytmetyczną, wtedy Prawda ( g ( A )) zachodzi w N wtedy i tylko wtedy, gdy A zachodzi w N . Stąd dla wszystkich A formuła True ( g ( A )) ↔ A zachodzi w N . Ale lemat diagonalny dostarcza kontrprzykładu dla tej równoważności, podając formułę „kłamcy” S taką, że S ↔ ¬ Prawda ( g ( S )) zachodzi w N . Zatem żadna formuła L True ( n ) nie może zdefiniować T *. CO BYŁO DO OKAZANIA.

Formalna maszyneria tego dowodu jest całkowicie elementarna, z wyjątkiem diagonalizacji, której wymaga lemat diagonalny. Dowód lematu diagonalnego jest również zaskakująco prosty; na przykład w żaden sposób nie wywołuje funkcji rekurencyjnych . Dowód zakłada, że ​​każda formuła L ma liczbę Gödla , ale specyfika metody kodowania nie jest wymagana. Stąd twierdzenie Tarskiego jest znacznie łatwiejsze do uzasadnienia i udowodnienia niż bardziej znane twierdzenia Gödla o metamatematycznych własnościach arytmetyki pierwszego rzędu .

Dyskusja

Smullyan (1991, 2001) dobitnie argumentował, że twierdzenie Tarskiego o niedefiniowalności zasługuje na wiele uwagi, jaką przykuwają twierdzenia Gödla o niezupełności . To, że te ostatnie twierdzenia mają wiele do powiedzenia o całej matematyce i, co bardziej kontrowersyjne, o szeregu zagadnień filozoficznych (np. Lucas 1961) jest mniej niż oczywiste. Z drugiej strony, twierdzenie Tarskiego nie dotyczy bezpośrednio matematyki, ale nieodłącznych ograniczeń każdego języka formalnego wystarczająco wyrazistego, by wzbudzić rzeczywiste zainteresowanie. Takie języki muszą być w stanie na tyle samo-odniesienia dla przekątnej lemat stosuje się do nich. Bardziej uderzający jest szerszy filozoficzny wymiar twierdzenia Tarskiego.

Język interpretowany jest silnie semantycznie samoreprezentacyjny dokładnie wtedy, gdy zawiera predykaty i symbole funkcyjne definiujące wszystkie koncepcje semantyczne specyficzne dla języka. Stąd wymagane funkcje obejmują „funkcję wyceny semantycznej” odwzorowującą formułę A na jej wartość logiczną || A || i „semantyczna funkcja denotacji” odwzorowująca termin t na obiekt, który oznacza. Twierdzenie Tarskiego uogólnia zatem w następujący sposób: Żaden wystarczająco mocny język nie jest silnie semantycznie samoreprezentacyjny .

Twierdzenie o niedefiniowalności nie uniemożliwia zdefiniowania prawdy w jednej teorii w silniejszej teorii. Na przykład zestaw (kodów) formuł arytmetyki Peano pierwszego rzędu, które są prawdziwe w N, można zdefiniować za pomocą formuły w arytmetyce drugiego rzędu . Podobnie zbiór prawdziwych formuł standardowego modelu arytmetyki drugiego rzędu (lub arytmetyki n-tego rzędu dla dowolnego n ) można zdefiniować za pomocą formuły w ZFC pierwszego rzędu .

Zobacz też

Bibliografia

  • JL Bell i M. Machover, 1977. Kurs logiki matematycznej . Północna Holandia.
  • G. Boolos , J. Burgess i R. Jeffrey , 2002. Computability and Logic , wyd. Wydawnictwo Uniwersytetu Cambridge.
  • JR Lucas , 1961. „ Umysł, maszyny i Gödel ”. Filozofia 36: 112–27.
  • R. Murawski, 1998. Niedefiniowalność prawdy. Problem priorytetu: Tarski kontra Gödel . Historia i filozofia logiki 19, 153-160
  • R. Smullyan , 1991. Twierdzenia Gödla o niezupełności . Uniwersytet Oksfordzki Naciśnij.
  • R. Smullyan , 2001. „Twierdzenia o niezupełności Gödla”. W L. Goble, ed. The Blackwell Guide to Philosophical Logic , Blackwell, 72-89.
  • A. Tarski 1933. Pozyskanie Prawdy w Językach Nauk Dedukcyjnych . Nakładem Towarzystwa Naukowego Warszawskiego.
  • A. Tarskiego (1936). „Der Wahrheitsbegriff in den formalisierten Sprachen” (PDF) . Studia Filozoficzne . 1 : 261-405. Zarchiwizowane z oryginału (PDF) w dniu 9 stycznia 2014 r . Źródło 26 czerwca 2013 .