Stałe twierdzenia punktowe dla konstruktywnych przestrzeni metrycznych?

Twierdzenie Banacha o punkcie stałym mówi, że jeśli mamy niepustą pełną przestrzeń metryczną $A$ , 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 ) , $f : A \to A$$\mu(f)$$a \in A$$f$$a, f(a), f^2(a), f^3(a), \ldots$

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 $U$$U$$U$

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.

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ą „$\exists x \in A . \phi(x)$$x \in A$$\phi(x)$ $x \in A$ ”, który następnie wygląda jak zastosowanie wybranego aksjomatu.$\phi(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,d)$$f : M \to M$$f$$\alpha$$0 < \alpha < 1$$d(f(x), f(y)) \leq \alpha \cdot d(x,y)$$x, y \in M$.

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 ) $u$$v$$f$

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

Pozostaje udowodnić istnienie stałego punktu. Ze względu zamieszkuje istnieje x 0 ∈ M . Zdefiniuj sekwencję ( x i ) rekurencyjnie przez x i + 1 = f ( x i ) . Możemy udowodnić przez indukcję, że d ( x i , x i + 1 ) ≤ α i ⋅ d ( x 0 , x 1 ) . Z tego wynika, że$M$$x_0 \in M$$(x_i)$

$$x_{i+1} = f(x_i).$$ $d(x_i, x_{i+1}) \leq \alpha^i \cdot d(x_0, x_1)$ 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 $(x_i)$$M$$y = \lim_i x_i$$f$ Zatem y jest stałym punktem f . CO BYŁO DO OKAZANIA $$f(y) = f(\lim_i x_i) = \lim_i f(x_i) = \lim_i x_{i+1} = \lim_i x_i = y.$$ $y$$f$

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.$\alpha$$x_0$

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.$u$$v$$f$$\lnot\lnot (u = v)$$u = v$

3. $(x_i)$$x_0$$\exists x \in M . \top$$x_0$$M$

4. $M$$\exists x \in M . \top$$M$$\lnot\forall x \in M . \bot$

5. $\mathrm{fix}_M$$M$$M$$\forall\exists$

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ś.