Odwrócona matematyka

Odwrotna matematyka to program z logiki matematycznej , który ma na celu określenie, które aksjomaty są wymagane do udowodnienia twierdzeń matematyki. Jego metodę definiowania można krótko opisać jako „cofanie się od twierdzeń do aksjomatów ”, w przeciwieństwie do zwykłej praktyki matematycznej polegającej na wyprowadzaniu twierdzeń z aksjomatów. Można to pojmować jako wyodrębnienie niezbędnych z warunków wystarczających .

Odwrotny program matematyczny był zapowiedzią wyników teorii mnogości, takich jak klasyczne twierdzenie, że aksjomat wyboru i lemat Zorna są równoważne teorii mnogości ZF . Celem matematyki odwrotnej jest jednak badanie możliwych aksjomatów zwykłych twierdzeń matematyki, a nie możliwych aksjomatów teorii mnogości.

Matematyka odwrotna jest zwykle przeprowadzana przy użyciu podsystemów arytmetyki drugiego rzędu , gdzie wiele jej definicji i metod jest inspirowanych wcześniejszymi pracami z zakresu analizy konstruktywnej i teorii dowodu . Zastosowanie arytmetyki drugiego rzędu pozwala również na zastosowanie wielu technik z teorii rekurencji ; wiele wyników matematyki odwrotnej ma odpowiednie wyniki w analizie obliczeniowej . W wyższego rzędu nacisk kładziony jest na podsystemy arytmetyki wyższego rzędu i związany z nimi bogatszy język. ^{[ potrzebne wyjaśnienie ]}

Program został założony przez Harveya Friedmana ( 1975 , 1976 ) i wprowadzony przez Steve'a Simpsona . Standardowym źródłem informacji na ten temat jest Simpson (2009) , natomiast wprowadzeniem dla niespecjalistów jest Stillwell (2018) . Wprowadzenie do matematyki odwrotnej wyższego rzędu, a także artykuł założycielski, to Kohlenbach (2005) .

Ogólne zasady

W matematyce odwróconej zaczyna się od języka ramowego i podstawowej teorii — podstawowego systemu aksjomatów — który jest zbyt słaby, aby udowodnić większość twierdzeń, którymi można być zainteresowanym, ale wciąż wystarczająco potężny, aby opracować definicje niezbędne do sformułowania tych twierdzeń. Na przykład, aby zbadać twierdzenie „Każdy ograniczony ciąg liczb rzeczywistych ma supremum ”, konieczne jest użycie systemu bazowego, który może mówić o liczbach rzeczywistych i ciągach liczb rzeczywistych.

Dla każdego twierdzenia, które można sformułować w systemie podstawowym, ale którego 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 wykazać, że do udowodnienia twierdzenia T potrzebny jest system S , potrzebne są dwa dowody. Pierwszy dowód pokazuje, że T można udowodnić na podstawie S ; jest to zwykły dowód matematyczny wraz z uzasadnieniem , że można go przeprowadzić w układzie S. Drugi dowód, znany jako odwrócenie , pokazuje, że T samo w sobie implikuje S ; dowód ten przeprowadza się w systemie bazowym. Odwrócenie ustala, że żaden system aksjomatów S′ , który rozszerza system podstawowy, nie może być słabszy od S , a jednocześnie dowodzi T.

Zastosowanie arytmetyki drugiego rzędu

Większość badań matematyki odwrotnej koncentruje się na podsystemach arytmetyki drugiego rzędu . Wyniki badań nad matematyką odwrotną wykazały, że słabe podsystemy arytmetyki drugiego rzędu wystarczą do sformalizowania prawie całej matematyki na poziomie licencjackim. W arytmetyce drugiego rzędu wszystkie obiekty można przedstawić albo jako liczby naturalne , albo jako zbiory liczb naturalnych. Na przykład, aby udowodnić twierdzenia o liczbach rzeczywistych, liczby rzeczywiste można przedstawić jako ciągi liczb wymiernych Cauchy'ego , z których każdy można przedstawić 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 . Schemat taki stwierdza, że istnieje dowolny zbiór liczb naturalnych możliwych do zdefiniowania za pomocą wzoru 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 matematyka odwrócona nie jest przeprowadzana przy użyciu teorii mnogości jako systemu podstawowego, jest to, że język teorii mnogości jest zbyt wyrazisty. Niezwykle złożone zbiory liczb naturalnych można zdefiniować za pomocą prostych wzorów w języku teorii mnogości (którą można określić ilościowo na dowolnych zbiorach). W kontekście arytmetyki drugiego rzędu wyniki takie jak twierdzenie Posta ustanawiają ścisły związek między złożonością wzoru a (nie)obliczalnością zbioru, który definiuje.

Innym skutkiem stosowania arytmetyki drugiego rzędu jest potrzeba ograniczenia ogólnych twierdzeń matematycznych do form, które można wyrazić w ramach arytmetyki. Na przykład arytmetyka drugiego rzędu może wyrazić zasadę „Każda przeliczalna przestrzeń wektorowa ma bazę”, ale nie może wyrazić zasady „Każda przestrzeń wektorowa ma bazę”. W praktyce oznacza to, że twierdzenia algebry i kombinatoryki ograniczają się do struktur przeliczalnych, podczas gdy twierdzenia analizy i topologii ograniczają się do przestrzeni rozłącznych ₀ . Wiele zasad, które implikują aksjomat wyboru w ich ogólnej formie (takich jak „Każda przestrzeń wektorowa ma bazę”) można udowodnić w słabych podsystemach arytmetyki drugiego rzędu, gdy są one ograniczone. Na przykład „każde ciało ma domknięcie algebraiczne” nie jest możliwe do udowodnienia w teorii mnogości ZF, ale ograniczona forma „każde ciało przeliczalne ma domknięcie algebraiczne” jest możliwa do udowodnienia w RCA , najsłabszym systemie zwykle stosowanym w matematyce odwrotnej.

Stosowanie arytmetyki wyższego rzędu

Niedawny nurt badań matematyki odwrotnej wyższego rzędu , zainicjowany przez Ulricha Kohlenbacha w 2005 roku, 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 ciągi binarne na ciągi binarne i która również spełnia zwykłą definicję ciągłości „epsilon-delta”.

Matematyka odwrotna wyższego rzędu obejmuje wersje schematów rozumienia wyższego rzędu (drugiego rzędu). Taki aksjomat wyższego rzędu stwierdza istnienie funkcjonału decydującego 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 . Odpowiedniki wyższego rzędu głównych podsystemów arytmetyki drugiego rzędu generalnie dowodzą tych samych zdań drugiego rzędu (lub dużego podzbioru), co 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 , aż do języka.

₀ Jak zauważono w poprzednim akapicie, aksjomaty rozumienia drugiego rzędu łatwo można uogólnić na ramy wyższego rzędu. Jednak twierdzenia wyrażające zwartość przestrzeni podstawowych zachowują się zupełnie inaczej w arytmetyce drugiego i wyższego rzędu: z jednej strony, gdy ograniczają się do przeliczalnych pokryw/języka arytmetyki drugiego rzędu, zwartość przedziału jednostkowego można udowodnić w WKL z następna sekcja. Z drugiej strony, biorąc pod uwagę niezliczone pokrycia/język arytmetyki wyższego rzędu, zwartość przedziału jednostkowego można udowodnić jedynie na podstawie (pełnej) arytmetyki drugiego rzędu. Inne lematy obejmujące (np. za sprawą Lindelöfa , Vitali , Besicovitch itp.) wykazują takie samo zachowanie, a wiele podstawowych właściwości całki cechowania jest równoważnych zwartości podstawowej przestrzeni.

Pięć wielkich podsystemów arytmetyki drugiego rzędu

Arytmetyka drugiego rzędu to formalna teoria liczb naturalnych i zbiorów liczb naturalnych. Wiele obiektów matematycznych, takich jak przeliczalne pierścienie , grupy i ciała , a także punkty w efektywnych przestrzeniach polskich , można przedstawić w postaci zbiorów 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 matematyki odwrotnej pokazuje, że określone twierdzenie matematyczne T jest równoważne określonemu podsystemowi S arytmetyki drugiego rzędu w stosunku do słabszego podsystemu B. Ten słabszy system B jest znany jako system podstawowy wyniku; aby odwrotny wynik matematyczny miał znaczenie, system ten sam nie może być w stanie udowodnić twierdzenia matematycznego T . ^{[ wymagany cytat ]}

₀₀₀₀₀ Simpson (2009) opisuje pięć szczególnych podsystemów arytmetyki drugiego rzędu, które nazywa Wielką Piątką , które często występują w matematyce odwrotnej. W kolejności rosnącej siły systemy te nazywane są inicjalizacjami RCA , WKL , ACA , ATR i
^Π11_- CA .

Poniższa tabela podsumowuje systemy „wielkiej piątki” i zawiera listę systemów odpowiedników w arytmetyce wyższego rzędu. Te ostatnie generalnie dowodzą tych samych zdań drugiego rzędu (lub dużego podzbioru), co oryginalne systemy drugiego rzędu.

Podsystem	Oznacza	Porządkowy	Odpowiada mniej więcej	Uwagi	Odpowiednik wyższego rzędu
RCA₀	Aksjomat rozumienia rekurencyjnego	ω ^ω	Matematyka konstruktywna ( biskup )	Podstawowa teoria	RCA $ω 0$ ; dowodzi tych samych zdań drugiego rzędu, co RCA ₀
WKL₀	Słaby lemat Kőniga	ω ^ω	Redukcjonizm finitystyczny ( Hilbert )	₀ Konserwatywny w stosunku do PRA (odpowiednio RCA ) dla $Π 02$ (odpowiednio $Π 11$ ) zdań	Wentylator funkcjonalny; oblicza moduł jednolitej ciągłości dla funkcji ciągłych ${\ displaystyle 2 ^ {\ mathbb {N}}}$
ACTA₀	Aksjomat rozumienia arytmetycznego	ε₀	Predykatywizm ( Weyl , Feferman )	Konserwatywny względem arytmetyki Peano dla zdań arytmetycznych	Funkcjonał „skoku Turinga” $mathbb {R}}$ $displaystyle$ \
ATR₀	Arytmetyczna rekurencja pozaskończona	Γ₀	Redukcjonizm predykatywny (Friedman, Simpson)	Konserwatywny w stosunku do systemu Fefermana IR dla $Π 11$ zdań	₀ Funkcjonalność „rekurencji pozaskończonej” daje zbiór, o którym twierdzi ATR .
Π ¹₁ -CA ₀	Π ¹₁ aksjomat zrozumienia	₀ Ψ (Ω _ω )	Impredykatywizm		Funkcjonał Suslina $formułach$ o $(. parametrów$ drugiego rzędu)

₀₀ Indeks dolny w tych nazwach oznacza, że program indukcyjny został ograniczony do pełnego programu indukcyjnego drugiego rzędu. Na przykład ACA zawiera aksjomat indukcyjny $(0 \in X \land \forall n (n \in X \to n + 1 \in X)) \to \forall n n \in X$ . To, wraz z pełnym zrozumieniem aksjomatu arytmetyki drugiego rzędu, implikuje pełny schemat indukcji drugiego rzędu dany przez uniwersalne domknięcie ₀₀ $(φ (0) \land \forall n (φ (n) \to φ (n +1))) \to \forall n φ (n)$ dla dowolnej formuły drugiego rzędu φ . Jednak ACA nie ma aksjomatu pełnego zrozumienia, a indeks dolny przypomina, że nie ma również pełnego schematu indukcji drugiego rzędu. To ograniczenie jest ważne: systemy z ograniczoną indukcją mają znacznie niższe liczby porządkowe dowodowo-teoretyczne niż systemy z pełnym schematem indukcji drugiego rzędu.

Podstawowy system RCA₀

₀ RCA jest fragmentem arytmetyki drugiego rzędu, którego aksjomaty są aksjomatami arytmetyki Robinsona , indukcją dla wzorów Σ ⁰
₁ i zrozumieniem dla wzorów Δ ⁰
₁ .

₀₀₀₀ Podsystem RCA jest najczęściej używanym systemem podstawowym w matematyce odwrotnej. Inicjały „RCA” oznaczają „aksjomat zrozumienia rekurencyjnego”, gdzie „rekurencyjny” oznacza „obliczalny”, jak w przypadku funkcji rekurencyjnej . Nazwa ta jest używana, ponieważ RCA nieformalnie odpowiada „matematyce obliczeniowej”. W szczególności każdy zbiór liczb naturalnych, którego istnienie można udowodnić w RCA, jest obliczalny, a zatem żadne twierdzenie, które sugeruje, że istnieją zbiory nieprzeliczalne, nie jest możliwe do udowodnienia w RCA . W tym zakresie RCA ₀ jest systemem konstruktywnym, choć nie spełnia wymogów programu konstruktywizmu, gdyż jest teorią logiki klasycznej uwzględniającą prawo wyłączonego środka .

₀₀ Pomimo swojej pozornej słabości (niedowodzenia istnienia żadnych nieobliczalnych zbiorów), RCA 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 odwrotnego przedsięwzięcia matematycznego, ponieważ można je już udowodnić w systemie podstawowym. Klasyczne twierdzenia, które można udowodnić w RCA, obejmują:

Podstawowe właściwości liczb naturalnych, całkowitych i wymiernych (np. to, że te ostatnie tworzą pole uporządkowane ).
Podstawowe właściwości liczb rzeczywistych (liczby rzeczywiste są polem uporządkowanym Archimedesa ; każdy zagnieżdżony ciąg zamkniętych przedziałów , których długość dąży do zera, ma w swoim przecięciu pojedynczy punkt; liczb rzeczywistych nie można przeliczyć).
Twierdzenie kategorii Baire'a dla zupełnej rozdzielnej przestrzeni metrycznej (warunek rozdzielności jest konieczny, aby w ogóle sformułować twierdzenie w języku arytmetyki drugiego rzędu).
Twierdzenie o wartości pośredniej o ciągłych funkcjach rzeczywistych.
Banacha – Steinhausa dla ciągu ciągłych operatorów liniowych na rozdzielnych przestrzeniach Banacha.
Słaba wersja twierdzenia Gödla o zupełności (dla zbioru zdań w języku przeliczalnym, który jest już zamknięty w konsekwencji).
Istnienie domknięcia algebraicznego ciała przeliczalnego (ale nie jego jednoznaczność).
Istnienie i jednoznaczność domknięcia rzeczywistego pola przeliczalnego uporządkowanego.

₀₀ Część pierwszego rzędu RCA (twierdzenia układu nie zawierające żadnych zmiennych zbiorczych) to zbiór twierdzeń arytmetyki Peano pierwszego rzędu z indukcją ograniczoną do wzorów Σ ⁰
₁ . Jest ona w sposób możliwy do udowodnienia spójna, podobnie jak RCA , w pełnej arytmetyce Peano pierwszego rzędu.

Słaby lemat Kőniga WKL₀

₀₀₀ Podsystem WKL składa się z RCA oraz słabej formy lematu Kőniga , a mianowicie stwierdzenia, ż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ę. Twierdzenie to, znane jako słaby lemat Kőniga , jest łatwe do sformułowania w języku arytmetyki drugiego rzędu. WKL można również zdefiniować jako zasadę separacji Σ ⁰
₁ (biorąc pod uwagę dwa wyłączne wzory Σ ⁰
₁ wolnej zmiennej n , istnieje klasa zawierająca wszystkie n ₀₀ spełniający jedno i nie spełniający drugiego). Kiedy ten aksjomat zostanie dodany do RCA , powstały podsystem zostanie nazwany WKL . Podobnego rozróżnienia między poszczególnymi aksjomatami z jednej strony a podsystemami zawierającymi podstawowe aksjomaty i indukcję z drugiej strony 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 udowodnić w klasycznej teorii mnogości Zermelo – Fraenkla bez aksjomatu wyboru). Nie jest to konstruktywnie ważne w pewnym sensie słowa „konstruktywny”.

₀₀₀₀ Aby pokazać, że WKL jest rzeczywiście silniejszy niż (nie do udowodnienia w) RCA , wystarczy wykazać twierdzenie WKL , które implikuje, że istnieją zbiory nieprzeliczalne. To nie jest trudne; WKL implikuje istnienie zbiorów oddzielających dla skutecznie nierozłącznych, rekurencyjnie przeliczalnych zbiorów.

₀₀₀₀ Okazuje się, że RCA i WKL mają tę samą część pierwszego rzędu, co oznacza, że dowodzą tych samych zdań pierwszego rzędu. WKL może jednak udowodnić dużą liczbę klasycznych wyników matematycznych, które nie wynikają z RCA . Wyniki te nie dają się wyrazić jako stwierdzenia pierwszego rzędu, ale można je wyrazić jako stwierdzenia drugiego rzędu.

₀₀ Poniższe wyniki są równoważne słabemu lematowi Kőniga, a tym samym WKL nad RCA :

Heinego -Borela dla rzeczywistego przedziału jednostkowego domkniętego w następującym sensie: każde pokrycie ciągiem przedziałów otwartych ma skończone podkrycie.
Twierdzenie Heinego-Borela dla całkowitych, całkowicie ograniczonych, rozdzielnych przestrzeni metrycznych (gdzie pokrycie jest sekwencją otwartych kul).
Ciągła funkcja rzeczywista na zamkniętym przedziale jednostkowym (lub na dowolnej zwartej rozdzielnej przestrzeni metrycznej, jak powyżej) jest ograniczona (lub: ograniczona i osiąga swoje granice).
Ciągłą funkcję rzeczywistą na zamkniętym przedziale jednostkowym można równomiernie aproksymować wielomianami (ze współczynnikami wymiernymi).
Ciągła funkcja rzeczywista na zamkniętym przedziale jednostkowym jest równomiernie ciągła.
Ciągła funkcja rzeczywista na zamkniętym przedziale jednostkowym jest całkowalna Riemanna .
Brouwera o punkcie stałym (dla funkcji ciągłych na skończonym iloczynie kopii zamkniętego przedziału jednostkowego).
Rozłączne twierdzenie Hahna – Banacha w postaci: ograniczona postać liniowa na podprzestrzeni rozdzielnej przestrzeni Banacha rozciąga się na ograniczoną postać liniową na całej przestrzeni.
Twierdzenie o krzywej Jordana
Twierdzenie Gödla o zupełności (dla języka przeliczalnego).
Określalność dla gier otwartych (lub nawet zamkniętych) na {0,1} długości ω.
Każdy przeliczalny pierścień przemienny ma ideał pierwszy .
Każde przeliczalne formalnie rzeczywiste pole jest uporządkowane.
Jedyność domknięcia algebraicznego (dla ciała przeliczalnego).

Rozumienie arytmetyczne ACA₀

₀₀₀₀ ACA to RCA plus schemat rozumienia formuł arytmetycznych (który jest czasami nazywany „aksjomatem rozumienia arytmetycznego”). Oznacza to, że ACA pozwala nam utworzyć zbiór liczb naturalnych odpowiadający dowolnej formule arytmetycznej (takiej, która nie ma żadnych powiązanych zmiennych zestawu, chociaż ewentualnie zawiera ustawione parametry). Właściwie wystarczy dodać do RCA schemat rozumienia dla wzorów Σ ₁ , aby uzyskać pełne zrozumienie arytmetyczne.

₀₀₀₀ Część pierwszego rzędu ACA jest dokładnie arytmetyką Peano pierwszego rzędu; ACA jest konserwatywnym rozszerzeniem arytmetyki Peano pierwszego rzędu. Te dwa systemy są w sposób możliwy do udowodnienia (w systemie słabym) równoważne. ACA można traktować jako ramy matematyki predykatywnej , chociaż istnieją twierdzenia predykatywnie udowodnialne, których w ACA nie da się udowodnić . Większość podstawowych wyników dotyczących liczb naturalnych i wiele innych twierdzeń matematycznych można udowodnić w tym systemie.

₀₀₀₀ Jednym ze sposobów sprawdzenia, czy ACA jest silniejszy niż WKL, jest pokazanie modelu WKL , który nie zawiera wszystkich zbiorów arytmetycznych. W rzeczywistości możliwe jest zbudowanie modelu WKL składającego się wyłącznie z niskich zbiorów przy użyciu twierdzenia o niskiej podstawie , ponieważ niskie zbiory w porównaniu z niskimi zbiorami są niskie.

₀₀ Następujące twierdzenia są równoważne ACA zamiast RCA :

Kompletność sekwencyjna liczb rzeczywistych (każdy ograniczony, rosnący ciąg liczb rzeczywistych ma granicę).
Bolzano –Weierstrassa .
Twierdzenie Ascoliego : każdy ograniczony, równociągły ciąg funkcji rzeczywistych na przedziale jednostkowym ma podciąg jednostajnie zbieżny.
Każdy przeliczalny pierścień przemienny ma ideał maksymalny .
Każda przeliczalna przestrzeń wektorowa nad wymiernymi (lub nad dowolnym ciałem przeliczalnym) ma bazę.
Każde ciało przeliczalne ma bazę transcendencji .
Lemat Kőniga (dla dowolnych, skończenie rozgałęzionych drzew, w przeciwieństwie do opisanej powyżej słabej wersji).
Różne twierdzenia kombinatoryki, takie jak pewne formy twierdzenia Ramseya .

Arytmetyczna rekurencja pozaskończona ATR₀

₀₀₀₀₀ System ATR dodaje do ACA aksjomat, który nieformalnie stwierdza, że dowolny funkcjonał arytmetyczny (czyli dowolny wzór arytmetyczny z wolną zmienną liczbową n i wolną zmienną klasową X , postrzegany jako operator prowadzący X do zbioru n spełniającego formułę) można iterować w nieskończoność wzdłuż dowolnego policzalnego uporządkowania studni , zaczynając od dowolnego zestawu. ATR jest w stosunku do ACA odpowiednikiem zasady separacji Σ
¹₁ . ATR jest impredykatywny i ma teoria dowodu $,$ supremum systemów predykatywnych.

₀₀ ATR dowodzi spójności ACA , a zatem zgodnie z twierdzeniem Gödla jest ono ściśle silniejsze.

₀₀ Następujące twierdzenia są równoważne ATR zamiast RCA :

Dowolne dwie policzalne kolejności odwiertów są porównywalne. Oznacza to, że są izomorficzne lub jeden jest izomorficzny z odpowiednim początkowym segmentem drugiego.
Twierdzenie Ulma dla przeliczalnych zredukowanych grup abelowych.
Twierdzenie o mnogościach doskonałych , które stwierdza, że każdy nieprzeliczalny podzbiór domknięty zupełnej rozdzielnej przestrzeni metrycznej zawiera zbiór doskonały domknięty.
Twierdzenie Lusina o separacji (zasadniczo separacja Σ
¹₁ ).
Określalność zbiorów otwartych w przestrzeni Baire'a .

Π
¹₁ zrozumienie Π
¹₁ -CA ₀

₀₀ Π
¹₁ -CA jest silniejsze niż arytmetyczna rekurencja pozaskończona i jest w pełni impredykatywne. Składa się z RCA i schematu rozumienia dla wzorów Π
¹₁ .

₀₀ W pewnym sensie zrozumienie Π
¹₁ -CA ma się do arytmetycznej rekurencji pozaskończonej (oddzielenie Σ
¹₁ ), tak jak ACA do słabego lematu Kőniga (oddzielenie Σ ⁰
₁ ). Jest to odpowiednik kilku twierdzeń opisowej teorii mnogości, których dowody wykorzystują argumenty silnie impredykatywne; ta równoważność pokazuje, że tych impredykatywnych argumentów nie można usunąć.

₀₀ Poniższe twierdzenia są równoważne Π
¹₁ -CA przez RCA :

Cantora – Bendixsona (każdy domknięty zbiór liczb rzeczywistych jest sumą zbioru doskonałego i przeliczalnego).
Dychotomia Silvera (każda koanalityczna relacja równoważności ma albo przeliczalnie wiele klas równoważności, albo doskonały zbiór nieporównywalnych)
Każda przeliczalna grupa abelowa jest sumą bezpośrednią grupy podzielnej i grupy zredukowanej.

Dodatkowe systemy

⁰
₀ Można zdefiniować systemy słabsze niż zrozumienie rekurencyjne. Słaby system RCA ^*
₀ składa się z elementarnej arytmetyki funkcji EFA (podstawowe aksjomaty plus Δ indukcja w języku wzbogaconym z działaniem wykładniczym) plus Δ ⁰
₁ zrozumienie. W przypadku RCA ^*
₀ rozumienie rekurencyjne zdefiniowane wcześniej (tj. z indukcją Σ ⁰
₁ ) jest równoważne stwierdzeniu, że wielomian (na ciele przeliczalnym) ma tylko skończenie wiele pierwiastków oraz twierdzeniu o klasyfikacji dla skończenie generowanych grup abelowych. System RCA ^*
₀ ma to samo dowód teoretyczny porządkowy ω ³ jako EFA i jest konserwatywny w stosunku do EFA dla Π ⁰
₂ zdań.
₀₀₀ Słaby Słaby Lemat Kőniga to stwierdzenie, że poddrzewo nieskończonego drzewa binarnego nie mające nieskończonych ścieżek ma asymptotycznie zanikającą proporcję liści na długości n (przy jednolitym oszacowaniu, ile istnieje liści o długości n ). Równoważne sformułowanie jest takie, że każdy podzbiór przestrzeni Cantora, który ma miarę dodatnią, jest niepusty (nie można tego udowodnić w RCA ). WWKL uzyskuje się przez dołączenie tego aksjomatu do RCA . Jest to równoznaczne ze stwierdzeniem, że jeśli rzeczywisty przedział jednostkowy pokrywa się z ciągiem przedziałów, to suma ich długości wynosi co najmniej jeden. Modelowa teoria WWKL ₀₀ jest ściśle powiązana z teorią ciągów algorytmicznie losowych . W szczególności model ω RCA 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 „diagonalnie nierekurencyjny”) dodaje do RCA aksjomat stwierdzający istnienie funkcji nierekurencyjnej po przekątnej w stosunku do każdego zbioru. Oznacza to, że DNR stwierdza, że dla dowolnego zbioru A istnieje funkcja całkowita f taka, że dla wszystkich e częściowa funkcja rekurencyjna z wyrocznią A nie jest równa f . DNR jest zdecydowanie słabszy niż WWKL (Lempp i in. , 2004).
Δ
¹₁ -rozumienie jest w pewnym sensie analogiczne do arytmetycznej rekurencji pozaskończonej, tak jak zrozumienie rekurencyjne jest do słabego lematu Kőniga. Ma zbiory hiperarytmetyczne jako minimalny model ω. Arytmetyczna rekurencja pozaskończona dowodzi Δ
¹₁ -rozumienia, ale nie na odwrót.
Σ
¹₁ -wybór to stwierdzenie, że jeśli η ( n , X ) jest wzorem Σ
¹₁ takim, że dla każdego n istnieje X spełniający η to istnieje ciąg zbiorów X _n taki, że η ( n , X _n ) obowiązuje dla każdego n . Σ
¹₁ -wybór ma również zbiory hiperarytmetyczne jako minimalny model ω. Arytmetyczna rekurencja pozaskończona dowodzi Σ ¹
₁ - wybór, ale nie odwrotnie.
HBU (skrót od „uncountable Heine-Borel”) wyraża (otwartą pokrywę) zwartość przedziału jednostkowego, obejmującą niezliczone pokrywy . Ten ostatni aspekt HBU sprawia, że można go wyrazić jedynie w języku trzeciego rzędu . Twierdzenie Cousina (1895) implikuje HBU, a twierdzenia te wykorzystują to samo pojęcie pokrycia ze względu na Cousina i Lindelöfa . HBU jest trudne do udowodnienia: jeśli chodzi o zwykłą hierarchię aksjomatów zrozumienia, dowód HBU wymaga pełnej arytmetyki drugiego rzędu.
Twierdzenie Ramseya dla grafów nieskończonych nie należy do żadnego z pięciu wielkich podsystemów i istnieje wiele innych słabszych wariantów o różnej sile dowodu.

Silniejsze systemy

₀ Na RCA , rekurencja pozaskończona Π
¹₁ , wyznaczalność ∆ ⁰
₂ i twierdzenie Ramseya ∆
¹₁ są sobie równoważne.

₀ Na RCA , indukcja monotoniczna Σ
¹_{1 , wyznaczalność} Σ ⁰
₂ i twierdzenie Ramseya Σ
¹₁ są sobie równoważne.

Następujące są równoważne:

(schemat) Π
¹₃ konsekwencje Π
¹₂ -CA ₀
₀ RCA + (schemat nad skończonym n ) determinantą na n- tym poziomie hierarchii różnic Σ ⁰
₂ zbiorów
₀ RCA + {τ: τ jest prawdziwym zdaniem S2S }

₀ Zbiór Π
¹₃ konsekwencji arytmetyki drugiego rzędu Z ₂ ma tę samą teorię, co RCA + (schemat na skończonym n ) wyznaczalności na n- tym poziomie hierarchii różnic zbiorów Σ ⁰
₃ .

Modele ω i modele β

ω w modelu ω oznacza zbiór nieujemnych liczb całkowitych (lub skończonych liczb porządkowych). Model ω jest modelem fragmentu arytmetyki drugiego rzędu, którego część pierwszego rzędu jest modelem standardowym arytmetyki Peano, ale którego 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 ω, oraz +, × mają swoje zwykłe znaczenia, natomiast zmienne drugiego rzędu są interpretowane jako elementy S . Istnieje standardowy model ω, w którym po prostu bierze się S ₀ składać się ze wszystkich podzbiorów liczb całkowitych. Istnieją jednak również inne modele ω; na przykład RCA ma minimalny model ω, w którym S składa się z rekurencyjnych podzbiorów ω.

Model β to model ω, który jest zgodny ze standardowym modelem ω w zakresie prawdziwości zdań Π
¹₁ i Σ
¹₁ (z parametrami).

Modele inne niż ω są również przydatne, szczególnie w dowodach twierdzeń zachowania.

Zobacz też

Notatki

Ambos-Spies, K.; Kjos-Hanssen, B.; Lempp, S.; Slaman, TA (2004), „Comparing DNR and WWKL”, Journal of Symbolic Logic , 69 (4): 1089, arXiv : 1408.2281 , doi : 10.2178/jsl/1102022212 , S2CID 17582399 .
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. Congress, Montreal, Que., s. 235–242, MR 0429508
Friedman, Harvey (1976), Baldwin, John; Martin, Da ; Soare, RI ; Tait, WW (red.), „Systemy arytmetyki drugiego rzędu z ograniczoną indukcją, I, II”, Spotkanie Stowarzyszenia Logiki Symbolicznej, The Journal of Symbolic Logic , 41 (2): 557–559, doi : 10.2307 /2272259 , JSTOR 2272259
Hirschfeldt, Denis R. (2014), Krojenie prawdy , Seria notatek z wykładów Instytutu Nauk Matematycznych, National University of Singapore, tom. 28, Świat Naukowy
Hunter, James (2008), Topologia odwrotna (PDF) (praca doktorska), Uniwersytet 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ładów 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 podstawowym znaczeniu niepoliczalnego”, Journal of Mathematical Logic , 19 : 1950001, arXiv : 1711.08939 , doi : 10.1142/S0219061319500016 , S2CID 119120366
Simpson, Stephen G. (2009), Podsystemy arytmetyki drugiego rzędu , Perspectives in Logic (wyd. 2), Cambridge University Press , doi : 10.1017/CBO9780511581007 , ISBN 978-0-521-88439-6 , MR 2517689
Stillwell, John (2018), Reverse Mathematics, dowody od podszewki , 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 , S2CID 508431

Linki zewnętrzne