Fixpunktsätze für konstruktive metrische Räume?

Banachs Fixpunktsatz besagt, dass, wenn wir einen nicht leeren vollständigen metrischen Raum $A$ , jede gleichmäßig kontrahierende Funktion $f : A \to A$ einen eindeutigen Fixpunkt $\mu(f)$ . Der Beweis dieses Theorems erfordert jedoch das Axiom der Wahl - wir müssen ein beliebiges Element wählen $a \in A$, um mit der Iteration von $f$ zu beginnen und die Cauchy-Folge $a, f(a), f^2(a), f^3(a), \ldots$ .

1. Wie werden Fixpunktsätze in der konstruktiven Analyse formuliert?
2. Gibt es auch prägnante Verweise auf konstruktive metrische Räume?

Der Grund, den ich frage, ist, dass ich ein Modell von System F konstruieren möchte, in dem die Typen (unter anderem) zusätzlich eine metrische Struktur aufweisen. Es ist ziemlich nützlich, dass wir in der konstruktiven Mengenlehre eine Familie von Mengen , so dass U unter Produkten, Exponentialen und U- indizierten Familien geschlossen ist, was es einfach macht, ein Modell von System F zu geben.$U$$U$$U$

Es wäre sehr schön, wenn ich eine ähnliche Familie konstruktiver ultrametrischer Räume zusammenstellen könnte. Aber da die konstruktive Mengenlehre durch das Hinzufügen von Wahlmöglichkeiten klassischer wird, muss ich natürlich vorsichtiger mit Fixpunkt-Theoremen umgehen, und wahrscheinlich auch mit anderen Dingen.

Das Axiom der Wahl wird verwendet, wenn es eine Sammlung von "Dingen" gibt und Sie für jedes "Ding" ein Element auswählen. Wenn es nur eine Sache in der Sammlung gibt, ist das nicht das Axiom der Wahl. In unserem Fall haben wir nur einen metrischen Raum und "wählen" einen Punkt darin. So dass nicht das Axiom der Wahl ist , aber Beseitigung der Existenzquantoren, das heißt, wir haben eine Hypothese und wir sagen "lass x ∈ A so sein, dass ϕ ( x ) ". Leider sagen die Leute oft "$\exists x \in A . \phi(x)$$x \in A$$\phi(x)$ $x \in A$ ", was dann aussieht wie die Anwendung des Axioms der Wahl.$\phi(x)$

Als Referenz ist hier ein konstruktiver Beweis für Banachs Fixpunktsatz.

Satz: Eine Kontraktion auf einen bewohnten vollständigen metrischen Raum hat einen eindeutigen Fixpunkt.

Beweis. Angenommen ist ein bewohnter vollständiger metrischer Raum und f : M → M ist eine Kontraktion. Da f eine Kontraktion gibt es existiert α , so dass 0 < α < 1 und D ( f ( x ) , f ( y ) ) ≤ α ⋅ d ( x , y ) für alle 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$.

Angenommen, und v sind ein fester Punkt von f . Dann gilt d ( u , v ) = d ( f ( u ) , f ( v ) ) ≤ α d ( u , v ), woraus folgt, dass 0 ≤ d ( u , v ) ≤ ( α - 1 ) d $u$$v$$f$

$$d(u,v) = d(f(u), f(v)) \leq \alpha d(u,v)$$ , daher ist d (. Dies beweist, dass f höchstens einen festen Punkt hat.$0 \leq d(u,v) \leq (\alpha - 1) d(u,v) \leq 0$ und u = $d(u,v) = 0$$u = v$$f$

Es bleibt zu beweisen, dass es einen festen Punkt gibt. Da bewohnt existiert x 0 ∈ M . Definieren Sie die Folge ( x i ) rekursiv durch x i + 1 = f ( x i ) . Wir können durch Induktion beweisen, dass d ( x i , x i + 1 ) ≤ α i ⋅ d ( x 0 , ( x i$M$$x_0 \in M$$(x_i)$

$$x_{i+1} = f(x_i).$$ . Daraus folgt das$d(x_i, x_{i+1}) \leq \alpha^i \cdot d(x_0, x_1)$$(x_i)$ist eine Cauchy-Sequenz. Da vollständig ist, hat die Folge eine Grenze y = lim i x i . Da f eine Kontraktion ist, ist es gleichförmig kontinuierlich und so pendelt er mit Grenzen von Sequenzen: f ( y ) = f ( lim i x i ) = lim i f ( x i ) = lim i x i + 1 = lim = y . Also ist y ein Fixpunkt von$M$$y = \lim_i x_i$$f$ $$f(y) = f(\lim_i x_i) = \lim_i f(x_i) = \lim_i x_{i+1} = \lim_i x_i = y.$$ $y$ . QED$f$

Bemerkungen:

1. Ich habe darauf geachtet, nicht "wähle " und "wähle x 0 " zu sagen . Es ist üblich, solche Dinge zu sagen, und sie tragen nur zu der Verwirrung bei, die normale Mathematiker daran hindert, zu erkennen, was das Axiom der Wahl ist und was nicht.$\alpha$$x_0$

2. $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$ ) äquivalent. Ersteres ist konstruktiv sinnvoller und sinnvoll.

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

6. Schließlich haben die folgenden Fixpunktsätze konstruktive Versionen:

   • Knaster-Tarski-Fixpunktsatz für monotone Karten auf vollständigen Gittern
   • Banachs Fixpunktsatz für Kontraktionen auf einem vollständigen metrischen Raum
   • Knaster-Tarski-Fixpunktsatz für monotone Karten auf dcpos (von Pataraia bewiesen)
   • Verschiedene Fixpunktsätze in der Domänentheorie haben in der Regel konstruktive Beweise
   • Der Rekursionssatz ist eine Form des Fixpunktsatzes und hat einen konstruktiven Beweis
   • Ich beweisen , dass Knaster-Tarski-Punkt festen Satz für monotone Karten auf Ketten komplette posets hat nicht einen konstruktiven Beweis hat. In ähnlicher Weise versagt der Bourbaki-Witt-Fixpunktsatz für Progressive Maps auf kettenvollständigen Posets konstruktiv. Das Gegenbeispiel für das spätere ergibt sich aus den effektiven Topos: In den effektiven Topos bilden Ordinalzahlen (entsprechend definiert) eine Menge und die Nachfolgemaps sind progressiv und haben keine Fixpunkte. Übrigens ist die Nachfolgerkarte auf den Ordnungszahlen in den effektiven Topos nicht monoton.

Das sind eher mehr Informationen, als Sie verlangt haben.