Stałe twierdzenia punktowe dla konstruktywnych przestrzeni metrycznych?

15

Twierdzenie Banacha o punkcie stałym mówi, że jeśli mamy niepustą pełną przestrzeń metryczną ZA , wówczas każda jednorodnie kurcząca się funkcja ma unikalny punkt stały . Jednak dowód tego twierdzenia wymaga aksjomatu wyboru - musimy wybrać dowolny element aby rozpocząć iterację , aby uzyskać sekwencję Cauchyego . μ ( f ) a A f a , f ( a ) , f 2 ( a ) , f 3 ( a ) , fa:ZAZAμ(fa)zaZAfaza,fa(za),fa2)(za),fa3)(za),

  1. Jak sformułowane są twierdzenia o punkcie stałym w analizie konstruktywnej?
  2. Czy są też jakieś zwięzłe odniesienia do konstruktywnych przestrzeni metrycznych?

Pytam dlatego, że chcę skonstruować model Systemu F, w którym typy dodatkowo niosą między innymi strukturę metryczną. Przydatne jest to, że w konstruktywnej teorii zbiorów możemy ugotować rodzinę zbiorów , tak że jest zamknięte pod produktami, wykładnikami i rodzinami z indeksem , co ułatwia podanie modelu Systemu F.U UUUU

Byłoby bardzo miło, gdybym mógł przygotować podobną rodzinę konstrukcyjnych przestrzeni ultradźwiękowych. Ale ponieważ dodanie wyboru do konstruktywnej teorii zbiorów czyni ją klasyczną, oczywiście muszę bardziej uważać na twierdzenia o punkcie stałym i prawdopodobnie także inne rzeczy.

Neel Krishnaswami
źródło
2
Możesz zmienić hipotezę na będący zestawem zamieszkanym . Nie jesteś powołując aksjomat wyboru, aby wybrać się A . AaZA
Colin McQuillan,

Odpowiedzi:

22

Aksjomat wyboru jest używany, gdy istnieje zbiór „rzeczy” i wybierasz jeden element dla każdej „rzeczy”. Jeśli w kolekcji jest tylko jedna rzecz, to nie jest to aksjomat wyboru. W naszym przypadku mamy tylko jedną przestrzeń metryczną i „wybieramy” w niej punkt. Więc nie jest to aksjomat wyboru, ale eliminacji kwantyfikatorów egzystencjalnych, czyli mamy hipotezę i mówimy „niech x A będzie takie, że ϕ ( x ) ”. Niestety ludzie często mówią „xZA.ϕ(x)xZAϕ(x) xZA ”, który następnie wygląda jak zastosowanie wybranego aksjomatu.ϕ(x)

Dla porównania, tutaj jest konstruktywny dowód twierdzenia Banacha o punkcie stałym.

Twierdzenie: Skurcz na zamieszkanej pełnej przestrzeni metrycznej ma unikalny punkt stały.

Dowód. Załóżmy, że jest zamieszkaną pełną przestrzenią metryczną, a f : M M jest skurczem. Ponieważ f ma skurcz istnieje α takie, że 0 < α < 1 , a d ( f ( x ) , F ( y ) ) α d ( x , y ) dla każdego X , Y M(M.,re)fa:M.M.faα0<α<1re(fa(x),fa(y))αre(x,y)x,yM..

Załóżmy, że i v są stałym punktem f . Mamy zatem d ( u , v ) = d ( f ( u ) , f ( v ) ) α d ( u , v ), z którego wynika, że 0 d ( u , v ) ( α - 1 ) d ( u , v ) uvfa

re(u,v)=re(fa(u),fa(v))αre(u,v)
, a więc d ( u , v ) = 0 i U = V . Dowodzi to, że f ma co najwyżej jeden stały punkt.0re(u,v)(α-1)re(u,v)0re(u,v)=0u=vfa

Pozostaje udowodnić istnienie stałego punktu. Ze względu zamieszkuje istnieje x 0M . Zdefiniuj sekwencję ( x i ) rekurencyjnie przez x i + 1 = f ( x i ) . Możemy udowodnić przez indukcję, że d ( x i , x i + 1 ) α id ( x 0 , x 1 ) . Z tego wynika, żeM.x0M.(xja)

xja+1=fa(xja).
re(xja,xja+1)αjare(x0,x1) jest sekwencją Cauchy'ego. Ponieważ M jest zakończone, sekwencja ma granicę y = lim i x i . Ponieważ f jest skurczem, jest jednolicie ciągły i dlatego dojeżdża do granic sekwencji: f ( y ) = f ( lim i x i ) = lim i f ( x i ) = lim i x i + 1 = lim i x ja(xja)M.y=limjaxjafa Zatem y jest stałym punktem f . CO BYŁO DO OKAZANIA
fa(y)=fa(limjaxja)=limjafa(xja)=limjaxja+1=limjaxja=y.
yfa

Uwagi:

  1. Uważałem, aby nie powiedzieć „wybierz ” i „wybierz x 0 ”. Często mówi się takie rzeczy, a one tylko zwiększają zamieszanie, które uniemożliwia zwykłym matematykom stwierdzenie, co jest, a co nie jest aksjomatem wyboru.αx0

  2. W części dowodowej dotyczącej wyjątkowości ludzie często niepotrzebnie zakładają, że istnieją dwa różne punkty stałe i dochodzą do sprzeczności. W ten sposób udało im się tylko udowodnić, że jeśli i v są stałymi punktami f, to ¬ ¬ ( u = v ) . Więc teraz potrzebują wykluczonego środkowego, aby dostać się do u = v . Nawet w przypadku matematyki klasycznej jest to nieoptymalne i pokazuje tylko, że autor dowodu nie przestrzega dobrej logicznej higieny.uvfa¬¬(u=v)u=v

  3. (xja)x0xM..x0M.

  4. M.xM..M.¬xM..

  5. fajaxM.M.M.

  6. Wreszcie następujące twierdzenia o stałym punkcie mają konstruktywne wersje:

    • Twierdzenie Knastera-Tarskiego o punkcie stałym dla map monotonicznych na kompletnych sieciach
    • Twierdzenie Banacha o stałym punkcie dla skurczów w pełnej przestrzeni metrycznej
    • Twierdzenie Knastera-Tarskiego o punkcie stałym dla map monotonicznych na dcpos (udowodnione przez Pataraię)
    • Różne twierdzenia o stałym punkcie w teorii domen zwykle mają konstruktywne dowody
    • Twierdzenie o rekurencji jest formą twierdzenia o stałym punkcie i ma konstruktywny dowód
    • Udowodniłem, że twierdzenie Knastera-Tarskiego o punktach stałych dla map monotonicznych na zestawach pełnych łańcuchów nie ma konstruktywnego dowodu. Podobnie, twierdzenie Bourbaki-Witt o punkcie stałym dla map progresywnych na zestawach zakończonych łańcuchem zawodzi konstruktywnie. Kontrprzykład na późniejszy pochodzi ze skutecznych toposów: w efektywnych porządkach toposu (odpowiednio zdefiniowanych) tworzy się zestaw, a mapy następców są progresywne i nie mają stałych punktów. Nawiasem mówiąc, mapa następców na rzędnych nie jest monotonna w skutecznych toposach.

To więcej informacji, niż prosiłeś.

Andrej Bauer
źródło
1
Czy któryś z aksjomatów przestrzeni metrycznych wymaga przeformułowania?
Neel Krishnaswami,
to kolejna miła odpowiedź, Andrej!
Suresh Venkat,
1
@Neel: Nie, aksjomaty są takie same jak w klasycznym przypadku.
Andrej Bauer,
2
fajaxfajaxfajax
2
fajaxfajax=λM..λfa.fa(fajaxM.(fa))M.faM.M.