Nowe Fundamenty - New Foundations

W logice matematycznej , nowe fundamenty ( NF ) jest aksjomat zestaw teorii , poczęty Willard Van Orman Quine jako uproszczenia teorii typów z Principia Mathematica . Quine po raz pierwszy zaproponował NF w artykule z 1937 roku zatytułowanym „ Nowe podstawy logiki matematycznej ”; stąd nazwa. Wiele z tego wpisu dotyczy NFU , ważnego wariantu NF stworzonego przez Jensena (1969) i przedstawionego w Holmes (1998). W 1940 r. i w wersji z 1951 r. Quine wprowadził rozszerzenie NF zwane czasem „logiką matematyczną” lub „ML”, które obejmowało odpowiednie klasy, a takżezestawy .

New Foundations ma zbiór uniwersalny , więc jest to teoria zbiorów nieuzasadniona . To znaczy, jest to aksjomatyczna teoria mnogości, która dopuszcza nieskończone malejące łańcuchy przynależności, takie jak … x n ∈ x n-1 ∈ … ∈ x 2 ∈ x 1 . Unika paradoksu Russella, zezwalając na definiowanie tylko formuł stratyfikowalnych za pomocą aksjomalnego schematu rozumienia . Na przykład x ∈ y jest formułą stratyfikowalną, ale x ∈ x nie.

Teoria typów TST

Prymitywne predykaty Russellowskiej nierozgałęzionej teorii mnogości typów (TST), uproszczonej wersji teorii typów, to równość ( ) i członkostwo ( ). TST ma liniową hierarchię typów: typ 0 składa się z indywiduów nieopisanych w inny sposób. Dla każdej (meta-) liczby naturalnej n obiekty typu n +1 są zbiorami obiektów typu n ; zbiory typu n mają członków typu n -1. Obiekty połączone tożsamością muszą mieć ten sam typ. Poniższe dwie formuły atomowe zwięźle opisują reguły typowania: i . (Teoria mnogości Quine'a ma na celu wyeliminowanie potrzeby stosowania takich indeksów górnych do oznaczania typów).

Aksjomaty TST to:

  • Rozszerzalność : zbiory tego samego (pozytywnego) typu z tymi samymi członkami są równe;
  • Schemat aksjomatu rozumienia, a mianowicie:
Jeśli  jest formułą, to zbiór istnieje.
Innymi słowy, biorąc pod uwagę dowolną formułę , formuła jest aksjomatem, w którym reprezentuje zbiór i nie jest wolna w .

Ta teoria typów jest znacznie mniej skomplikowana niż ta po raz pierwszy przedstawiona w Principia Mathematica , która zawierała typy relacji, których argumenty niekoniecznie były tego samego typu. W 1914 r. Norbert Wiener pokazał, jak zakodować uporządkowaną parę jako zbiór zbiorów, co umożliwia eliminację typów relacji na rzecz opisanej tu liniowej hierarchii zbiorów.

Teoria mnogości chińskich

Aksjomaty i stratyfikacja

Prawidłowo sformułowane formuły New Foundations (NF) są takie same jak poprawnie sformułowane formuły TST, ale z usuniętymi adnotacjami typu. Aksjomaty NF to:

  • Rozszerzalność : dwa obiekty z tymi samymi elementami są tym samym obiektem;
  • Schematu zrozumieniem : Wszystkie przypadki TST Zrozumienia ale z indeksami typu spadła (i bez wprowadzania nowych identyfikacje między zmiennymi).

Zgodnie z konwencją, schemat rozumienia NF jest określony przy użyciu koncepcji formuły warstwowej i nie ma bezpośredniego odniesienia do typów. Wzór mówi się podzielono jeśli istnieje funkcja f kawałków składni liczb naturalnych, na przykład, że dla każdego podstruktura atomowej od mamy F ( y ) = f ( x ) + 1, podczas gdy dla każdego podstruktura atomowej z , mamy f ( x ) = f ( y ). Zrozumienie staje się wtedy:

istnieje dla każdej formuły warstwowej .

Nawet pośrednie odniesienie do typów zawarte w pojęciu stratyfikacji może zostać wyeliminowane. Theodore Hailperin wykazał w 1944 roku, że rozumienie jest równoważne skończonej koniunkcji jego instancji, tak że NF może być skończenie aksjomatyzowane bez żadnego odniesienia do pojęcia typu.

Może się wydawać, że rozumienie napotyka na problemy podobne do tych w naiwnej teorii mnogości , ale tak nie jest. Na przykład istnienie niemożliwej klasy Russella nie jest aksjomatem NF, ponieważ nie można go rozwarstwić.

Zamówiłem parę

Relacje i funkcje są zdefiniowane w TST (oraz w NF i NFU) jako zbiory uporządkowanych par w zwykły sposób. Zwykła definicja pary uporządkowanej, zaproponowana po raz pierwszy przez Kuratowskiego w 1921 roku, ma poważną wadę dla NF i teorii pokrewnych: wynikowa para uporządkowana z konieczności ma typ drugi wyższy niż typ jej argumentów (jej lewa i prawa projekcja ). Stąd dla celów wyznaczenia stratyfikacji funkcja jest o trzy typy wyższa od członków jej pola.

Jeśli można zdefiniować parę w taki sposób, że jej typ jest tego samego typu, co jej argumenty (co skutkuje parą uporządkowaną na poziomie typu), to relacja lub funkcja jest tylko o jeden typ wyższy niż typ członków jego pole. Stąd NF i pokrewne teorie zwykle stosują definicję pary uporządkowanej Quine'a z teorią mnogości , która daje parę uporządkowaną na poziomie typu . Holmes (1998) przyjmuje uporządkowaną parę i jej lewą i prawą projekcję jako prymitywne. Na szczęście to, czy uporządkowana para jest z definicji na poziomie typu, czy z założenia (tj. jest traktowana jako pierwotna), zwykle nie ma znaczenia.

Istnienie pary uporządkowanej na poziomie typu implikuje Nieskończoność , a NFU + Nieskończoność interpretuje NFU + „istnieje para uporządkowana na poziomie typu” (nie są one całkiem tą samą teorią, ale różnice są nieistotne). I odwrotnie, NFU + Infinity + Choice dowodzi istnienia pary uporządkowanej na poziomie typu.

Dopuszczalność użytecznych dużych zestawów

NF (oraz NFU + Infinity + Choice , opisane poniżej i znane jako spójne) pozwalają na konstruowanie dwóch rodzajów zbiorów, których ZFC i jego właściwe rozszerzenia nie pozwalają, ponieważ są "zbyt duże" (niektóre teorie zbiorów dopuszczają te byty pod nagłówkiem odpowiednich klas ):

Skończona aksjomatyzowalność

Nowe Fundamenty mogą być skończone zaksjomatyzowane .

Zamknięcie kartezjańskie

Kategoria, której obiektami są zbiory NF, a strzałkami są funkcjami pomiędzy tymi zbiorami, nie jest domknięta kartezjańsko ; Zamknięcie kartezjańskie może być użyteczną właściwością kategorii zbiorów. Ponieważ w NF brakuje domknięcia kartezjańskiego, nie każda funkcja krzywi się, jak można by się spodziewać intuicyjnie, a NF nie jest toposem .

Problem spójności i związane z nim wyniki cząstkowe

Przez wiele lat nierozstrzygnięty problem z NF polegał na tym, że nie udowodniono jednoznacznie, że jest względnie spójny z jakimkolwiek innym dobrze znanym systemem aksjomatycznym, w którym można modelować arytmetykę. NF obala wybór , a tym samym dowodzi nieskończoności (Specker, 1953). Ale wiadomo również ( Jensen , 1969), że dopuszczenie urelementów (wielu odrębnych obiektów bez elementów) daje NFU, teorię, która jest spójna w stosunku do arytmetyki Peano ; jeśli doda się nieskończoność i wybór, uzyskana teoria ma taką samą siłę spójności jak teoria typów z nieskończonością lub teorią ograniczonego zbioru Zermelo. (NFU odpowiada teorii typów TSTU, gdzie typ 0 ma urelementy, a nie tylko jeden pusty zbiór.) Istnieją inne stosunkowo spójne warianty NF.

NFU jest z grubsza słabszy niż NF, ponieważ w NF zbiorem mocy wszechświata jest sam wszechświat, podczas gdy w NFU zbiór mocy wszechświata może być ściśle mniejszy niż wszechświat (zestaw mocy wszechświata zawiera tylko zestawy, podczas gdy wszechświat może zawierać urelementy). W rzeczywistości tak właśnie jest w przypadku NFU+„Wybór”.

Ernst Specker wykazał, że NF jest równospójny z TST + Amb , gdzie Amb jest schematem aksjomatu typowej niejednoznaczności, który potwierdza dla dowolnej formuły , będąc formułą uzyskaną przez podniesienie indeksu każdego typu o jeden. NF jest również zgodny z teorią TST wzbogaconą o „automorfizm z przesunięciem typu”, operację, która podnosi typ o jeden, mapując każdy typ na następny wyższy typ i zachowuje relacje równości i członkostwa (i która nie może być używana w przypadkach Zrozumienie : jest poza teorią). Te same wyniki dotyczą różnych fragmentów TST w stosunku do odpowiadających im fragmentów NF.

W tym samym roku (1969), w którym Jensen okazał się konsekwentny w NFU, Grishin okazał się konsekwentny. jest fragmentem NF z pełną ekstensjonalnością (bez urelementów) i tymi instancjami Zrozumienia, które mogą być stratyfikowane przy użyciu tylko trzech typów. Teoria ta jest bardzo niezręcznym medium dla matematyki (chociaż były próby złagodzenia tej niezręczności), głównie dlatego, że nie ma oczywistej definicji pary uporządkowanej . Mimo tej niezręczności jest bardzo ciekawy, ponieważ każdy nieskończony model TST ograniczony do trzech typów spełnia Amba . Stąd dla każdego takiego modelu istnieje model z tą samą teorią. Nie dotyczy to czterech typów: jest to ta sama teoria co NF i nie mamy pojęcia, jak uzyskać model TST z ​​czterema typami, w których utrzymuje się Amb .

W 1983 roku Marcel Crabbé udowodnił, że jest spójny z systemem, który nazwał NFI, którego aksjomaty są nieograniczoną ekstensjonalnością i tymi przypadkami rozumienia, w których żadna zmienna nie ma przypisanego typu wyższego niż zestaw, który twierdził, że istnieje. Jest to ograniczenie predykatywności , chociaż NFI nie jest teorią predykatywną: dopuszcza wystarczającą niepredykatywność do zdefiniowania zbioru liczb naturalnych (definiowanego jako przecięcie wszystkich zbiorów indukcyjnych; zauważ, że zbiory indukcyjne skwantyfikowane są tego samego typu co zbiór definiowanych liczb naturalnych). Crabbé omówił również podteorię NFI, w której tylko parametry (zmienne wolne) mogą mieć typ zbioru potwierdzony przez instancję Comprehension . Nazwał wynik „predykatywnym NF” (NFP); jest oczywiście wątpliwe, czy jakakolwiek teoria o samodzielnym wszechświecie jest naprawdę predykatywna. Holmes wykazał, że NFP ma taką samą siłę spójności jak predykatywna teoria typów Principia Mathematica bez aksjomatu redukowalności .

Od 2015 r., zarówno na arxiv, jak i na stronie domowej logika, dostępnych jest kilka kandydatów dowodowych autorstwa Randalla Holmesa na temat spójności NF w stosunku do ZF. Holmes demonstruje ekwispójność „dziwnego” wariantu TST, a mianowicie TTT λ – „teoria splątanych typów z typami λ” – z NF. Holmes następnie pokazuje, że TTT λ jest spójne w stosunku do ZFA, czyli ZF z atomami, ale bez wyboru. Holmes demonstruje to, konstruując w ZFA+C, czyli ZF z atomami i wyborem, klasowy model ZFA, który zawiera „splątane sieci kardynałów”. Wszystkie kandydackie dowody są dość długie, ale społeczność NF nie zidentyfikowała jeszcze żadnych nieodwracalnych błędów.

Jak NF(U) unika paradoksów teorii mnogości

NF wołów jasne z trzech znanych paradoksów z teorii mnogości . To, że NFU, spójna (względem arytmetyki Peano), teoria, która również unika paradoksów, może zwiększyć zaufanie do tego faktu.

Russell paradoks : łatwą sprawą; nie jest formułą warstwową, więc istnienie nie jest potwierdzone przez żaden przypadek zrozumienia . Quine powiedział, że skonstruował NF mając na uwadze ten paradoks.

Paradoks Cantora dotyczący największej liczby kardynalnej wykorzystuje zastosowanie twierdzenia Cantora do zbioru uniwersalnego . Twierdzenie Cantora mówi (biorąc pod uwagę ZFC), że zbiór potęg dowolnego zbiorujest większy niż(nie może być wstrzykiwania (mapa jeden do jednego) zdo). Teraz oczywiście jest wtrysk zdo, jeślijest to zestaw uniwersalny! Rezolucja wymaga, aby zauważyć,że nie ma to sensu w teorii typów: typjest o jeden wyższy niż typ. Poprawnie wpisana wersja (która jest twierdzeniem w teorii typów z zasadniczo tych samych powodów, co oryginalna forma twierdzenia Cantora w ZF ) to, gdziejest zbiorem jednoelementowych podzbiorów. Konkretnym przykładem tego twierdzenia jest: jest mniej zbiorów jednoelementowych niż zbiorów (a więc mniej zbiorów jednoelementowych niż obiektów ogólnych, jeśli jesteśmy w NFU). „Oczywista” bijekcja z wszechświata do zbiorów jednoelementowych nie jest zbiorem; nie jest zbiorem, ponieważ jego definicja nie jest rozwarstwiona. Zauważ, że we wszystkich znanych modelach NFU jest tak, że; Wybór pozwala nie tylko udowodnić, że istnieją urelementy, ale że jest wielu kardynałów pomiędzya.

Można teraz wprowadzić kilka przydatnych pojęć. Mówi się, że zbiór, który spełnia intuicyjnie pociągający, jest kantorem : zbiór kantora spełnia zwykłą formę twierdzenia Cantora . Zestaw , który spełnia warunek, że dalsze The ograniczenie z singleton mapie do A , to zestaw jest nie tylko Cantorian zestaw ale silnie Cantorian .

Paradoks burali-fortiego największej liczby porządkowej jest następujący. Define (po naiwnej teorii mnogości ) z porządkowe jak równoważności klas z dołkowych uporządkowania pod izomorfizmu . Istnieje oczywiste naturalne uporządkowanie liczb porządkowych; ponieważ jest dobrze uporządkowany, należy do liczby porządkowej . Łatwo jest udowodnić (przez indukcję pozaskończoną ), że typ porządku naturalnego porządku na liczbach porządkowych mniejszych niż dana liczba porządkowa jest sama w sobie. Ale to oznacza, że jest to typ porządku liczb porządkowych, a więc jest ściśle mniejszy niż typ porządku wszystkich liczb porządkowych — ale ten ostatni jest z definicji sam w sobie!

Rozwiązanie paradoksu w NF(U) zaczyna się od spostrzeżenia, że ​​typ porządku naturalnego na liczbach porządkowych mniejszy niż jest typu wyższego niż . Stąd para uporządkowana na poziomie typu jest o dwa typy wyższa niż typ jej argumentów, a zwykła para uporządkowana przez Kuratowskiego o cztery typy wyższa. Dla dowolnego typu zlecenia możemy zdefiniować typ zlecenia o jeden typ wyższy: if , to jest typem zlecenia zlecenia . Trywialność operacji T jest tylko pozorna; łatwo wykazać, że T jest operacją ściśle monotoniczną (zachowującą porządek) na liczbach porządkowych.

Teraz lemat o typach porządków można przeformułować w sposób warstwowy: typ porządku naturalnego na liczbach porządkowych to lub w zależności od tego, która para jest używana (zakładamy poniżej parę poziomów typów). Z tego można wywnioskować, że typ porządku na liczbach porządkowych to , a więc . Stąd operacja T nie jest funkcją; nie może być ściśle monotonnej mapy od porządkowej do porządkowej, która wysyła liczbę porządkową w dół! Ponieważ T jest monotoniczne, mamy , "kolejność malejącą" w liczbach porządkowych, która nie może być zbiorem.

Można stwierdzić, że ten wynik pokazuje, że żaden model NF(U) nie jest „standardowy”, ponieważ liczby porządkowe w każdym modelu NFU nie są zewnętrznie dobrze uporządkowane. Nie trzeba zajmować stanowiska w tej sprawie, ale można zauważyć, że jest to również twierdzenie NFU, że każdy zestaw modelu NFU ma nieuporządkowane „liczby porządkowe”; NFU nie stwierdza, że ​​wszechświat V jest modelem NFU, mimo że V jest zbiorem, ponieważ relacja przynależności nie jest relacją zbioru.

Dalszy rozwój matematyki w NFU, z porównaniem do rozwoju tego samego w ZFC, patrz implementacja matematyki w teorii mnogości .

System ML (logika matematyczna)

ML jest rozszerzeniem NF, które obejmuje zarówno odpowiednie klasy, jak i zbiory. Zestaw teoria 1940 pierwszej edycji Quine „s Logika matematyczna żonaty NF do odpowiednich klas z NBG teorii mnogości i obejmowała schemat aksjomatu nieograniczonego zrozumienia dla odpowiednich klas. Jednak J. Barkley Rosser  ( 1942 ) udowodnił, że system przedstawiony w logice matematycznej podlegał paradoksowi Burali-Forti. Ten wynik nie dotyczy NF. Hao Wang  ( 1950 ) pokazał, jak zmienić aksjomaty Quine'a dla ML, aby uniknąć tego problemu, a Quine umieścił wynikową aksjomatyzację w drugim i ostatnim wydaniu Mathematical Logic z 1951 roku .

Wang udowodnił, że jeśli NF jest niesprzeczny, to zrewidowany ML jest tym samym, a także wykazał, że spójność zrewidowanego ML implikuje spójność NF. Oznacza to, że NF i poprawiony ML są jednakowo spójne.

Modele NFU

Istnieje dość prosta metoda masowej produkcji modeli NFU. Używając dobrze znanych technik teorii modeli , można skonstruować niestandardowy model teorii mnogości Zermelo (do podstawowej techniki nie jest potrzebne nic tak silnego jak pełny ZFC), na którym występuje zewnętrzny automorfizm j (nie zbiór modelu) który przesuwa rangę skumulowanej hierarchii zbiorów. Możemy przypuszczać bez utraty ogólności, że . Mówimy o automorfizmie przesuwania rangi, a nie liczby porządkowej, ponieważ nie chcemy zakładać, że każda liczba porządkowa w modelu jest indeksem rangi.

Domeną modelu NFU będzie ranga niestandardowa . Relacja członkostwa modelu NFU będzie:

Teraz można udowodnić, że jest to w rzeczywistości model NFU. Niech będzie formułą warstwową w języku NFU. Wybierz przypisanie typów do wszystkich zmiennych w formule, co świadczy o tym, że jest ona rozwarstwiona. Wybierz liczbę naturalną N większą niż wszystkie typy przypisane do zmiennych przez tę stratyfikację.

Rozwiń formułę do formuły w języku niestandardowego modelu teorii mnogości Zermelo z automorfizmem j wykorzystując definicję przynależności do modelu NFU. Zastosowanie dowolnej potęgi j do obu stron równania lub oświadczenia przynależności zachowuje jego wartość logiczną, ponieważ j jest automorfizmem. Złożyć taki wniosek do każdego wzoru atomowej w w taki sposób, że każda zmienna x przypisany typ i występuje z dokładnie zastosowań j . Jest to możliwe dzięki postaci atomowych oświadczeń o przynależności wywodzących się z oświadczeń o przynależności do NFU oraz warstwowaniu formuły. Każde zdanie kwantyfikowane można przekonwertować do postaci (i podobnie do kwantyfikatorów egzystencjalnych ). Przeprowadź tę transformację wszędzie i uzyskaj wzór, w którym j nigdy nie jest stosowane do zmiennej związanej.

Wybierz dowolną wolną zmienną y w przypisanym typie i . Zastosuj jednolicie do całej formuły, aby uzyskać formułę, w której y pojawia się bez żadnego zastosowania j . Teraz istnieje (ponieważ j wydaje się być stosowane tylko do wolnych zmiennych i stałych), należy do y i zawiera dokładnie te y, które spełniają oryginalną formułę w modelu NFU. ma to rozszerzenie w modelu NFU (zastosowanie j koryguje inną definicję członkostwa w modelu NFU). Oznacza to, że w modelu NFU obowiązuje zrozumienie uwarstwione.

Aby zobaczyć, że słaba Rozszerzalność jest prosta: każdy niepusty element dziedziczy unikalne rozszerzenie z niestandardowego modelu, pusty zbiór dziedziczy również swoje zwykłe rozszerzenie, a wszystkie inne obiekty są urelementami.

Podstawową ideą jest to, że automorfizm j koduje „zestaw mocy” naszego „wszechświata” w jego zewnętrznie izomorficzną kopię wewnątrz naszego „wszechświata”. Pozostałe obiekty niekodujące podzbiorów wszechświata traktowane są jako urelementy .

Jeśli jest liczbą naturalną n , otrzymujemy model NFU, który twierdzi, że wszechświat jest skończony (oczywiście jest zewnętrznie nieskończony). Jeśli jest nieskończony, a wybór obowiązuje w niestandardowym modelu ZFC, otrzymuje się model NFU + Infinity + Choice .

Samowystarczalność podstaw matematycznych w NFU

Ze względów filozoficznych należy zauważyć, że do przeprowadzenia tego dowodu nie jest konieczna praca w ZFC lub jakimkolwiek powiązanym systemie. Powszechnym argumentem przeciwko używaniu NFU jako podstawy matematyki jest to, że powody opierania się na nim mają związek z intuicją, że ZFC jest poprawny. Wystarczy zaakceptować TST (w rzeczywistości TSTU). W zarysie: weź teorię typów TSTU (dopuszczającą urelementy w każdym typie pozytywnym) jako metateorię i rozważ teorię modeli mnogości TSTU w TSTU (te modele będą ciągami zbiorów (wszystkie tego samego typu w metateorii) z osadzeniami każdego w kodowanie osadzeń zespołu mocy w w sposób zgodny z typem). Biorąc pod uwagę osadzenie w (identyfikujące elementy podstawowego „typu” z podzbiorami typu podstawowego), można w naturalny sposób zdefiniować osadzenia z każdego „typu” w jego następcę. Można to ostrożnie uogólnić na sekwencje transskończone .

Zauważ, że konstruowanie takich sekwencji zbiorów jest ograniczone rozmiarem typu, w jakim są konstruowane; to uniemożliwia TSTU udowodnienie własnej spójności (TSTU + Infinity może udowodnić spójność TSTU; aby udowodnić spójność TSTU+ Infinity, potrzebny jest typ zawierający zbiór liczności , którego nie można udowodnić w TSTU+ Infinity bez silniejszych założeń). Teraz te same wyniki teorii modeli można wykorzystać do zbudowania modelu NFU i zweryfikowania, że ​​jest to model NFU w podobny sposób, z użyciem 's zamiast w zwykłej konstrukcji. Ostatnim posunięciem jest zauważenie, że skoro NFU jest spójne, możemy zrezygnować z używania typów absolutnych w naszej metateorii, przenosząc metateorię z TSTU do NFU.

Fakty o automorfizmie j

Automorfizmem j modelu tego rodzaju jest ściśle związane z niektórymi operacjami fizycznych w NFU. Na przykład, jeśli W jest dobrze uporządkowanym w modelu niestandardowym (przypuszczamy tutaj, że używamy par Kuratowskiego, aby kodowanie funkcji w obu teoriach w pewnym stopniu się zgadzało), co jest również dobrym uporządkowaniem w NFU (wszystkie dobre uporządkowania NFU są dobrze uporządkowanymi w niestandardowym modelu teorii mnogości Zermelo, ale nie odwrotnie, ze względu na tworzenie urelementów w konstrukcji modelu), a W ma typ α w NFU, następnie j ( W ) będzie dobrym uporządkowaniem typu T (α) w NFU.

W rzeczywistości j jest kodowane przez funkcję w modelu NFU. Funkcja w modelu niestandardowym, która wysyła singletona dowolnego elementu do jego jedynego elementu, staje się w NFU funkcją, która wysyła każdy singleton { x }, gdzie x jest dowolnym obiektem we wszechświecie, do j ( x ). Wywołania tej funkcji Endo i pozwolić mieć następujące właściwości: endo jest wtryskowo ze zbioru pojedynczych do zbioru zestawów, z właściwości, endo ({ x }) = { endo ({ R }) | yx } dla każdego zbioru x . Ta funkcja może zdefiniować relację „członkostwa” na poziomie typu we wszechświecie, odtwarzając relację członkostwa oryginalnego modelu niestandardowego.

Silne aksjomaty nieskończoności

W tej sekcji rozważany jest efekt dodania różnych „silnych aksjomatów nieskończoności” do naszej zwykłej teorii bazowej, NFU + Nieskończoność + Wybór . Ta podstawowa teoria, znana jako spójna, ma taką samą siłę jak teoria mnogości TST + nieskończoność lub teoria mnogości Zermelo z separacją ograniczoną do wzorów ograniczonych (teoria mnogości MacLane'a).

Do tej podstawowej teorii można dodać silne aksjomaty nieskończoności znane z kontekstu ZFC , takie jak „istnieje niedostępny kardynał”, ale bardziej naturalne jest rozważenie twierdzeń dotyczących zbiorów kantora i silnie kantora. Takie twierdzenia nie tylko powołują do życia wielkich kardynałów zwykłego rodzaju, ale wzmacniają teorię na jej własnych warunkach.

Najsłabszą ze zwykłych silnych zasad jest:

  • Aksjomat liczenia Rossera . Zbiór liczb naturalnych jest zbiorem silnie kantoriańskim.

Aby zobaczyć, jak liczby naturalne są definiowane w NFU, zobacz teoretyczną definicję liczb naturalnych . Oryginalną formą tego aksjomatu podaną przez Rossera było „zbiór { m |1≤ mn } ma n członków”, dla każdej liczby naturalnej n . To intuicyjnie oczywiste twierdzenie nie jest rozwarstwione: w NFU można udowodnić „zbiór { m |1≤ mn } ma członków” (gdzie operacja T na kardynałach jest zdefiniowana przez ; podnosi to typ kardynała o jeden). Dla dowolnej liczby kardynalnej (w tym liczb naturalnych) stwierdzenie, jest równoważne stwierdzeniu, że zbiory A o tej liczności są kantorami (przez zwykłe nadużycie języka, nazywamy takich kardynałów „kardynałami kantora”). Łatwo jest wykazać, że twierdzenie, że każda liczba naturalna jest kantorem, jest równoważne twierdzeniu, że zbiór wszystkich liczb naturalnych jest silnie kantorski.

Liczenie jest zgodne z NFU, ale zauważalnie zwiększa jego wytrzymałość; nie, jak można by się spodziewać, w dziedzinie arytmetyki, ale w teorii wyższych zbiorów. NFU + Infinity udowadnia, że ​​każdy istnieje, ale nie istnieje; NFU + liczenie (z łatwością) dowodzi nieskończoności , a ponadto dowodzi istnienia dla każdego n, ale nie istnienia . (Patrz numery beth ).

Liczenie implikuje od razu, że nie trzeba przypisywać typów zmiennym ograniczonym do zbioru liczb naturalnych dla celów stratyfikacji; jest to twierdzenie, że zbiór potęgowy silnie Cantoriańskiego jest silnie Cantoriański, więc nie jest konieczne przypisywanie typów zmiennym ograniczonym do dowolnego iterowanego zbioru potęgowego liczb naturalnych lub do tak znanych zbiorów, jak zbiór liczb rzeczywistych , zbiór funkcji od liczb rzeczywistych do liczb rzeczywistych i tak dalej. Siła funkcji liczenia w teorii mnogości jest w praktyce mniej ważna niż wygoda polegająca na braku konieczności adnotowania zmiennych, o których wiadomo, że mają wartości liczb naturalnych (lub pokrewnych rodzajów wartości) w nawiasach pojedynczych, lub stosowania operacji T w celu uzyskania zbioru warstwowego definicje.

Liczenie implikuje nieskończoność ; każdy z poniższych aksjomatów musi być połączony z NFU + Nieskończoność, aby uzyskać efekt silnych wariantów Nieskończoności ; Ali Enayat zbadał siłę niektórych z tych aksjomatów w modelach NFU + „wszechświat jest skończony”.

Model skonstruowany powyżej spełnia wymagania liczenia na wypadek, gdyby automorfizm j ustalał wszystkie liczby naturalne w leżącym u jego podstaw niestandardowym modelu teorii mnogości Zermelo.

Kolejnym silnym aksjomatem, który rozważamy, jest

  • Aksjomat separacji silnie kantorowskiej : Dla dowolnego silnie kantorowskiego zbioru A i dowolnej formuły (niekoniecznie stratyfikowanej!) istnieje zbiór { xA |φ}.

Bezpośrednie konsekwencje obejmują indukcję matematyczną dla warunków nieuwarstwionych (która nie jest konsekwencją liczenia ; wiele, ale nie wszystkie nieuwarstwione przypadki indukcji na liczbach naturalnych wynikają z liczenia ).

Ten aksjomat jest zaskakująco silny. Nieopublikowana praca Roberta Solovay'a pokazuje, że siła spójności teorii NFU* = NFU + Liczenie + Silnie Cantoriańska Separacja jest taka sama jak teoria mnogości Zermelo + Zastąpienie .

Ten aksjomat obowiązuje w modelu skonstruowanym powyżej (z opcją Choice ), jeśli liczby porządkowe ustalone przez j i dominują tylko liczby porządkowe ustalone przez j w podstawowym modelu niestandardowym teorii mnogości Zermelo są standardowe, a zbiór potęgowy dowolnej takiej liczby porządkowej w modelu jest również standardem. Ten warunek jest wystarczający, ale nie konieczny.

Następne jest

  • Aksjomat zbiorów kantorów : Każdy zbiór kantorów jest silnie kantorowski.

To bardzo proste i atrakcyjne twierdzenie jest niezwykle silne. Solovay wykazał dokładną równoważność siły spójności teorii NFUA = NFU + Nieskończoność + Zbiory Kantorów z teorią ZFC + schematu zakładającego istnienie kardynała n- Mahlo dla każdej konkretnej liczby naturalnej n . Ali Enayat wykazał, że teoria kantorskich klas równoważności dobrze ugruntowanych relacji ekstensjonalnych (która daje naturalny obraz początkowego segmentu kumulatywnej hierarchii ZFC) bezpośrednio interpretuje rozszerzenie ZFC z n- Mahlo kardynałami. Do modelu tej teorii można zastosować technikę permutacyjną, aby uzyskać model, w którym dziedzicznie silnie Cantorian zestawia ze zwykłym modelem relacji przynależności silne rozszerzenie ZFC.

Ten aksjomat obowiązuje w modelu skonstruowanym powyżej (z Choice ) na wypadek, gdyby liczby porządkowe ustalone przez j w bazowym niestandardowym modelu ZFC były początkowym (właściwej klasy) segmentem liczb porządkowych modelu.

Następnie rozważ

  • Aksjomat separacji kantora : Dla dowolnego zbioru kantora A i dowolnej formuły (niekoniecznie rozwarstwionej!) istnieje zbiór { xA |φ}.

Łączy to efekt dwóch poprzednich aksjomatów i jest w rzeczywistości jeszcze silniejsze (nie wiadomo dokładnie, w jaki sposób). Unstratified indukcja matematyczna pozwala na udowodnienie, że istnieją n -Mahlo kardynałowie dla każdego n , podane Cantorian Zestawy , które daje rozszerzenie ZFC , że jest nawet silniejszy niż poprzedni, co tylko potwierdza, że istnieją n -Mahlos dla każdej liczby naturalnej betonu ( pozostawiając otwartą możliwość niestandardowych kontrprzykładów).

Ten aksjomat będzie obowiązywał w modelu typu opisanego powyżej, jeśli każda liczba porządkowa ustalona przez j jest standardowa, a każdy zbiór potęgowy liczby porządkowej ustalonej przez j jest również standardem w podstawowym modelu ZFC . Znowu ten warunek jest wystarczający, ale nie jest konieczny.

Mówi się, że liczba porządkowa jest kantoriańska, jeśli jest ustalona przez T , i silnie kantoriańska, jeśli dominuje tylko nad liczbami porządkowymi kantoriańskimi (to implikuje, że sama jest kantoriańska). W modelach tego rodzaju, co zbudowane powyżej, kantorowskie liczby porządkowe NFU odpowiadają liczbom porządkowym ustalonym przez j (nie są to te same obiekty, ponieważ w obu teoriach stosowane są różne definicje liczebników porządkowych).

Równie silna jak Zbiory Kantorów jest

  • Aksjomat wielkich liczb porządkowych : Dla każdej niekantorskiej liczby porządkowej , istnieje liczba naturalna n taka, że .

Przypomnijmy, że jest to rodzaj porządku porządku naturalnego na wszystkich liczbach porządkowych. Oznacza to tylko Zestawy Kantorów, jeśli mamy Wybór (ale w każdym przypadku jest na tym poziomie siły spójności). Godne uwagi jest to, że można również określić : to n p określenie jakiegokolwiek skończonej sekwencji porządkowe s długości n taki sposób, że , dla każdej odpowiedniej ı . Ta definicja jest całkowicie niestratyfikowana. Wyjątkowość może być udowodnione (dla tych n , dla których istnieje) i pewnej ilości zdroworozsądkowego rozumowania na temat tego pojęcia można przeprowadzić, wystarczy wykazać, że Large porządkowych implikuje Cantorian Zestawy w obecności wyboru . Pomimo zawiłego formalnego stwierdzenia tego aksjomatu, jest to bardzo naturalne założenie, sprowadzające się do uczynienia działania T na liczbach porządkowych tak prostym, jak to tylko możliwe.

Model tego rodzaju skonstruowany powyżej zadowoli duże liczby porządkowe, jeśli liczby porządkowe przesunięte przez j są dokładnie tymi liczbami porządkowymi, które dominują w niektórych z bazowego niestandardowego modelu ZFC .

  • Aksjomat małych liczb porządkowych : Dla każdej formuły φ istnieje zbiór A taki, że elementy A, które są silnie kantoriańskimi liczbami porządkowymi, są dokładnie tymi silnie kantoriańskimi liczbami porządkowymi takimi, że φ.

Solovay wykazał dokładną równoważność siły spójności NFUB = NFU + Nieskończoność + Zbiory Kantora + Małe liczby porządkowe z teorią mnogości Morse'a-Kelley'a plus twierdzenie, że właściwa klasa porządkowa (klasa wszystkich porządkowych) jest słabo zwartą liczbą kardynalną . To naprawdę bardzo mocne! Co więcej, NFUB-, który jest NFUB z pominiętymi zestawami Cantorian , łatwo zauważyć, że ma taką samą siłę jak NFUB.

Model skonstruowany powyżej spełni ten aksjomat, jeśli każdy zbiór liczb porządkowych ustalonych przez j jest przecięciem pewnego zbioru liczb porządkowych z liczbami porządkowymi ustalonymi przez j , w bazowym niestandardowym modelu ZFC.

Jeszcze silniejsza jest teoria NFUM = NFU + Nieskończoność + Duże liczby porządkowe + Małe liczby porządkowe . Jest to równoważne teorii mnogości Morse'a-Kelley'a z predykatem na klasach, który jest κ-kompletnym ultrafiltrem non-głównym na odpowiedniej porządkowej klasy κ; w efekcie jest to teoria mnogości Morse-Kelley + „właściwa liczba porządkowa klasy jest mierzalną liczbą kardynalną ”!

Szczegóły techniczne nie są tutaj głównym punktem, ponieważ rozsądne i naturalne (w kontekście NFU) twierdzenia okazują się równoważne w mocy bardzo silnym aksjomatom nieskończoności w kontekście ZFC . Fakt ten jest związany z korelacją pomiędzy istnieniem opisanych powyżej modeli NFU i spełniających te aksjomaty, a istnieniem modeli ZFC z automorfizmami o specjalnych właściwościach.

Zobacz też

Uwagi

Bibliografia

  • Krab, Marcel (1982). „O spójności impredatywnego fragmentu NF Quine'a”. Dziennik logiki symbolicznej . 47 (1): 131–136. doi : 10.2307/2273386 . JSTOR  2273386 .
  • Forster, TE (1992), Teoria mnogości ze zbiorem uniwersalnym. Odkrywanie nieopisanego wszechświata , Oxford Science Publications, Oxford Logic Guides, 20 , Nowy Jork: The Clarendon Press, Oxford University Press, ISBN 0-19-853395-0, MR  1166801
  • Holmes, M. Randall (1998), Elementarna teoria mnogości ze zbiorem uniwersalnym (PDF) , Cahiers du Centre de Logique, 10 , Louvain-la-Neuve: Université Catholique de Louvain, Departament Filozofii, ISBN 2-87209-488-1, MR  1759289
  • Jensen, RB (1969), "O spójności niewielkiej (?) Modyfikacja NF Quine'a", Synthese , 19 (1/2): 250-63, doi : 10.1007/bf00568059 , JSTOR  20114640 , S2CID  46960777 Z dyskusją Quine'a.
  • Quine, WV (1937), "Nowe podstawy logiki matematycznej", The American Mathematical Monthly , Mathematical Association of America, 44 (2): 70-80, doi : 10.2307/2300564 , JSTOR  2300564
  • Quine, Willard Van Orman (1940), Logika matematyczna (pierwsze wydanie), New York: WW Norton & Co., Inc., MR  0002508
  • Quine, Willard Van Orman (1951), Logika matematyczna (red. poprawione), Cambridge, Massachusetts: Harvard University Press, ISBN 0-674-55451-5, MR  0045661
  • Quine, WV , 1980, „New Foundations for Mathematical Logic” w From a Logical Point of View , wyd. 2, poprawione. Uniwersytet Harvarda Prasa: 80-101. Ostateczna wersja tego, od czego wszystko się zaczęło, a mianowicie artykuł Quine'a z 1937 roku w American Mathematical Monthly .
  • Rosser, Barkley (1942), "Paradoks Burali-Forti", Journal of Symbolic Logic , 7 (1): 1-17, doi : 10.2307/2267550 , JSTOR  2267550 , MR  0006327
  • Wang, Hao (1950), "formalny system logiki", Journal of Symbolic Logic , 15 (1): 25-32, doi : 10.2307/2268438 , JSTOR  2268438 , MR  0034733
  • Holmes, M. Randall (2008). „Symetria jako kryterium rozumienia motywującego 'nowe podstawy ' Quine'a ”. Studia Logiki . 88 (2): 195–213. doi : 10.1007/s11225-008-9107-8 . S2CID  207242273 .

Zewnętrzne linki