Twierdzenie Gödla o przyspieszeniu - Gödel's speed-up theorem

W matematyce twierdzenie Gödla o przyspieszeniu , udowodnione przez Gödla  ( 1936 ), pokazuje, że istnieją twierdzenia, których dowody można drastycznie skrócić, pracując w potężniejszych systemach aksjomatycznych.

Kurt Gödel pokazał, jak znaleźć wyraźne przykłady zdań w systemach formalnych, które można w tym systemie udowodnić, ale których najkrótszy dowód jest niewyobrażalnie długi. Na przykład oświadczenie:

„To stwierdzenie nie może być udowodnione w arytmetyce Peano w mniej niż symbolach googolplex ”

jest do udowodnienia w arytmetyce Peano (PA), ale najkrótszy dowód ma przynajmniej symbole googolplex, przez argument podobny do dowodu pierwszego twierdzenia Gödla o niezupełności : Jeśli PA jest niesprzeczny, to nie może udowodnić twierdzenia w mniej niż symbolach googolplex, ponieważ samo istnienie takiego dowodu byłoby twierdzeniem PA, sprzecznością. Ale proste wyliczenie wszystkich łańcuchów o długości aż do googolplex i sprawdzenie, czy każdy taki łańcuch nie jest dowodem (w PA) instrukcji, daje dowód instrukcji (który jest koniecznie dłuższy niż symbole googolplex).

Zdanie to ma krótki dowód w potężniejszym systemie: w rzeczywistości dowód podany w poprzednim akapicie jest dowodem w systemie arytmetyki Peano plus zdanie „Arytmetyka Peano jest niesprzeczna” (którego według twierdzenia o niezupełności nie można udowodnić w arytmetyce Peano).

W tym argumencie arytmetyka Peano może zostać zastąpiona przez dowolny mocniejszy spójny system, a googolplex może zostać zastąpiony dowolną liczbą, którą można zwięźle opisać w systemie.

Harvey Friedman znalazł kilka wyraźnych naturalnych przykładów tego zjawiska, podając kilka wyraźnych stwierdzeń w arytmetyce Peano i innych systemach formalnych, których najkrótsze dowody są śmiesznie długie ( Smoryński 1982 ). Na przykład stwierdzenie

„istnieje liczba całkowita n taka, że ​​jeśli istnieje ciąg ukorzenionych drzew T 1 , T 2 , ..., T n taki, że T k ma co najwyżej k +10 wierzchołków, to pewne drzewo może być homeomorficznie osadzone w późniejszym jeden"

można udowodnić w arytmetyce Peano, ale najkrótszy dowód ma długość co najmniej A (1000), gdzie A (0)=1 i A ( n +1)=2 A ( n ) . Stwierdzenie jest szczególnym przypadkiem twierdzenia Kruskala i ma krótki dowód w arytmetyce drugiego rzędu .

Jeśli weźmiemy arytmetykę Peano wraz z negacją powyższego zdania, otrzymamy niespójną teorię, której najkrótsza znana sprzeczność jest równoważnie długa.

Zobacz też

Bibliografia

  • Buss, Samuel R. (1994), „O twierdzeniach Gödla o długości dowodów. I. Liczba linii i przyspieszenie dla arytmetyki”, The Journal of Symbolic Logic , 59 (3): 737-756, doi : 10.2307/2275906 , ISSN  0022-4812 , JSTOR  2275906 , MR  1295967
  • Buss, Samuel R. (1995), "O twierdzeniach Gödla o długościach dowodów. II. Dolne granice rozpoznawania dowodliwości symbolu k", w Clote, Peter; Remmel, Jeffrey (red.), Matematyka wykonalna, II (Ithaca, NY, 1992) , Progr. Komputer. Nauka. Zał. Logika, 13 , Boston, MA: Birkhäuser Boston, s. 57-90, ISBN 978-0-8176-3675-3, MR  1322274
  • Gödel, Kurt (1936), „Über die Lange von Beweisen” , Ergebnisse eines Mathematischen Kolloquiums (w języku niemieckim), 7 : 23-24, ISBN 9780195039641, Przedrukowany z tłumaczeniem na język angielski w pierwszym tomie jego dzieł zebranych.
  • Smoryński, C. (1982), "Rozmaitości doświadczenia nadrzewnego", Matematyka. Wywiadowca , 4 (4): 182-189, doi : 10.1007/bf03023553 , MR  0685558