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.
Rys historyczny
Metoda 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 zastosował metodę forsingu iterowanego z nośnikami przeliczalnymi, aby wykazać niesprzeczność hipotezy Borela[7].
W okresie
1976
-
1978
Saharon Shelah
rozwinął 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
rozwinął teorię wokół forsingu
, który okazuje się być kluczowym elementem badań
struktury
przy założeniu
aksjomatu determinacji
w
(gdzie INS jest
ideałem
niestacjonarnych
podzbiorów ω1, a
jest rodziną zbiorów dziedzicznie
mocy
< ω2)[11].
Metoda działania: modele boole'owskie
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. 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
możemy myśleć jak o dużej
koniunkcji
po wszystkich możliwych x. Taka duża koniunkcja powinna się tłumaczyć na przekrój w algebrze Boole'a i to sugeruje, że powinniśmy ograniczyć się do takich algebr, w których istnieją wszystkie kresy górne i dolne. Jest jeszcze jeden wymagający omówienia szczegół techniczny: obliczając boole'owską wartość logiczną zdania
, będziemy redukować problem do wyznaczenia kresu dolnego
. Pytanie, jakie może powstać, dotyczy x, które powinny być brane pod uwagę. Okazuje się, że otrzymamy bardzo ładną i 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
α definujemy zbiory
złożone z termów boole'owskich rangi α:
,
gdy α jest liczbą
graniczną
,
jest zbiorem wszystkich
funkcji
t których
dziedzina
dom(t) jest podzbiorem
, a wartości należą do algebry
.
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 t, s):
,
.
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.)
I tak dochodzimy do sedna forsingu: rozważając zdanie
języka teorii mnogości, możemy 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.
Forsing w praktyce: roszerzenia modeli ZFC
Rozszerzenia generyczne
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 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
(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
- (i) G jest
filtrem
w
, tzn.
i
oraz
,- (ii) G jest V-zupełny, tzn. dla każdego zbioru
takiego, że
mamy
jeśli
, to
.Przypuśćmy
jest filtrem generycznym w algebrze
nad modelem
. Dla tego filtru definiujemy interpretację termów boole'owskich oraz model
:
- przez indukcje po randze termu
określamy
i
;- kładziemy
.
Okazuje się, że
,- dla każdej formuły
języka teorii mnogości oraz termów
mamy
wtedy i tylko wtedy gdy
,- w szczególności,
jest modelem ZFC.
Model
nazywany jest rozszerzeniem generycznym uniwersum V. Badania modeli tej postaci zastępują obliczanie wartości boole'owskich formuł.
Pojęcia forsingu
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ę
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
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
(czyt. p forsuje/wymusza
) wtedy i tylko wtedy, gdy 
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.
Przykłady zastosowań
- Używając forsingu można wykazać niezależność (od aksjomatów ZFC) następujących klasycznych zdań w teorii mnogości:
- Wyniki, które można zbiorowo opisać stwierdzeniem każde rozmieszczenie wartości
i
w
diagramie Cichonia
, które jest zgodne z nierównościami diagramu i dwoma dodatkowymi równościami jest niesprzeczne z ZFC były uzyskane przy użyciu forsingu. Pełny opis tych rezultatów jest przedstawiony w monografii
Tomka Bartoszyńskiego
i Haima Judaha [14]. - Innymi przykładami zastosowania forsingu mogą być następujące dwa wyniki, których sformułowanie powinno być zrozumiałe dla każdego matematyka:
- Możliwość znalezienia dla każdej funkcji
zbioru
, który nie jest
pierwszej kategorii
, takiego, że obcięcie
jest
ciągłe
jest niesprzeczne z ZFC. [15]. - Jest niesprzeczne z ZFC, że dla każdej funkcji
można znaleźć zbiór
który nie jest
miary zero
i taki, że obcięcie
jest ciągłe. [16].
Aksjomaty forsingowe
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[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.
Definicje
- Dla pojęcia forsingu
i liczby kardynalnej κ, niech
oznacza następujące zdanie:
- jeśli
jest rodziną gęstych podzbiorów
oraz
, - to istnieje filtr
który ma niepusty przekrój z każdym zbiorem z
(tzn
).
- Dla klasy
pojęć forsingu i liczby kardynalnej κ,
jest zdaniem
.
Uwagi
Należy zauważyć, że 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 Shelaha 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 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.
Bibliografia
- ↑ Cohen, Paul: The independence of the continuum hypothesis. "Proc. Nat. Acad. Sci. U.S.A." 50 (1963), s. 1143-1148.
- ↑ Cohen, Paul: The independence of the continuum hypothesis. II. "Proc. Nat. Acad. Sci. U.S.A." 51 (1964), s. 105-110.
- ↑ Cohen, Paul: Set theory and the continuum hypothesis. W. A. Benjamin, Inc., New York-Amsterdam, 1966.
- ↑ Cohen, Paul: The discovery of forcing. Rocky Mountain J. Math. 32 (2002), no. 4, s. 1071-1100
- ↑ Shoenfield, Joseph R.: Unramified forcing. "1971 Axiomatic Set Theory" (Proc. Sympos. Pure Math., Vol. XIII, Part I, Univ. California, Los Angeles, Calif., 1967), Amer. Math. Soc., Providence, R.I. s. 357-381
- ↑ Solovay, R. M.; Tennenbaum, S.: Iterated Cohen extensions and Souslin's problem. "Ann. of Math." (2) 94 (1971), s. 201-245.
- ↑ Laver, Richard: On the consistency of Borel's conjecture. "Acta Math." 137 (1976), nr 3-4, s. 151-169.
- ↑ Shelah, Saharon: Independence results. "J. Symbolic Logic" 45 (1980), nr 3, s. 563-573.
- ↑ Shelah, Saharon: Proper and improper forcing. "Perspectives in Mathematical Logic". Springer-Verlag, Berlin, 1998. .
- ↑ Goldstern, Martin: Tools for your forcing construction. Set theory of the reals (Ramat Gan, 1991), "Israel Math. Conf. Proc.", 6, Bar-Ilan Univ., Ramat Gan, 1993, s. 305-360.
- ↑ Woodin, W. Hugh: The axiom of determinacy, forcing axioms, and the nonstationary ideal. "de Gruyter Series in Logic and its Applications", 1. Walter de Gruyter & Co., Berlin, 1999.
- ↑ Guzicki, Wojciech; Zbierski, Paweł: Podstawy teorii mnogości. Państwowe Wydawnictwo Naukowe, Warszawa, 1978.
- ↑ Jech, Thomas: Set theory. The third millennium edition. "Springer Monographs in Mathematics". Springer-Verlag, Berlin, 2003.
- ↑ Bartoszyński, Tomek; Judah, Haim: Set theory. On the structure of the real line. A K Peters, Ltd., Wellesley, MA, 1995.
- ↑ Shelah, Saharon: Possibly every real function is continuous on a non-meagre set. "Publ. Inst. Math. (Beograd)" (N.S.) 57(71) (1995), s. 47-60.
- ↑ Rosłanowski, Andrzej; Shelah, Saharon: Measured creatures. "Israel J. Math." 151 (2006), s. 61-110.
- ↑ Kunen, Kenneth: Set theory. An introduction to independence proofs. "Studies in Logic and the Foundations of Mathematics", 102. North-Holland Publishing Co., Amsterdam-New York, 1980.
- ↑ Fremlin, David H.: Consequences of Martin's axiom. "Cambridge Tracts in Mathematics", 84. Cambridge University Press, Cambridge, 1984. .
Zobacz też