Loading AI tools
metoda dowodu w teorii mnogości Z Wikipedii, wolnej encyklopedii
Forsing (forcing) – metoda dowodzenia niesprzeczności i niezależności zdań teorii mnogości względem aksjomatów Zermela-Fraenkla. Forsing to jedna z metod używanych w matematyce do ścisłego udowodnienia, że pewnych stwierdzeń nie można ani udowodnić, ani obalić (ten ostatni termin oznacza udowodnienie zaprzeczenia).
Polska terminologia w teorii forsingu nie jest jednoznacznie ustalona, chociaż polskojęzyczni matematycy mieli (i mają) wkład w rozwój tej teorii. Angielskie zwroty forcing i forcing relation tłumaczone są jako forsing, forcing, wymuszanie oraz relacja forsingu, relacja forcingu lub relacja wymuszania. W tym artykule zastosowano fonetyczną interpretację nazewnictwa angielskiego.
Metodę forsingu stworzył Paul Cohen na przełomie lat 1963 i 1964[1][2][3][4]. Pierwszym jej zastosowaniem był dowód, że zarówno aksjomat wyboru, jak i hipoteza continuum, są niezależne od aksjomatów ZF. Oryginalna metoda użyta przez Cohena była dużo bardziej skomplikowana niż forsing używany dzisiaj. Rozwój współczesnego forsingu (tzw. unramified forcing) datuje się od pracy Josepha Shoenfielda[5].
Około roku 1965 amerykańscy matematycy Robert Solovay i Stanley Tennenbaum rozwinęli metodę forsingu, wprowadzając forsing iterowany, aby udowodnić niezależność hipotezy Suslina[6]. We współczesnej terminologii metoda wprowadzona przez Solovaya i Tennenbauma to forsing iterowany z nośnikami skończonymi.
W 1976 amerykański matematyk Richard Laver zastosował metodę forsingu iterowanego z nośnikami przeliczalnymi, aby wykazać niesprzeczność hipotezy Borela[7]. W okresie 1976–1978 Saharon Szelach rozwinął teorię forsingów właściwych[8], która dzisiaj jest najbardziej rozwiniętą i najczęściej stosowaną częścią teorii iterowanego forsingu[9][10].
W latach 90. XX wieku W. Hugh Woodin rozwinął teorię wokół forsingu który okazuje się być kluczowym elementem badań struktury przy założeniu aksjomatu determinacji w (gdzie jest ideałem niestacjonarnych podzbiorów a jest rodziną zbiorów dziedzicznie mocy )[11].
Poniżej przedstawione zostało, w formie szkicu, omówienie jednego ze sposobów wprowadzania i interpretacji forsingu. Wywody te nie są ani kompletne, ani całkowicie poprawne – ze względu na jasność ekspozycji trzeba było zrezygnować z części szczegółów technicznych[12].
W przypadku, gdy dokonuje się wartościowania zdań rachunku kwantyfikatorów, używanie dwóch wartości logicznych nie jest owocne. Jeśli jesteśmy zainteresowani zdaniami języka (pierwszego rzędu) teorii mnogości, to możemy wartościować zdania w pewnej algebrze Boole’a. Użycie algebry Boole’a pozwala na naturalne obchodzenie się ze spójnikami logicznymi, dalej jednak istnieje problem kwantyfikatorów, który można rozwiązać następująco: o kwantyfikatorze ogólnym możemy myśleć jak o dużej koniunkcji po wszystkich możliwych Taka duża koniunkcja powinna się tłumaczyć na przekrój w algebrze Boole’a i to sugeruje, że należy ograniczyć się do takich algebr, w których istnieją wszystkie kresy dolne i górne. Ponadto obliczając boole’owską wartość logiczną zdania należy redukować problem do wyznaczenia kresu dolnego Pytanie, jakie może powstać, dotyczy które powinny być brane pod uwagę. Okazuje się, że otrzymamy użyteczną teorię, jeśli ograniczymy się do tzw. termów boole’owskich.
Spróbujmy nieco sformalizować idee przedstawione wyżej.
Niech będzie zupełną algebrą Boole’a. Przez indukcję po wszystkich liczbach porządkowych definiujemy zbiory złożone z termów boole’owskich rangi
Kładziemy też
Następnie, dla formuł języka teorii mnogości z parametrami definiujemy wartość boole’owską Zaczynamy od wartości boole’owskich formuł atomowych (tutaj mamy do czynienia z indukcją po randze termów boole’owskich ):
Teraz, przez indukcję po złożoności formuł, definiujemy wartość boole’owską dla bardziej skomplikowanych formuł:
Okazuje się, że jeśli jest jednym z aksjomatów ZFC, to Co więcej, jeśli istnieje dowód zdania w oparciu o aksjomaty ZFC, to Podobnie, jeśli istnieje dowód negacji w oparciu o aksjomaty ZFC, to (Te stwierdzenia są twierdzeniami teorii ZFC).
Rozważając zdanie języka teorii mnogości, można dla dowolnej algebry Boole’a wyznaczyć wartość boole’owską Jeśli dla pewnej algebry odkryjemy, że jest 1 (jedynką algebry), to nasze zdanie jest niesprzeczne z ZFC (tzn. nie można udowodnić jego zaprzeczenia). Jeśli zauważymy, że to nasze zdanie nie może być twierdzeniem ZFC. Oczywiście, gdy to nasze zdanie nie może być ani udowodnione, ani odrzucone.
W praktyce matematycznej obliczanie wartości formuł okazuje się zwykle być zajęciem dość skomplikowanym. Łatwiej jest nam myśleć o formułach jako zdaniach opisujących pewną rzeczywistość (choćby idealną), niż traktować je jako czysto formalne napisy. Z tego powodu w zastosowaniach forsingu najczęściej używane jest podejście semantyczne. To podejście, używające generycznych rozszerzeń modeli teorii mnogości może być całkowicie sformalizowane i poprawne, często budzi jednak pewne opory u adeptów forsingu (być może jest to spowodowane przez typowe rozpoczęcie rozważań od niech będzie przeliczalnym tranzytywnym modelem dostatecznie dużego fragmentu ZFC). Należy jednak podkreślić, że wszystkie argumenty używające języka rozszerzeń generycznych mogą być przetłumaczone na obliczenia pewnych wartości boole’owskich (sama możliwość takiego przetłumaczenia jest dla specjalistów wystarczająca i nikt tego w praktyce nie robi).
Tak jak w sekcji wcześniejszej, nasze rozważania tutaj mają charakter szkicu tylko i nie są całkowicie poprawne ani kompletne. Czytelnika zainteresowanego tematem odsyłamy do cytowanej wcześniej literatury.
Załóżmy, że (tranzytywne) uniwersum teorii mnogości V jest zanurzone w większym (tranzytywnym) uniwersum (tzn. ). Niech będzie zupełną (z punktu widzenia uniwersum V) algebrą Boole’a. Powiemy, że zbiór należący do jest filtrem generycznym w algebrze nad modelem , jeśli
Przypuśćmy jest filtrem generycznym w algebrze nad modelem Dla tego filtru definiujemy interpretację termów boole’owskich oraz model
Okazuje się, że
Model nazywany jest rozszerzeniem generycznym uniwersum V. Badania modeli tej postaci zastępują obliczanie wartości boole’owskich formuł.
Pozostaje jeszcze jeden aspekt forsingu, związany z odpowiedzią na pytanie skąd się biorą rozważane zupełne algebry Boole’a? Algebry Boole’a używane w dowodach niesprzecznościowych są zwykle powiązane bezpośrednio ze zdaniem, którego niesprzeczność ma być udowodniona. Często to zdanie postuluje istnienie pewnego obiektu dla którego rozważa się przybliżenia przez obiekty mniejsze. Zwykle zbiór tych przybliżeń ma naturalną strukturę częściowego porządku lub, w najogólniejszym przypadku, przynajmniej praporządku. Tak otrzymujemy dużą część pojęć forsingu używanych w teorii mnogości. Każde pojęcie forsingu związane jest z pewną zupełną algebrą Boole’a i to jest właśnie źródło badanych algebr.
Należy zauważyć, że jeśli pojęcie forsingu jest separatywnym porządkiem częściowym, to może być ono traktowane bezpośrednio jako gęsty podzbiór algebry zupełnej (W ogólnym przypadku należy najpierw dokonać pewnych utożsamień). Wówczas elementy naszego pojęcia forsingu są również elementami algebry Boole’a i możemy porównywać je do wartości boole’owskich formuł, a także pytać czy należą one do filtru generycznego. Z rozważaniami tego typu związana jest relacja forsingu (zwana też relacją wymuszania). Przypuśćmy, że jest formułą języka teorii mnogości, są termami boole’owskimi oraz Definiujemy wówczas
Warto zauważyć, że wtedy i tylko wtedy, gdy dla każdego filtru generycznego nad V takiego, że mamy
W rozumowaniach forsingowych często jako narzędzia używa się relacji W niektórych prezentacjach teorii forsingu ta właśnie relacja, a nie model boole’owski, jest punktem wyjścia do rozwinięcia teorii.
Metoda forsingu i jej stosowanie mogą być dość skomplikowane, dlatego wielu matematyków woli swoje rozumowania opierać na tzw. aksjomatach forsingowych. Aksjomaty forsingowe to zdania matematyczne, które postulują istnienie obiektów zbliżonych do filtrów generycznych. Pierwszym (i chyba najbardziej popularnym) aksjomatem forsingowym był aksjomat Martina.
Źródło popularności aksjomatów forsingowych tkwi w możliwości wyeliminowania dość skomplikowanych dowodów niesprzeczności pewnych stwierdzeń przy użyciu forsingu iterowanego. Mają więc one pewne znaczenie dydaktyczne jako wprowadzenie do metody forsingu[16] oraz praktyczne jako narzędzie dla matematyków nie zaznajomionych z metodą forsingu[17]. Oczywiście za każdym aksjomatem forsingowym (a ściśle mówiąc jego niesprzecznością) stoją dość głębokie rozumowania w teorii forsingu iterowanego.
Na mocy klasycznego lematu Heleny Rasiowej i Romana Sikorskiego jest prawdziwe (w ZFC). Można też wykazać, że jeśli jest porządkiem bezatomowym i separatywnym, to jest zdaniem fałszywym (w ZFC).
Jeśli CCC oznacza klasę wszystkich porządków częściowych spełniających ccc, to aksjomat Martina jest zdaniem Aksjomat był uogólniony przez Szelacha do PFA.
Należy zauważyć, że w literaturze matematycznej istnieją pewne rozbieżności dotyczące terminologii związanej z aksjomatami forsingowymi. Niektórzy autorzy rezerwują nazwę aksjomat Martina i symbol dla a dla pozostałych przypadków używają oznaczenia Istnieją również pewne niekonsekwencje w formułowaniu definicji i roli liczby Czasami jest rozumiany jako tzn. postulat istnienia filtru przecinającego zadane zbiorów gęstych.
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.