Wymuszanie (matematyka) - Forcing (mathematics)

W matematycznej dyscypliny teorii mnogości , zmuszając jest techniką udowadniając spójności i niezależności wyników. Po raz pierwszy został użyty przez Paula Cohena w 1963 roku, aby udowodnić niezależność aksjomatu wyboru i hipotezy continuum od teorii mnogości Zermelo-Fraenkla .

Wymuszanie zostało znacznie przerobione i uproszczone w następnych latach i od tego czasu służy jako potężna technika, zarówno w teorii mnogości, jak iw obszarach logiki matematycznej, takich jak teoria rekurencji . Opisowa teoria mnogości wykorzystuje pojęcia wymuszania zarówno z teorii rekurencji, jak i teorii mnogości. Wymuszanie było również używane w teorii modeli , ale w teorii modeli często definiuje się generacyjność bezpośrednio bez wzmianki o wymuszaniu.

Intuicja

Intuicyjnie wymuszanie polega na rozszerzeniu zbioru teoretycznego wszechświata na większy wszechświat . W tym większym wszechświecie, na przykład, można mieć wiele nowych podzbiory o które nie było w starym wszechświecie, a tym samym narusza hipoteza continuum .

Chociaż niemożliwe w przypadku zbiorów skończonych , jest to tylko kolejna wersja paradoksu Cantora dotyczącego nieskończoności. W zasadzie można by rozważyć:

identyfikować się z , a następnie wprowadzać rozszerzoną relację przynależności obejmującą „nowe” zbiory postaci . Forsing jest bardziej rozbudowaną wersją tego pomysłu, redukującą ekspansję do istnienia jednego nowego zestawu i pozwalającą na precyzyjną kontrolę nad właściwościami rozszerzonego wszechświata.

Oryginalna technika Cohena, zwana obecnie forsowaniem rozgałęzionym , różni się nieco od wymuszenia nierozgałęzionego, które tu omówiono . Wymuszanie jest również równoważne z metodą modeli o wartościach logicznych , która według niektórych jest koncepcyjnie bardziej naturalna i intuicyjna, ale zwykle znacznie trudniejsza do zastosowania.

Wymuszanie pozy

Zmuszając poset jest uporządkowana potrójne, gdzie jest preorder na to atomless , co oznacza, że spełnia następujący warunek:

  • Dla każdego są takie , że , bez takich , że . Największym elementem jest , czyli dla wszystkich .

Z członkami są nazywane zmuszając warunków lub tylko warunki . Jeden czyta się jako „ jest silniejszy niż ”. Intuicyjnie, "mniejszy" warunek dostarcza "więcej" informacji, tak jak mniejszy przedział dostarcza więcej informacji o liczbie π niż przedział .

Stosowane są różne konwencje. Niektórzy autorzy wymagają również bycia antysymetrycznym , aby relacja była porządkiem częściowym . Niektórzy i tak używają terminu zamówienie częściowe , co jest sprzeczne ze standardową terminologią, podczas gdy niektórzy używają terminu przedsprzedaż . Można zrezygnować z największego elementu. Odwrotna kolejność jest również używana, w szczególności przez Saharona Shelaha i jego współautorów.

P-nazwy

Związany z zmuszając poset jest klasa z - nazwy . A -nazwa to zbiór form

W rzeczywistości jest to definicja rekurencji nieskończonej . Z pustego zestawu, w następcy porządkowej do porządkową , zasilania zestaw operatora oraz graniczną , określa hierarchię następujące:

Wtedy klasa -names jest zdefiniowana jako

W -names są w rzeczywistości, ekspansją wszechświata . Biorąc pod uwagę , definiuje się jako -name

Ponownie, jest to tak naprawdę definicja rekurencji nieskończonej.

Interpretacja

Biorąc pod uwagę dowolny podzbiór o , jeden przy Definiuje interpretacja lub wycena map z -names przez

To znowu definicja rekurencji pozaskończonej. Zauważ, że jeśli , to . Jeden wtedy definiuje

tak, że .

Przykład

Dobrym przykładem zmuszając poset to , gdzie i jest zbiorem borelowskich podzbiorów o konieczności niezerową miary Lebesgue'a . W tym przypadku można mówić o warunkach jako o prawdopodobieństwach, a -name przypisuje członkostwo w sensie probabilistycznym. Ze względu na gotową intuicję, jaką może zapewnić ten przykład, język probabilistyczny jest czasami używany z innymi rozbieżnymi pozycjami wymuszalnymi.

Policzalne modele przechodnie i filtry generyczne

Kluczowym krokiem w wymuszenia jest, biorąc pod uwagę wszechświat , znalezienie odpowiedniego obiektu nie w . Powstała klasa wszystkich interpretacji -names będzie modelem, który właściwie rozszerza oryginał (od ).

Zamiast pracować z , warto rozważyć przeliczalny model przechodni z . „Model” odnosi się do modelu teorii mnogości, albo wszystkich , albo modelu dużego, ale skończonego podzbioru , lub jakiegoś jego wariantu. „Przechodniość” oznacza, że ​​jeśli , to . Kolaps mostowskiego stwierdza, że można przyjąć, jeśli relacja członków jest dobrze założony . Efektem przechodniości jest to, że członkostwo i inne podstawowe pojęcia mogą być obsługiwane intuicyjnie. Przeliczalność modelu opiera się na twierdzeniu Löwenheima-Skolema .

Jak jest zbiór, nie ma zbiorów w – wynika to z paradoksu Russella . Odpowiednim zestawem do pobrania i dołączenia jest filtr ogólny na . Warunek „filtr” oznacza, że:

  • jeśli , to
  • jeśli , to istnieje taka, że

By być „ogólnym” oznacza:

  • Jeśli jest „gęstym” podzbiorem (to znaczy dla każdego , istnieje taki, który ), to .

Istnienie filtra generycznego wynika z lematu Rasiowa-Sikorski . W rzeczywistości, nieco więcej jest prawdą: biorąc pod uwagę warunek , można znaleźć ogólny filtr, taki jak . Ze względu na włączony warunek podziału (określany powyżej jako „bezatomowy”), jeśli jest filtrem, to jest gęsty. Jeśli , to ponieważ jest modelem . Z tego powodu filtr ogólny nigdy nie występuje w .

Wymuszanie

Mając ogólny filtr , postępuj w następujący sposób. Podklasa -names w jest oznaczona . Pozwolić

Aby zredukować badania nad teorią mnogości do teorii , pracuje się z „językiem wymuszającym”, który jest zbudowany jak zwykła logika pierwszego rzędu , gdzie członkostwo jest relacją binarną, a wszystkie -nazwy jako stałe.

Zdefiniuj (będzie odczytywane jako " siły w modelu z poset "), gdzie jest warunkiem, jest formułą w języku wymuszającym, a są to nazwy, co oznacza, że ​​if jest filtrem ogólnym zawierającym , then . Szczególny przypadek jest często pisany jako „ ” lub po prostu „ ”. Takie stwierdzenia są prawdziwe w , bez względu na to, co jest.

Co ważne, ta zewnętrzna definicja relacji wymuszającej jest równoznaczna z definicją wewnętrzną w , definiowaną przez indukcję ponadskończoną nad nazwami na instancjach i , a następnie przez zwykłą indukcję nad złożonością formuł. Skutkuje to tym, że wszystkie właściwości są w rzeczywistości właściwościami , a weryfikacja in staje się prosta. Zwykle podsumowuje się to jako następujące trzy kluczowe właściwości:

  • Prawda : wtedy i tylko wtedy, gdy jest wymuszona przez , czyli pod pewnym warunkiem , mamy .
  • Definiowalność : Stwierdzenie " " jest definiowalne w .
  • Spójność : .

Relację wymuszającą definiujemy in przez indukcję na złożoności formuł, w której najpierw definiujemy relację dla formuł atomowych przez -indukcję, a następnie definiujemy ją dla dowolnych formuł przez indukcję na ich złożoności.

Najpierw definiujemy relację wymuszającą na formułach atomowych, robiąc to jednocześnie dla obu typów formuł i . Oznacza to, że definiujemy jedną relację, w której określamy rodzaj formuły w następujący sposób:

  1. oznacza .
  2. oznacza .
  3. oznacza .

Oto warunek i są -nazwy. Niech będzie formułą określoną przez -indukcję:

R1. wtedy i tylko wtedy, gdy .

R2. wtedy i tylko wtedy, gdy .

R3. wtedy i tylko wtedy, gdy .

Bardziej formalnie, używamy następującej binarnej relacji -names: Let's hold for names and if and only if for co najmniej jednego warunku . Relacja ta jest dobrze ugruntowana, co oznacza, że ​​dla dowolnej nazwy klasa wszystkich nazw , taka jaka zachodzi, jest zbiorem i nie ma takiej funkcji, jak .

Ogólnie rzecz biorąc, dobrze ugruntowana relacja nie jest preorderem, ponieważ może nie być przechodnia. Ale jeśli uznamy to za „porządkowanie”, jest to relacja bez nieskończonych ciągów malejących i gdzie dla dowolnego elementu klasa elementów pod nim jest zbiorem.

Łatwo jest zamknąć dowolną relację binarną dla przechodniości. Dla nazw i , obowiązuje, jeśli istnieje co najmniej jeden skończony ciąg (jako odwzorowanie z domeną ) dla niektórych takich, że , i dla any , obowiązuje . Takie uporządkowanie też jest uzasadnione.

Definiujemy następujący dobrze zdefiniowany porządek na parach nazw: jeśli zachodzi jedno z poniższych:

  1. ,
  2. i ,
  3. i i .

Relację definiuje rekurencja na parach nazw. Dla dowolnej pary jest to określone przez tę samą relację na „prostszych” parach. W rzeczywistości, przez twierdzenie o rekurencji istnieje formuła taka, że ​​​​R1, R2 i R3 są twierdzeniami, ponieważ jego wartość logiczna w pewnym momencie jest zdefiniowana przez jego wartości logiczne w „mniejszych” punktach w stosunku do pewnej dobrze uzasadnionej relacji używanej jako „porządkowanie ”. Teraz jesteśmy gotowi do zdefiniowania relacji wymuszającej:

  1. oznacza .
  2. oznacza .
  3. oznacza .
  4. oznacza .
  5. oznacza .

W rzeczywistości jest to przekształcenie dowolnej formuły na formułę, w której i są dodatkowymi zmiennymi. Jest to definicja relacji wymuszającej we wszechświecie wszystkich zbiorów niezależnie od dowolnego przeliczalnego modelu przechodniego. Istnieje jednak związek między tym „syntaktycznym” sformułowaniem forsowania a „semantycznym” sformułowaniem forsowania względem jakiegoś przeliczalnego modelu przechodniego .

  1. Dla każdego wzoru jest twierdzenie teorii (na przykład, związku o skończonej liczbie axioms) tak, że dla każdego modelu policzalnych przechodniego taki sposób, oraz wszelkich atomless celu częściowego i każdy filtr -generic ponad

Nazywa się to własnością definiowalności relacji wymuszającej.

Konsystencja

Powyższą dyskusję można podsumować w wyniku fundamentalnej spójności, zgodnie z którą, mając pozycję wymuszającą , możemy założyć istnienie filtra generycznego , nienależącego do wszechświata , takiego, który jest ponownie modelującym wszechświatem opartym na teorii mnogości . Co więcej, wszystkie prawdy zawarte w niej mogą zostać zredukowane do prawd dotyczących relacji wymuszającej.

Oba style, przylegające albo do przeliczalnego modelu przechodniego, albo do całego wszechświata , są powszechnie używane. Rzadziej spotykane jest podejście wykorzystujące „wewnętrzną” definicję forsowania, w której nie wspomina się o modelach zbiorowych lub klasowych. Była to oryginalna metoda Cohena, aw jednym opracowaniu stała się metodą analizy o wartościach logicznych.

Wymuszanie Cohena

Najprostszym nietrywialnym pozycją wymuszającą jest , skończone funkcje cząstkowe od do pod odwrotnym włączeniem. Oznacza to, że stan jest zasadniczo dwa podzbiory rozłączne skończone i od , być traktowane jako „tak” i „nie” części , bez informacji umieszczonych na wartości poza domeną . „ jest silniejsze niż ” oznacza , innymi słowy, części „tak” i „nie” są nadzbiorami części „tak” i „nie” i w tym sensie dostarczają więcej informacji.

Niech będzie ogólnym filtrem dla tego postu. Jeśli i są w , to jest warunkiem, ponieważ jest filtrem. Oznacza to, że jest to dobrze zdefiniowana funkcja częściowa od do, ponieważ dowolne dwa warunki zgadzają się we wspólnej dziedzinie.

W rzeczywistości jest to funkcja całkowita. Biorąc pod uwagę , niech . Wtedy jest gęsty. (Mając dowolny , jeśli nie należy do domeny , dołącz wartość for — wynik jest w .) Warunek ma w swojej dziedzinie, a ponieważ , stwierdzamy, że jest zdefiniowany.

Let , zbiór wszystkich "tak" członków warunków ogólnych. Możliwe jest bezpośrednie nadanie nazwy . Pozwolić

Następnie załóżmy, że w . Twierdzimy, że . Pozwolić

Wtedy jest gęsty. (Biorąc pod uwagę , znajdź to, co nie należy do jego domeny, i dołącz wartość za sprzeczną ze statusem " ".) Następnie wszyscy świadkowie . Podsumowując, jest to „nowy” podzbiór , z konieczności nieskończony.

Wymiana z , czyli rozważyć zamiast skończonych funkcje cząstkowe, których wejścia są od formy , ze i , i których wyjścia są albo , dostaje nowe podzbiory . Wszystkie są różne za pomocą argumentu gęstości: Biorąc pod uwagę , niech

wtedy każdy jest gęsty, a stan ogólny w nim dowodzi, że a-ty nowy zbiór nie zgadza się gdzieś z tym nowym zbiorem.

Nie jest to jeszcze falsyfikacja hipotezy kontinuum. Trzeba udowodnić, że żadne nowe mapy, które zostały wprowadzone na mapie wychodzą albo na . Na przykład, jeśli zamiast tego rozważymy skończone funkcje cząstkowe od do , pierwszą niepoliczalną liczbę porządkową , otrzymamy bijekcję od do . Innymi słowy, nie załamał się , a na przedłużeniu zmusza, jest przeliczalna porządkowej.

Ostatnim krokiem w ukazaniu niezależności hipotezy continuum jest zatem wykazanie, że wymuszanie Cohena nie załamuje kardynałów. Do tego wystarczająca kombinatoryczna właściwość polega na tym, że wszystkie antyłańcuchy pozy wymuszającej są policzalne.

Policzalny warunek łańcucha

(Silny) antyłańcuch o to podzbiór taki, że jeśli , to i są niekompatybilne (pisemny ), co oznacza, że nie jest w taki sposób, że i . W przykładzie na zbiorach Borel niezgodność oznacza, że ma miarę zerową. W przykładzie dotyczącym skończonych funkcji częściowych niezgodność oznacza, że nie jest to funkcja, innymi słowy, i przypisuje różne wartości do pewnych danych wejściowych domeny.

spełnia warunek łańcucha policzalnego (ccc) wtedy i tylko wtedy, gdy każdy antyłańcuch jest policzalny. (Nazwa, która jest oczywiście nieodpowiednia, jest pozostałością po starszej terminologii. Niektórzy matematycy piszą „cac” dla „policzalnego stanu antyłańcucha”).

Łatwo zauważyć, że jest to zgodne z ccc, ponieważ miary sumują się co najwyżej . Ponadto spełnia KSH, ale dowodem na to jest coraz trudniejsze.

Biorąc pod uwagę niepoliczalną podrodzinę , dla niektórych zmniejsz się do niepoliczalnej podrodziny zestawów wielkości . Jeśli dla niepoliczalnych wielu , zmniejsz to do niepoliczalnej podrodziny i powtórz, uzyskując skończony zbiór i niepoliczalną rodzinę o niezgodnych warunkach wielkości, tak że każda jest dla co najwyżej policzalnych wielu . Teraz, pick arbitralny i wybrać z dowolnego , że nie jest jednym z przeliczalnie wielu członków posiadających członkiem domeny wspólnego z . Wtedy i są kompatybilne, więc nie jest antyłańcuchem. Innymi słowy, -antyłańcuchy są policzalne.

Znaczenie antyłańcuchów w forsowaniu jest takie, że dla większości celów gęste zestawy i maksymalne antyłańcuchy są równoważne. Maksymalny antyłańcuch to taki, który nie może zostać rozszerzona na większą antyłańcuch. Oznacza to, że każdy element jest zgodny z jakimś członkiem . Istnienie maksymalnego antyłańcucha wynika z lematu Zorna . Biorąc pod uwagę maksymalny antyłańcuch , niech

Wtedy jest gęsty i wtedy i tylko wtedy, gdy . I odwrotnie, mając gęsty zbiór , Lemat Zorna pokazuje, że istnieje maksymalny antyłańcuch , a wtedy wtedy i tylko wtedy, gdy .

Załóżmy, że spełnia ccc Given , z funkcją w , można aproksymować wewnątrz w następujący sposób. Niech będzie nazwą dla (z definicji ) i niech będzie warunkiem, który wymusza bycie funkcją od do . Zdefiniuj funkcję , której dziedziną jest , by

Dzięki definiowalności forsowania definicja ta ma sens w ramach . Przez spójność wymuszeń, inne pochodzą od niezgodnych . Przez ccc jest policzalne.

Podsumowując, jest nieznany, ponieważ zależy od , ale nie jest szalenie nieznany w przypadku forsowania ccc. Można zidentyfikować policzalny zestaw domysłów dla tego, jaka jest wartość na dowolnym wejściu, niezależnie od .

Ma to następującą bardzo ważną konsekwencję. Jeśli w , jest odjęciem od jednej nieskończonej liczby porządkowej na drugą, to następuje odjęcie w , a co za tym idzie, odjęcie w . W szczególności kardynałowie nie mogą upaść. Wniosek jest taki, że w .

Wymuszanie Eastona

Dokładną wartość continuum w powyższym modelu Cohena i wariantów, jak dla kardynałów w ogóle, opracował Robert M. Solovay , który również opracował sposób naruszania ( hipoteza uogólnionego continuum ), tylko dla regularnych kardynałów , skończoną kilka razy. Na przykład w powyższym modelu Cohena, jeśli zachodzi w , to zachodzi w .

William B. Easton wypracować właściwą wersję klasy jest naruszenie regularnych kardynałów, pokazując, że w zasadzie znane ograniczenia (monotoniczność, Cantora Twierdzenie i König Twierdzenie ), były jedynymi -provable ograniczenia (patrz Easton Twierdzenie ).

Praca Eastona była godna uwagi, ponieważ obejmowała wymuszanie w odpowiedniej klasie warunków. Generalnie metoda forsowania odpowiednią klasą warunków nie daje modelu . Na przykład forsowanie z , gdzie jest właściwą klasą wszystkich liczb porządkowych, sprawia, że ​​continuum jest właściwą klasą. Z drugiej strony forsowanie wprowadza policzalne wyliczanie liczb porządkowych. W obu przypadkach wynik wyraźnie nie jest modelem .

Kiedyś sądzono, że bardziej wyrafinowane wymuszanie pozwoliłoby również na arbitralną zmianę uprawnień pojedynczych kardynałów . Okazało się to jednak trudnym, subtelnym, a nawet zaskakującym problemem, z kilkoma dodatkowymi ograniczeniami, które można udowodnić w modelach wymuszających, zależnie od spójności różnych właściwości wielkokardynalnych . Pozostaje wiele otwartych problemów.

Reale losowe

Wymuszanie losowe można zdefiniować jako wymuszanie zbioru wszystkich zwartych podzbiorów miary dodatniej uporządkowanych relacją (mniejszy zbiór w kontekście włączenia jest mniejszym zbiorem w porządkowaniu i reprezentuje stan z większą ilością informacji). Istnieją dwa rodzaje ważnych gęstych zestawów:

  1. Dla dowolnej liczby całkowitej dodatniej zbiór
    jest gęsty, gdzie jest średnica zbioru .
  2. Dla dowolnego podzbioru borelowskiego miary 1, zbiór
    jest gęsty.

Dla każdego filtra i dla każdego skończenie wielu elementów jest taki, który się trzyma . W przypadku tego uporządkowania oznacza to, że dowolny filtr jest zbiorem zwartych zbiorów z właściwością skończonego przecięcia. Z tego powodu przecięcie wszystkich elementów dowolnego filtra nie jest puste. Jeśli jest filtrem przecinającym gęsty zbiór dla dowolnej dodatniej liczby całkowitej , to filtr zawiera warunki o dowolnie małej dodatniej średnicy. Dlatego przecięcie wszystkich warunków z ma średnicę 0. Ale jedyne niepuste zbiory o średnicy 0 to singletony. Więc jest dokładnie jedna liczba rzeczywista taka, że .

Niech będzie dowolnym borelowskim zbiorem miary 1. Jeśli przecina , to .

Jednak filtr ogólny w modelu przechodnim przeliczalnym nie znajduje się w programie . Rzeczywistość określona przez dowodnie nie jest elementem . Problem polega na tym , że jeśli , to „ jest zwarte”, ale z punktu widzenia jakiegoś większego wszechświata , może być niezwarte, a przecięcie wszystkich warunków z filtru generycznego jest w rzeczywistości puste. Z tego powodu rozważamy zbiór domknięć topologicznych warunków z G. Z powodu własności skończonego przecięcia , zbiór ma również własność skończonego przecięcia. Elementy zbioru są zbiorami ograniczonymi domkniętymi jako domknięciami zbiorów ograniczonych. Dlatego jest zbiorem zwartych zbiorów z właściwością przecięcia skończonego, a zatem ma niepuste przecięcie. Ponieważ model gruntu dziedziczy metrykę z wszechświata , zbiór zawiera elementy o dowolnie małej średnicy. Na koniec jest dokładnie jedna rzeczywista, która należy do wszystkich członków zbioru . Filtr ogólny można zrekonstruować z jako .

Jeśli jest nazwą , a dla hold " jest zbiorem borelowskim o takcie 1", to przechowuje

dla niektórych . Jest taka nazwa , że dla każdego ogólnego filtra trzyma się

Następnie

obowiązuje dla każdego warunku .

Każdy zbiór borelowski może być, w sposób nieunikalny, budowany, zaczynając od przedziałów z racjonalnymi punktami końcowymi i stosując operacje dopełnienia i policzalnych sum policzalną liczbę razy. Zapis takiej konstrukcji nazywany jest kodem borelowskim . Mając zestaw Borel w , odzyskuje się kod Borel, a następnie stosuje tę samą sekwencję konstrukcji w , otrzymując zestaw Borel . Można udowodnić, że otrzymuje się ten sam zbiór niezależnie od konstrukcji , oraz że zachowane są podstawowe własności. Na przykład, jeśli , to . Jeśli ma miarę zero, to ma miarę zero. To mapowanie jest iniektywne.

Dla dowolnego zbioru takiego, jak i " jest zbiorem borelowskim o mierze 1" obowiązuje .

Oznacza to, że jest to „nieskończony ciąg losowy zer i jedynek” z punktu widzenia , co oznacza, że ​​spełnia wszystkie testy statystyczne z modelu naziemnego .

Tak więc dana , losowa wartość rzeczywista, można to wykazać

Ze względu na wzajemną interdefiniowalność między a , zazwyczaj pisze się dla .

Inną interpretację rzeczywistości przedstawiła Dana Scott . Liczby wymierne w mają nazwy, które odpowiadają policzalnie – wielu odrębnym wartościom wymiernym przypisanym do maksymalnego antyłańcucha zbiorów borelowskich – innymi słowy, pewnej funkcji o wartościach wymiernych na . Liczby rzeczywiste w odpowiadają wówczas cięciom Dedekinda takich funkcji, czyli funkcji mierzalnych .

Modele o wartości logicznej

Być może jaśniej, metodę można wyjaśnić w kategoriach modeli o wartościach logicznych. W nich każdemu zdaniu przypisywana jest wartość prawdy z jakiejś kompletnej bezatomowej algebry Boole'a , a nie tylko wartość prawda/fałsz. Następnie w tej algebrze Boole'a wybierany jest ultrafiltr , który przypisuje wartości prawda/fałsz do stwierdzeń naszej teorii. Chodzi o to, że powstała teoria ma model, który zawiera ten ultrafiltr, co można rozumieć jako nowy model uzyskany przez rozszerzenie starego o ten ultrafiltr. Wybierając w odpowiedni sposób model o wartości logicznej, możemy otrzymać model, który posiada pożądaną właściwość. W nim tylko zdania, które muszą być prawdziwe (są „zmuszone” być prawdziwe), będą w pewnym sensie prawdziwe (ponieważ ma tę właściwość rozszerzenia/minimalności).

Wyjaśnienie metamatematyczne

W forsowaniu zwykle staramy się wykazać, że jakieś zdanie jest zgodne z (lub opcjonalnie z rozszerzeniem ). Jednym ze sposobów interpretacji argumentu jest założenie, że jest spójny, a następnie udowodnienie, że w połączeniu z nowym zdaniem jest również spójny.

Każdy „warunek” jest skończoną informacją – chodzi o to, że tylko skończone kawałki są istotne dla spójności, ponieważ zgodnie z twierdzeniem o zwartości teoria jest spełnialna wtedy i tylko wtedy, gdy każdy skończony podzbiór jej aksjomatów jest spełnialny. Następnie możemy wybrać nieskończony zestaw spójnych warunków, aby rozszerzyć nasz model. Dlatego zakładając niesprzeczność , dowodzimy niesprzeczności rozciągniętej o ten nieskończony zbiór.

Logiczne wyjaśnienie

Przez drugie twierdzenie Gödla o niezupełności nie można udowodnić spójności jakiejkolwiek wystarczająco silnej teorii formalnej, takiej jak , używając tylko aksjomatów samej teorii, chyba że teoria jest niespójna. W konsekwencji matematycy nie próbują dowodzić niesprzeczności, używając tylko aksjomatów , ani dowodzić, że jest to zgodne z każdą hipotezą używającą tylko . Z tego powodu celem dowodu spójności jest udowodnienie spójności względem spójności . Takie problemy są znane jako problemy względnej spójności , z których jeden dowodzi


 

 

 

 

( )

Poniżej przedstawiono ogólny schemat dowodów spójności względnej. Ponieważ każdy dowód jest skończony, używa tylko skończonej liczby aksjomatów:

Dla każdego danego dowodu, może zweryfikować ważność tego dowodu. Można to udowodnić przez indukcję na długości dowodu.

Następnie rozwiąż

Udowadniając, co następuje


 

 

 

 

( ⁎⁎ )

można wywnioskować, że

co jest równoważne

co daje (*). Dowodem jest rdzeń względnego dowodu spójności (**). Dowód może być wykonana z jakiegokolwiek danego skończonego podzespołu z axioms (z przyrządów przebiegu). ( Oczywiście nie ma uniwersalnego dowodu .)

W , można udowodnić, że dla dowolnego warunku zbiór formuł (ocenianych przez nazwy) wymuszonych przez jest dedukcyjnie domknięty. Co więcej, dla każdego aksjomatu dowodzi, że ten aksjomat jest wymuszony przez . Wtedy wystarczy udowodnić, że istnieje przynajmniej jeden warunek, który wymusza .

W przypadku forsowania o wartościach logicznych procedura jest podobna: udowodnienie, że wartość boolowska of not .

Inne podejście wykorzystuje twierdzenie o odbiciu. Dla dowolnego skończonego zbioru aksjomatów istnieje dowód, że ten zbiór aksjomatów ma przeliczalny model przechodni. Dla danego skończonego zbioru z aksjomatów, nie jest skończonym zbiorem od aksjomatów takich, które dowodzi, że jeśli przechodnich policzalnych modeli spełnia , potem spełnia . Dowodząc, że jest skończony zestaw z aksjomatów takie, że jeśli przechodnich policzalnych modeli spełnia , wówczas spełnia hipotezę . Następnie dla danego skończonego zbioru z aksjomatów, dowodzi .

Czasami w (**) silniejsza teoria niż jest używana do dowodzenia . Następnie mamy dowód na spójność względem spójności . Zauważ, że , gdzie jest (aksjomat konstruowalności).

Zobacz też

Bibliografia

  • Bell, JL (1985). Modele o wartościach logicznych i dowody niezależności w teorii mnogości , Oxford. ISBN  0-19-853241-5
  • Cohen, PJ (1966). Teoria mnogości i hipoteza continuum . Addisona-Wesleya. Numer ISBN 978-0-8053-2327-6.
  • Grishin, VN (2001) [1994], "Forcing Method" , Encyklopedia Matematyki , EMS Press
  • Kunen, K. (1980). Teoria mnogości: wprowadzenie do dowodów niezależności . Północna Holandia. Numer ISBN 978-0-444-85401-8.
  • Jech, Tomasz (2002). Teoria mnogości: wydanie trzecie tysiąclecie . Wiosna-Verlag. Numer ISBN 3-540-44085-2.

Linki zewnętrzne