Twierdzenie Gödla - Polski Serwis Naukowy

Twierdzenie Gödla to jeden z najbardziej znanych rezultatów logiki matematycznej. W istocie znane są dwa różne twierdzenia Gödla: pierwsze z nich to twierdzenie o niezupełności, drugie zaś to jego bezpośredni (równoważny) wniosek nazywany też twierdzeniem o niedowodliwości niesprzeczności. Oba twierdzenia zostały udowodnione w 1931 roku przez austriackiego matematyka i logika Kurta Gödla. Uważa się również, że twierdzenia te dają negatywną odpowiedź na drugi problem Hilberta, i w ten sposób mają spore znaczenie w filozofii matematyki. Inne bardzo ważne twierdzenia Gödla to: twierdzenie o istnieniu modelu i twierdzenie o nierozstrzygalności (patrz: teoria, struktura matematyczna).

Rachunek predykatów pierwszego rzędu – (ang. first order predicate calculus) to system logiczny, w którym zmienna, na której oparty jest kwantyfikator, może być elementem pewnej wybranej dziedziny (zbioru), nie może natomiast być zbiorem takich elementów. Tak więc nie mogą występować kwantyfikatory typu "dla każdej funkcji z X na Y ..." (gdyż funkcja jest podzbiorem X × Y), "istnieje własność p, taka że ..." czy "dla każdego podzbioru X zbioru Z ...". Rachunek ten nazywa się też krótko rachunkiem kwantyfikatorów, ale często używa się też nazwy logika pierwszego rzędu (szczególnie wśród matematyków zajmujących się logiką matematyczną).
Kwantyfikator – termin przyjęty w matematyce i logice matematycznej na oznaczenie zwrotów: dla każdego, istnieje takie i im pokrewnych, a także odpowiadającym im symbolom wiążacym zmienne w formułach. Są podstawowym elementem w rozwoju logiki pierwszego rzędu.

Kontekst

Twierdzenie Gödla było odpowiedzią na próbę przedstawienia wszystkich aksjomatów i twierdzeń matematycznych w postaci czysto symbolicznej (syntaktycznej), tzn. bez odwoływania się do ich znaczenia (czyli w oderwaniu od semantyki; por. logicyzm, formalizm). Próby takiej podjął się m.in. David Hilbert.

Język – Zbiór termów (zdań) tworzonych według pewnych reguł.

Definicja intuicyjna: Maszyna Turinga stanowi najprostszy, wyidealizowany matematyczny model komputera, zbudowany z taśmy, na której zapisuje się dane i poruszającej się wzdłuż niej "głowicy", wykonującej proste operacje na zapisanych na taśmie wartościach.
W logice matematycznej przez język rozumie się pewien zbiór symboli, przy użyciu których można tworzyć bardziej złożone wyrażenia (na przykład formuły, zdania) według ściśle określonych reguł syntaktycznych. Przyjmuje się, że w danym języku L mogą występować (w dowolnej ilości) symbole funkcyjne, relacyjne oraz symbole stałych. Zdania napisane przy użyciu języków tego typu wystarczają do opisu większości własności dowolnych struktur matematycznych oraz do wyrażenia twierdzeń mówiących o tych strukturach.

Teoria matematyczna nad pewnym językiem – Przyporządkowanie zdaniom w określonym języku własności prawdy lub fałszu. Teoria nadaje językowi znaczenie i opisuje pewną matematyczną rzeczywistość. Teoria pozwala odpowiedzieć, czy dane zdanie jest prawdziwe.

System formalny – Zbiór aksjomatów (zdań) wraz z regułami wnioskowania (algorytmem) generujący pewien podzbiór zdań języka. System formalny jest "przybliżeniem" teorii matematycznej. Pozwala odpowiedzieć, czy dane zdanie jest dowodliwe. Dla jednej teorii może istnieć wiele różnych systemów formalnych (aksjomatyzacji) przybliżających ją lepiej lub gorzej. Jeżeli zdanie jest dowodliwe, to musi być ono prawdziwe (ale niekoniecznie na odwrót).

Struktura matematyczna - zbiór obiektów matematycznych połączonych w pewien system. Często można się spotkać z innymi nazwami struktury matematycznej, na przykład: model, system semantyczny, model semantyczny, dziedzina, struktura pierwszego rzędu.
Aksjomat (postulat, pewnik; gr. αξιωμα aksíoma – godność, pewność, oczywistość) – jedno z podstawowych pojęć logiki matematycznej. Od czasów Euklidesa uznawano, że aksjomaty to zdania przyjmowane za prawdziwe, których nie dowodzi się w obrębie danej teorii matematycznej. We współczesnej matematyce definicja aksjomatu jest nieco inna:

System formalny niesprzeczny – System, w którym nie da się udowodnić jednocześnie pewnego zdania i jego zaprzeczenia.

System formalny zupełny – System, w którym możliwe jest przeprowadzenie dowodu dowolnego, prawidłowo zapisanego zdania tego systemu, lub jego zaprzeczenia. W systemie zupełnym każde prawdziwe zdanie jest dowodliwe.

System formalny pierwszego rzędu – System, w którym użyto wyłącznie standardowych reguł wnioskowania oraz wszystkie jego aksjomaty są wyrażone w logice pierwszego rzędu, czyli nie dopuszcza się kwantyfikatorów po zmiennych przebiegających zbiory.

Liczby naturalne – liczby służące podawaniu liczności (trzy osoby, zob. liczebnik główny/kardynalny) i ustalania kolejności (trzecia osoba, zob. liczebnik porządkowy), poddane w matematyce dalszym uogólnieniom (odpowiednio: liczby kardynalne, liczby porządkowe). Badaniem własności liczb naturalnych zajmują się arytmetyka i teoria liczb.
Logika matematyczna – dział matematyki, który wyodrębnił się jako samodzielna dziedzina na przełomie XIX i XX wieku, wraz z dążeniem do dogłębnego zbadania podstaw matematyki. Koncentruje się ona na analizowaniu zasad rozumowania oraz pojęć z nim związanych z wykorzystaniem sformalizowanych oraz uściślonych metod i narzędzi matematyki.

System formalny rozstrzygalny (efektywny) – Taki system, którego algorytm wnioskowania da się zaprogramować na maszynie Turinga. Żeby system był rozstrzygalny potrzeba i wystarcza, żeby istniała tylko jedna (ale odpowiednia) reguła wnioskowania (najczęściej przyjmuje się modus ponens) oraz żeby jego zbiór aksjomatów dał się wygenerować przy pomocy maszyny Turinga.

Zbiór skończony - oznacza w matematyce zbiór równoliczny ze zbiorem {1, 2, ..., n} dla pewnej liczby naturalnej n. Definicja ta obejmuje również zbiór pusty, wystarczy przyjąć n = 0.
Logicyzm to kierunek w filozofii matematyki, zakładający, że można oprzeć jej podstawy na bazie rachunku logicznego zdań (porównaj logika). W szczególności sprowadza to matematykę jako naukę do szczególnego rodzaju formalnej teorii logicznej implementującej pewien zestaw aksjomatów i wyprowadzającej z nich wnioski w oparciu o pewien zespół definicji (porównaj: formalizm (matematyka)).

Aksjomatyka Peano – Pewien system formalny pierwszego rzędu opisujący liczby naturalne.

czytaj dalej: [2], [3]

w oparciu o Wikipedię (licencja GFDL, CC-BY-SA 3.0, autorzy, historia, edycja)