Matematyka odwrotna - Reverse mathematics

„Odwrócona matematyka” przekierowuje tutaj. Aby zapoznać się z książką Johna Stillwella, zobacz Reverse Mathematics: Proofs from the Inside Out .

Matematyka odwrotna to program w logice matematycznej, który ma na celu określenie, które aksjomaty są wymagane do udowodnienia twierdzeń matematycznych. Jego metodę definiowania można krótko opisać jako „cofanie się od twierdzeń do aksjomatów ”, w przeciwieństwie do zwykłej matematycznej praktyki wyprowadzania twierdzeń z aksjomatów. Można to konceptualizować jako wyrzeźbienie warunków koniecznych z warunków wystarczających .

Program matematyki odwrotnej został zapowiedziany przez wyniki w teorii mnogości, takie jak klasyczne twierdzenie, że aksjomat wyboru i lemat Zorna są równoważne z teorią mnogości ZF . Celem matematyki odwrotnej jest jednak badanie możliwych aksjomatów zwykłych twierdzeń matematycznych, a nie możliwych aksjomatów teorii mnogości.

Matematyka odwrotna jest zwykle prowadzona przy użyciu podsystemów arytmetyki drugiego rzędu , gdzie wiele jej definicji i metod jest inspirowanych wcześniejszymi pracami nad konstruktywną analizą i teorią dowodu . Zastosowanie arytmetyki drugiego rzędu pozwala również na zastosowanie wielu technik z teorii rekurencji ; wiele wyników w matematyce odwrotnej ma odpowiednie wyniki w analizie obliczeniowej . W matematyce odwrotnej wyższego rzędu nacisk kładziony jest na podsystemy arytmetyki wyższego rzędu i powiązany z nimi bogatszy język.

Program został założony przez Harveya Friedmana  ( 1975 , 1976 ), a rozwinięty przez Steve'a Simpsona . Standardowym odniesieniem do tematu jest Simpson (2009) , natomiast wprowadzeniem dla niespecjalistów jest Stillwell (2018) . Wprowadzeniem do matematyki odwrotnej wyższego rzędu, a także dokumentem założycielskim, jest Kohlenbach (2005) .

Ogólne zasady

W matematyce odwrotnej zaczyna się od języka ramowego i teorii bazowej – podstawowego systemu aksjomatów – który jest zbyt słaby, aby udowodnić większość twierdzeń, którymi możemy być zainteresowani, ale wciąż wystarczająco potężny, aby opracować definicje niezbędne do sformułowania tych twierdzeń. Na przykład, aby zbadać twierdzenie „Każdy ograniczonym sekwencji z liczb rzeczywistych ma supremum ” Konieczne jest, aby korzystać z systemu bazowego, że można mówić o liczbach rzeczywistych i sekwencji liczb rzeczywistych.

Dla każdego twierdzenia, które można sformułować w systemie podstawowym, ale nie można udowodnić w systemie podstawowym, celem jest określenie konkretnego systemu aksjomatów (silniejszego niż system podstawowy), który jest niezbędny do udowodnienia tego twierdzenia. Aby pokazać, że system S jest wymagany do udowodnienia twierdzenia T , wymagane są dwa dowody. Pierwszy dowód pokazuje, że T jest dowodliwe z S ; jest to zwykły dowód matematyczny wraz z uzasadnieniem, że można go przeprowadzić w systemie S . Drugi dowód, znany jako odwrócenie , pokazuje, że samo T implikuje S ; dowód ten jest przeprowadzany w systemie podstawowym. Odwrócenie ustala, że ​​żaden system aksjomatów S′, który rozszerza system bazowy, nie może być słabszy niż S , wciąż udowadniając  T .

Korzystanie z arytmetyki drugiego rzędu

Większość badań nad matematyką odwrotną koncentruje się na podsystemach arytmetyki drugiego rzędu . Badania nad matematyką odwrotną wykazały, że słabe podsystemy arytmetyki drugiego rzędu wystarczają do sformalizowania prawie całej matematyki na poziomie studiów licencjackich. W arytmetyce drugiego rzędu wszystkie obiekty mogą być reprezentowane jako liczby naturalne lub zbiory liczb naturalnych. Na przykład, w celu udowodnienia twierdzenia o liczbach rzeczywistych, rzeczywiste liczby mogą być reprezentowane jako sekwencje Cauchy'ego o liczbach wymiernych , z których każdy może być przedstawiony jako zbiór liczb naturalnych.

Systemy aksjomatów najczęściej rozważane w matematyce odwrotnej są definiowane za pomocą schematów aksjomatów zwanych schematami rozumienia . Taki schemat zakłada, że ​​istnieje dowolny zbiór liczb naturalnych, który można określić wzorem o danej złożoności. W tym kontekście złożoność formuł mierzy się za pomocą hierarchii arytmetycznej i hierarchii analitycznej .

Powodem, dla którego nie stosuje się matematyki odwrotnej przy użyciu teorii mnogości jako systemu bazowego, jest to, że język teorii mnogości jest zbyt ekspresyjny. Niezwykle złożone zbiory liczb naturalnych można zdefiniować za pomocą prostych formuł w języku teorii mnogości (które można kwantyfikować na zbiorach arbitralnych). W kontekście arytmetyki drugiego rzędu wyniki, takie jak twierdzenie Posta, ustanawiają ścisły związek między złożonością formuły a (nie)obliczalnością zbioru, który definiuje.

Innym efektem zastosowania arytmetyki drugiego rzędu jest potrzeba ograniczenia ogólnych twierdzeń matematycznych do form, które można wyrazić w arytmetyce. Na przykład arytmetyka drugiego rzędu może wyrażać zasadę „Każda przeliczalna przestrzeń wektorów ma bazę”, ale nie może wyrażać zasady „Każda przestrzeń wektorów ma bazę”. W praktyce oznacza to, że twierdzenia algebry i kombinatoryki są ograniczone do struktur przeliczalnych, a twierdzenia analizy i topologii do przestrzeni separowalnych . Wiele zasad, które implikują aksjomat wyboru w ich ogólnej formie (takich jak „Każda przestrzeń wektorowa ma podstawę”), staje się możliwych do udowodnienia w słabych podsystemach arytmetyki drugiego rzędu, gdy są one ograniczone. Na przykład „każde pole ma domknięcie algebraiczne” nie jest dowodem w teorii mnogości ZF, ale forma ograniczona „każde pole policzalne ma domknięcie algebraiczne” jest dowodliwa w RCA 0 , najsłabszym systemie zwykle stosowanym w matematyce odwrotnej.

Użycie arytmetyki wyższego rzędu

Niedawny wątek badań nad matematyką odwrotną wyższego rzędu , zainicjowany przez Ulricha Kohlenbacha , koncentruje się na podsystemach arytmetyki wyższego rzędu . Ze względu na bogatszy język arytmetyki wyższego rzędu, użycie reprezentacji (inaczej „kodów”) powszechnych w arytmetyce drugiego rzędu jest znacznie ograniczone. Na przykład funkcja ciągła w przestrzeni Cantora jest po prostu funkcją, która odwzorowuje sekwencje binarne na sekwencje binarne, a także spełnia zwykłą definicję ciągłości „epsilon-delta”.

Matematyka odwrotna wyższego rzędu obejmuje wyższe wersje schematów rozumienia (drugiego rzędu). Taki aksjomat wyższego rzędu stwierdza istnienie funkcjonału, który decyduje o prawdziwości lub fałszywości formuł o danej złożoności. W tym kontekście złożoność formuł mierzy się również za pomocą hierarchii arytmetycznej i hierarchii analitycznej . Wyższego rzędu odpowiedniki głównych podsystemów arytmetyki drugiego rzędu ogólnie dowodzą tych samych zdań drugiego rzędu (lub dużego podzbioru) jak oryginalne systemy drugiego rzędu. Na przykład podstawowa teoria matematyki odwrotnej wyższego rzędu, zwana RCAω
0, dowodzi tych samych zdań co RCA 0 , aż do języka.

Jak zauważono w poprzednim akapicie, aksjomaty zrozumienia drugiego rzędu łatwo uogólniają się na strukturę wyższego rzędu. Twierdzenia wyrażające zwartość podstawowych przestrzeni zachowują się jednak zupełnie inaczej w arytmetyce drugiego i wyższego rzędu: z jednej strony, ograniczając się do policzalnych okładek/języka arytmetyki drugiego rzędu, zwartość przedziału jednostkowego można udowodnić w WKL 0 z następnej sekcji. Z drugiej strony, biorąc pod uwagę niezliczone okładki/język arytmetyki wyższego rzędu, zwartość przedziału jednostkowego można udowodnić tylko z (pełnej) arytmetyki drugiego rzędu. Inne lematy pokrywające (np. Lindelöf , Vitali , Besicovitch , itp.) wykazują to samo zachowanie, a wiele podstawowych własności całki z cechowaniem jest równoważnych zwartości leżącej poniżej przestrzeni.

Wielka piątka podsystemów arytmetyki drugiego rzędu

Arytmetyka drugiego rzędu to formalna teoria liczb i zbiorów liczb naturalnych. Wiele obiektów matematycznych, takich jak policzalne pierścienie , grupy i pola , a także punkty w efektywnych polskich przestrzeniach , można przedstawić jako zbiory liczb naturalnych, a modulo tę reprezentację można badać w arytmetyce drugiego rzędu.

Matematyka odwrotna wykorzystuje kilka podsystemów arytmetyki drugiego rzędu. Typowe twierdzenie matematyczne odwrotne pokazuje, że określone twierdzenie matematyczne T jest równoważne określonemu podsystemowi S arytmetyki drugiego rzędu nad słabszym podsystemem B . Ten słabszy system B jest znany jako system bazowy dla wyniku; aby wynik matematyki odwrotnej miał znaczenie, system ten nie może sam być w stanie udowodnić twierdzenia matematycznego T .

Simpson (2009) opisuje pięć poszczególnych podsystemów arytmetyki drugiego rzędu, które nazywa Wielką Piątką , które często występują w matematyce odwrotnej. W celu zwiększenia wytrzymałości systemy te są nazywane inicjałami RCA 0 , WKL 0 , ACA 0 , ATR 0 , i Π1
1-CA 0 .

Poniższa tabela podsumowuje systemy „wielkiej piątki” i wymienia systemy odpowiedników w arytmetyce wyższego rzędu. Te ostatnie na ogół dowodzą tych samych zdań drugiego rzędu (lub dużego podzbioru) jak oryginalne systemy drugiego rzędu.

Podsystem Oznacza Porządkowy Odpowiada mniej więcej Uwagi Odpowiednik wyższego rzędu
RCA 0 Aksjomat rekurencyjnego rozumienia Ohm Ohm Konstruktywna matematyka ( Biskup ) Podstawowa teoria RCAω
0; dowodzi tego samego zdania drugiego rzędu co RCA 0
WKL 0 Słaby lemat Kőniga Ohm Ohm Finitystyczny redukcjonizm ( Hilbert ) Konserwatywny nad PRA (odp. RCA 0 ) dla Π0
2(odp. Π1
1) zdania 		Wentylator funkcjonalny; oblicza moduł jednostajnej ciągłości dla funkcji ciągłych
ACA 0 Aksjomat arytmetycznego rozumienia ε 0 Predykatywizm ( Weyl , Feferman ) Konserwatywny w stosunku do arytmetyki Peano dla zdań arytmetycznych Funkcjonalność „skoku Turinga” wyraża istnienie funkcji nieciągłej na
ATR 0 Rekurencja arytmetyczna transskończona Γ 0 Redukcjonizm predykatywny (Friedman, Simpson) Konserwatywny w stosunku do systemu Fefermana IR dla Π1
1 zdania 		Funkcjonalność „rekurencja nieskończona” wyprowadza zbiór, który twierdził, że istnieje przez ATR 0 .
Π1
1-CA 0 		Π1
1 aksjomat rozumienia 		Ψ 0 (Ω ω ) Impredykatywizm Decyduje funkcja Suslina Π1
1-formuły (ograniczone do parametrów drugiego rzędu).

Indeks dolny 0 w tych nazwach oznacza, że ​​program edukacyjny został ograniczony z pełnego programu edukacyjnego drugiego rzędu. Na przykład ACA 0 zawiera aksjomat indukcyjny (0 ∈  X  ∧ ∀ n ( n  ∈  X  →  n  + 1 ∈  X )) → ∀ n  n  ∈ X . To wraz z pełnym aksjomatem rozumienia arytmetyki drugiego rzędu implikuje pełny schemat indukcji drugiego rzędu, dany przez uniwersalne domknięcie ( φ (0) ∧ ∀ n ( φ ( n ) → φ ( n +1))) → ∀ n φ ( n ) dla dowolnej formuły drugiego rzędu φ . Jednak ACA 0 nie ma pełnego aksjomatu rozumienia, a indeks dolny 0 przypomina, że ​​nie ma też pełnego schematu indukcji drugiego rzędu. To ograniczenie jest ważne: systemy z ograniczoną indukcją mają znacznie niższe liczby porządkowe teoretyczno-dowodowe niż systemy z pełnym schematem indukcji drugiego rzędu.

System bazowy RCA 0

RCA 0 to fragment arytmetyki drugiego rzędu, której aksjomaty są aksjomatami arytmetyki Robinsona , indukcja dla Σ0
1formuły i rozumienie Δ0
1 formuły.

Podsystem RCA 0 jest najczęściej używanym systemem bazowym dla matematyki odwrotnej. Inicjały „RCA” oznaczają „rekurencyjny aksjomat rozumienia”, gdzie „rekurencyjny” oznacza „obliczalny”, jak w funkcji rekurencyjnej . Ta nazwa jest używana, ponieważ RCA 0 odpowiada nieformalnie „matematyce obliczalnej”. W szczególności każdy zbiór liczb naturalnych, którego istnienie w RCA 0 można udowodnić, jest obliczalny, a zatem każde twierdzenie, które implikuje istnienie zbiorów nieobliczalnych, nie jest udowodnione w RCA 0 . W tym zakresie RCA 0 jest systemem konstruktywnym, choć nie spełnia wymogów programu konstruktywizmu, ponieważ jest teorią w logice klasycznej z uwzględnieniem prawa wyłączonego środka .

Pomimo swojej pozornej słabości (nie udowodnienia istnienia żadnych zbiorów nieobliczalnych), RCA 0 wystarcza do udowodnienia szeregu klasycznych twierdzeń, które w związku z tym wymagają jedynie minimalnej siły logicznej. Twierdzenia te są w pewnym sensie poniżej zasięgu matematyki odwrotnej, ponieważ można je już udowodnić w systemie podstawowym. Klasyczne twierdzenia, które można udowodnić w RCA 0 obejmują:

Część pierwszego rzędu RCA 0 (twierdzenia systemu, które nie obejmują żadnych zmiennych zbiorowych) to zbiór twierdzeń arytmetyki pierwszego rzędu Peano z indukcją ograniczoną do Σ0
1formuły. Jest dowodnie spójny, podobnie jak RCA 0 , w pełnej arytmetyce pierwszego rzędu Peano.

Słaby lemat Kőniga WKL 0

Podsystem WKL 0 składa się z RCA 0 plus słaba forma lematu Kőniga , czyli stwierdzenie, że każde nieskończone poddrzewo pełnego drzewa binarnego (drzewo wszystkich skończonych ciągów zer i jedynek) ma nieskończoną ścieżkę. To zdanie, znane jako słaby lemat Kőniga , jest łatwe do sformułowania w języku arytmetyki drugiego rzędu. WKL 0 można również zdefiniować jako zasadę Σ0
1 separacja (biorąc dwie Σ0
1formuły zmiennej wolnej n, które są wykluczające, istnieje klasa zawierająca wszystkie n spełniające jedno i żadne n nie spełniające drugiego).

Poniższa uwaga dotycząca terminologii jest w porządku. Termin „słaby lemat Kőniga” odnosi się do zdania, które mówi, że każde nieskończone poddrzewo drzewa binarnego ma nieskończoną ścieżkę. Gdy ten aksjomat zostanie dodany do RCA 0 , powstały podsystem nazywa się WKL 0 . Podobne rozróżnienie między poszczególnymi aksjomatami z jednej strony, a podsystemami zawierającymi podstawowe aksjomaty i indukcję z drugiej, dokonuje się dla silniejszych podsystemów opisanych poniżej.

W pewnym sensie słaby lemat Kőniga jest formą aksjomatu wyboru (choć, jak stwierdzono, można go dowieść w klasycznej teorii mnogości Zermelo-Fraenkla bez aksjomatu wyboru). Nie jest konstruktywnie ważne w pewnym sensie słowa konstruktywny.

Aby pokazać, że WKL 0 jest faktycznie silniejszy niż (nie dowodzący w) RCA 0 , wystarczy przedstawić twierdzenie WKL 0, które implikuje istnienie zbiorów nieobliczalnych. To nie jest trudne; WKL 0 implikuje istnienie zbiorów rozdzielających dla efektywnie nierozdzielnych zbiorów rekurencyjnie przeliczalnych.

Okazuje się, że RCA 0 i WKL 0 mają tę samą część pierwszego rzędu, co oznacza, że ​​dowodzą tych samych zdań pierwszego rzędu. WKL 0 może jednak udowodnić dużą liczbę klasycznych wyników matematycznych, które nie wynikają z RCA 0 . Te wyniki nie są wyrażalne jako instrukcje pierwszego rzędu, ale można je wyrazić jako instrukcje drugiego rzędu.

Następujące wyniki są równoważne słabemu lematowi Kőniga, a więc WKL 0 nad RCA 0 :

  • Twierdzenie Heinego-Borela dla domkniętego przedziału rzeczywistego, w następującym sensie: każde pokrycie ciągiem przedziałów otwartych ma skończone podkrycie.
  • Twierdzenie Heinego-Borela dla całkowicie ograniczonych rozłącznych przestrzeni metrycznych (gdzie pokrycie jest sekwencją otwartych kul).
  • Ciągła funkcja rzeczywista na zamkniętym przedziale jednostkowym (lub na dowolnej zwartej, separowalnej przestrzeni metrycznej, jak wyżej) jest ograniczona (lub: ograniczona i osiąga swoje granice).
  • Ciągła funkcja rzeczywista na domkniętym przedziale jednostkowym może być równomiernie aproksymowana wielomianami (ze współczynnikami wymiernymi).
  • Ciągła funkcja rzeczywista na zamkniętym przedziale jednostkowym jest jednostajnie ciągła.
  • Ciągła funkcja rzeczywista na zamkniętym przedziale jednostkowym jest całkowalna Riemanna .
  • Twierdzenie Brouwera o punkcie stałym (dla funkcji ciągłych na iloczynie skończonym kopii przedziału domkniętej jednostki).
  • Twierdzenie Hahna-Banacha o charakterze separowalnym w postaci: ograniczona forma liniowa na podprzestrzeni separowalnej przestrzeni Banacha rozciąga się na ograniczoną formę liniową na całej przestrzeni.
  • Krzywa twierdzenie Jordana
  • Twierdzenie o zupełności Gödla (dla języka policzalnego).
  • Determinacja dla otwartych (lub nawet sklonowanych) gier na {0,1} długości ω.
  • Każdy policzalny pierścień przemienny ma pierwotny ideał .
  • Porządkowalna jest każda policzalna formalnie rzeczywista dziedzina.
  • Jednoznaczność domknięcia algebraicznego (dla ciała przeliczalnego).

Rozumienie arytmetyczne ACA 0

ACA 0 to RCA 0 plus schemat rozumienia formuł arytmetycznych (który jest czasami nazywany „aksjomatem rozumienia arytmetycznego”). Oznacza to, że ACA 0 pozwala nam na utworzenie zbioru liczb naturalnych spełniającego arbitralną formułę arytmetyczną (jedną bez powiązanych zmiennych zbioru, chociaż prawdopodobnie zawierającą parametry zbioru). Właściwie wystarczy dodać do RCA 0 schemat rozumienia dla formuł Σ 1 w celu uzyskania pełnego rozumienia arytmetycznego.

Część pierwszego rzędu ACA 0 to dokładnie arytmetyka pierwszego rzędu Peano; ACA 0 jest konserwatywnym rozszerzeniem arytmetyki pierwszego rzędu Peano. Te dwa systemy są dowodnie (w słabym systemie) równospójne. ACA 0 można traktować jako szkielet matematyki predykatywnej , chociaż istnieją twierdzenia dowodzenia predykatywne, których nie można udowodnić w ACA 0 . Większość podstawowych wyników dotyczących liczb naturalnych i wielu innych twierdzeń matematycznych można udowodnić w tym systemie.

Jednym ze sposobów stwierdzenia, że ​​ACA 0 jest silniejsza niż WKL 0, jest przedstawienie modelu WKL 0 , który nie zawiera wszystkich zbiorów arytmetycznych. W rzeczywistości możliwe jest zbudowanie modelu WKL 0 składającego się wyłącznie ze zbiorów niskich przy użyciu twierdzenia o niskiej podstawie , ponieważ zbiory dolne w stosunku do zbiorów dolnych są niskie.

Następujące twierdzenia są równoważne ACA 0 nad RCA 0 :

  • Sekwencyjna kompletność liczb rzeczywistych (każdy ograniczony ciąg rosnący liczb rzeczywistych ma granicę).
  • Twierdzenie Bolzano–Weierstrassa .
  • Twierdzenie Ascoliego : każdy ograniczony równociągły ciąg funkcji rzeczywistych na przedziale jednostkowym ma jednostajnie zbieżny podciąg.
  • Każdy policzalny pierścień przemienny ma maksymalny ideał .
  • Każda policzalna przestrzeń wektorowa nad wymiernymi (lub nad jakimkolwiek polem policzalnym) ma swoją podstawę.
  • Każde pole policzalne ma podstawę transcendencji .
  • Lemat Kőniga (dla dowolnych, skończenie rozgałęzionych drzew, w przeciwieństwie do słabej wersji opisanej powyżej).
  • Różne twierdzenia w kombinatoryce, takie jak niektóre formy twierdzenia Ramseya .

Rekurencja arytmetyczna transskończona ATR 0

System ATR 0 dodaje do ACA 0 aksjomat, który stwierdza nieformalnie, że dowolny funkcjonał arytmetyczny (oznaczający dowolny wzór arytmetyczny ze zmienną o liczbie wolnej n i zmienną klasy swobodnej X , widziany jako operator dobierający X do zbioru n spełniającego wzór) można iterować w nieskończoność wzdłuż dowolnego policzalnego uporządkowania, zaczynając od dowolnego zestawu. ATR 0 jest równoważne z ACA 0 zasadzie Σ1
1separacja. ATR 0 jest bezpredykatywny i ma teoretyczną liczbę porządkową dowodu , nadrzędną względem systemów predykatywnych.

ATR 0 dowodzi zgodności ACA 0 , a zatem według twierdzenia Gödla jest ściśle silniejsze.

Następujące twierdzenia są równoważne ATR 0 nad RCA 0 :

Π1
1 zrozumienie1
1-CA 0

Π1
1-CA 0 jest silniejszy niż arytmetyczna rekursja transskończona i jest w pełni bezmyślna. Składa się z RCA 0 plus schemat rozumienia dla Π1
1 formuły.

W pewnym sensie Π1
1-CA 0 rozumienie jest do arytmetycznej rekursji nadskończonej (Σ1
1separacja) jak ACA 0 to słaby lemat Kőniga (Σ0
1separacja). Jest to równoważne kilku twierdzeniom opisowej teorii mnogości, których dowody posługują się argumentami silnie implikacyjnymi; ta równoważność pokazuje, że te nieprzydatne argumenty nie mogą być usunięte.

Następujące twierdzenia są równoważne Π1
1-CA 0 przez RCA 0 :

  • Twierdzenie Cantora-Bendixsona (każdy domknięty zbiór liczb rzeczywistych jest połączeniem zbioru doskonałego i zbioru przeliczalnego).
  • Każda policzalna grupa abelowa jest bezpośrednią sumą grupy podzielnej i grupy zredukowanej.

Dodatkowe systemy

  • Można zdefiniować systemy słabsze niż rozumienie rekurencyjne. Słaby system RCA*
    0    składa się z elementarnej funkcji arytmetycznej EFA (podstawowe aksjomaty plus Δ0
    0     indukcja w języku wzbogaconym z operacją wykładniczą) plus Δ0
    1    zrozumienie. Ponad RCA*
    0    , rekurencyjne rozumienie zdefiniowane wcześniej (tzn. z Σ0
    1    indukcja) jest równoważne stwierdzeniu, że wielomian (na polu przeliczalnym) ma tylko skończenie wiele pierwiastków oraz twierdzeniu klasyfikacyjnemu dla skończenie generowanych grup abelowych. System RCA*
    0    ma ten sam dowód teoretyczna liczba porządkowa ω 3 co EFA i jest konserwatywna względem EFA dla Π0
    2     zdania.
  • Słabe Słabe Lemat Kőniga to stwierdzenie, że poddrzewo nieskończonego drzewa binarnego, które nie ma nieskończonych ścieżek, ma asymptotycznie zanikającą proporcję liści o długości n (z jednorodnym oszacowaniem, ile liści o długości n istnieje). Równoważnym sformułowaniem jest to, że każdy podzbiór przestrzeni Cantora, który ma miarę dodatnią, jest niepusty (nie można tego udowodnić w RCA 0 ). WWKL 0 jest uzyskiwany przez przyłączenie tego aksjomatu do RCA 0 . Jest to równoznaczne ze stwierdzeniem, że jeżeli jednostkowy przedział rzeczywisty jest objęty ciągiem przedziałów, to suma ich długości wynosi co najmniej jeden. Teoria modelowa WWKL 0 jest ściśle powiązana z teorią ciągów algorytmicznie losowych . W szczególności ω-model RCA 0 spełnia słaby słaby lemat Kőniga wtedy i tylko wtedy, gdy dla każdego zbioru X istnieje zbiór Y, który jest 1-losowy względem X .
  • DNR (skrót od „diagonally non-recursive”) dodaje do RCA 0 aksjomat potwierdzający istnienie funkcji nierekurencyjnej po przekątnej względem każdego zestawu. Oznacza to, że DNR stwierdza, że dla dowolnej zadanej A istnieje całkowity funkcji f , że dla wszystkich e e p częściowego funkcji rekurencyjnej z oracle A nie jest równa f . DNR jest ściśle słabszy niż WWKL (Lempp et al. , 2004).
  • Δ1
    1    -rozumienie jest pod pewnymi względami analogiczne do arytmetycznej rekurencji pozaskończonej, tak jak rozumienie rekurencyjne jest do słabego lematu Kőniga. Ma zbiory hiperarytmetyczne jako minimalny ω-model. Arytmetyczna rekurencja transskończona dowodzi Δ1
    1    -rozumienie, ale nie na odwrót.
  • Σ1
    1    -wybór jest stwierdzeniem, że jeśli η ( n , X ) jest Σ1
    1    formuła taka, że ​​dla każdego n istnieje X spełniające η, to istnieje ciąg zbiorów X n taki, że η ( n , X n ) zachodzi dla każdego n . Σ1
    1    -choice ma również zbiory hiperarytmetyczne jako minimalny model ω. Arytmetyczna rekurencja transskończona dowodzi Σ1
    1    -wybór, ale nie na odwrót.
  • HBU (skrót od „uncountable Heine-Borel”) wyraża zwartość (otwartej pokrywy) przedziału jednostkowego, obejmującego niepoliczalne pokrywy . Ten ostatni aspekt HBU sprawia, że ​​można go wyrazić tylko w języku arytmetyki trzeciego rzędu . Twierdzenie Cousina (1895) implikuje HBU, a twierdzenia te wykorzystują to samo pojęcie osłony ze względu na Cousina i Lindelöfa . HBU jest trudny do udowodnienia: pod względem zwykłej hierarchii aksjomatów rozumienia, dowód HBU wymaga pełnej arytmetyki drugiego rzędu.
  • Twierdzenie Ramseya dla grafów nieskończonych nie należy do jednego z pięciu wielkich podsystemów i istnieje wiele innych słabszych wariantów o różnej sile dowodu.

ω-modele i β-modele

Model ω w oznacza zbiór nieujemnych liczb całkowitych (lub skończonych liczb porządkowych). Model ω to model fragmentu arytmetyki drugiego rzędu, którego część pierwszego rzędu jest standardowym modelem arytmetyki Peano, ale której część drugiego rzędu może być niestandardowa. Dokładniej, model ω jest dany przez wybór S ⊆2 ω podzbiorów ω. Zmienne pierwszego rzędu są interpretowane w zwykły sposób jako elementy ω, a +, × mają swoje zwykłe znaczenie, podczas gdy zmienne drugiego rzędu są interpretowane jako elementy S . Istnieje standardowy model ω, w którym po prostu bierze się S składające się ze wszystkich podzbiorów liczb całkowitych. Istnieją jednak również inne modele ω; na przykład RCA 0 ma minimalny model ω, w którym S składa się z rekurencyjnych podzbiorów ω.

Model β to model ω równoważny standardowemu modelowi ω dla Π1
1 i Σ1
1 zdania (z parametrami).

Przydatne są również modele inne niż ω, zwłaszcza w dowodach twierdzeń konserwatorskich.

Zobacz też

Uwagi

Bibliografia

  • Ambos-Szpiedzy, K.; Kjos-Hanssen, B.; Lempp, S.; Slaman, TA (2004), „Porównanie DNR i WWKL”, Journal of Symbolic Logic , 69 (4): 1089, arXiv : 1408.2281 , doi : 10.2178/jsl/1102022212 .
  • Friedman, Harvey (1975), „Niektóre systemy arytmetyki drugiego rzędu i ich zastosowanie”, Proceedings of the International Congress of Mathematicians (Vancouver, BC, 1974), tom. 1 , Kanada. Matematyka. Kongres, Montreal, Que., s. 235-242, MR  0429508
  • Friedman, Harvey (1976), Baldwin, John; Marcina, DA ; Soare, RI ; Tait, WW (red.), "Systemy drugiego rzędu arytmetyki z ograniczoną indukcją, I, II", Zgromadzenie Stowarzyszenia Symbolic Logic, The Journal of Symbolic Logic , 41 (2): 557-559, doi : 10,2307 /2272259 , JSTOR  2272259
  • Hirschfeldt, Denis R. (2014), Slicing the Truth , Seria notatek wykładowych Instytutu Nauk Matematycznych, National University of Singapore, 28 , World Scientific
  • Hunter, James (2008), Topologia odwrócona (PDF) (praca doktorska), University of Wisconsin-Madison
  • Kohlenbach, Ulrich (2005), "matematyka odwrotna wyższego rzędu" , w Simpson, Stephen G (red.), Matematyka odwrotna wyższego rzędu, Matematyka odwrotna 2001 (PDF) , Notatki z wykładu z logiki , Cambridge University Press , s. 281-295 , CiteSeerX  10.1.1.643.551 , doi : 10.1017/9781316755846.018 , ISBN 9781316755846
  • Normann, Dag; Sanders, Sam (2018), „O matematycznym i fundamentalnym znaczeniu tego, co niepoliczalne”, Journal of Mathematical Logic , 19 : 1950001, arXiv : 1711.08939 , doi : 10.1142/S0219061319500016
  • Simpson, Stephen G. (2009), Podsystemy arytmetyki drugiego rzędu , Perspektywy w logice (2nd ed.), Cambridge University Press , doi : 10.1017/CBO9780511581007 , ISBN 978-0-521-88439-6, MR  2517689
  • Stillwell, John (2018), Reverse Mathematics, dowody od środka , Princeton University Press , ISBN 978-0-691-17717-5
  • Solomon, Reed (1999), „Grupy uporządkowane: studium przypadku w matematyce odwrotnej”, The Bulletin of Symbolic Logic , 5 (1): 45–58, CiteSeerX  10.1.1.364.9553 , doi : 10.2307/421140 , ISSN  1079- 8986 , JSTOR  421140 , MR  1681895

Zewnętrzne linki