|
|||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||
Forsing (ang. forcing) – metoda dowodzenia niesprzeczności i niezależności zdań teorii mnogości względem aksjomatów Zermelo-Fraenkela. Można powiedzieć, że forsing to jedna z metod używanych w matematyce, aby ściśle udowodnić że pewnych stwierdzeń nie można udowodnić ani obalić (ten ostatni termin oznacza udowodnienie zaprzeczenia). Należy zauważyć, że polska terminologia w teorii forsingu nie jest jednoznacznie ustalona, chociaż polskojęzyczni matematycy mieli (i mają) bardzo poważny 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.
edytuj Rys historycznyMetoda forsingu została odkryta przez Paula Cohena w 1963/64[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 stosuje metodę forsingu iterowanego z nośnikami przeliczalnymi, aby wykazać niesprzeczność hipotezy Borela[7]. W okresie 1976-1978 Saharon Shelah rozwija teorię forsingów proper (ang. proper forcing; dosł. forsing właściwy)[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 rozwija teorię wokół forsingu edytuj Metoda działania: modele boole'owskiePoniż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. Czytelnika zainteresowanego głębszym zrozumieniem tej tematyki odsyłamy do książki Wojciecha Guzickiego i Pawła Zbierskiego[12] lub monografii Thomasa Jecha[13]. W matematyce jesteśmy przyzwyczajeni do używania dwóch wartości logicznych dla zdań: 0 (fałsz) oraz 1 (prawda). Są też rozważane logiki wielowartościowe, ale jeśli chcemy dokonywać wartościowania zdań rachunku kwantyfikatorów, to wspomniane metody nie należą do owocnych. Jeśli jesteśmy zainteresowani zdaniami języka (pierwszego rzędu) teorii mnogości, to możemy pokusić się o wartościowanie zdań 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 Spróbujmy nieco sformalizować idee przedstawione wyżej. Niech
Kładziemy też Następnie, dla formuł
Teraz, przez indukcję po złożoności formuł, definiujemy wartość boole'owską dla bardziej skomplikowanych formuł:
Okazuje się, że jeśli I tak dochodzimy do sedna forsingu: rozważając zdanie edytuj Forsing w praktyce: roszerzenia modeli ZFCedytuj Rozszerzenia generyczneW 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 N 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
oraz ,
, to .Przypuśćmy
i ;
Okazuje się, że
wtedy i tylko wtedy gdy ,
Model edytuj Pojęcia forsinguPozostaje 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ę porządku częściowego 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
Warto zauważyć, że W rozumowaniach forsingowych często jako narzędzia używa się relacji edytuj Przykłady zastosowań
edytuj Aksjomaty forsingoweMetoda 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[17] oraz praktyczne jako narzędzie dla matematyków nie zaznajomionych z metodą forsingu[18]. 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. edytuj Definicje
edytuj UwagiNależy zauważyć, że na mocy klasycznego lematu Heleny Rasiowej i Romana Sikorskiego Jeśli CCC oznacza klasę wszystkich porządków częściowych spełniających ccc, to aksjomat Martina jest zdaniem 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 MAκ dla MAκ(CCC), a dla pozostałych przypadków używają oznaczenia FAκ. Istnieją również pewne niekonsekwencje w formułowaniu definicji i roli liczby κ. Czasami MAκ jest rozumiany jako MA < κ, tzn. postulat istnienia filtru przecinającego zadane < κ zbiorów gęstych. edytuj Bibliografia
edytuj Zobacz też |
| All Right Reserved © 2007, Designed by Stylish Blog. |