Teorema titik tetap untuk ruang metrik konstruktif?

Teorema titik tetap Banach mengatakan bahwa jika kita memiliki ruang metrik kosong yang tidak kosong , maka fungsi kontraktual yang seragam memiliki titik tetap unik . Namun, bukti teorema ini membutuhkan aksioma pilihan - kita perlu memilih elemen yang sewenang-wenang untuk memulai iterasi dari, untuk mendapatkan Cauchy urutan . f : A → A μ ( f ) a ∈ A f a , f ( a ) , f 2 ( a ) , f 3 ( a ) , $A$$f : A \to A$$\mu(f)$$a \in A$$f$$a, f(a), f^2(a), f^3(a), \ldots$

1. Bagaimana teorema titik tetap dinyatakan dalam analisis konstruktif?
2. Juga, adakah referensi ringkas untuk ruang metrik konstruktif?

Alasan saya bertanya adalah bahwa saya ingin membangun model Sistem F di mana jenis tambahan membawa struktur metrik (antara lain). Agak berguna bahwa dalam teori himpunan konstruktif, kita dapat memasak sekumpulan himpunan $U$ , sehingga $U$ ditutup di bawah produk, eksponensial, dan keluarga berindeks $U$ , yang membuatnya mudah untuk memberikan model Sistem F.

Akan sangat menyenangkan jika saya bisa memasak keluarga serupa ruang ultrametrik konstruktif. Tetapi karena menambahkan pilihan pada teori himpunan konstruktif menjadikannya klasik, jelas saya perlu lebih berhati-hati tentang teorema titik tetap, dan mungkin hal-hal lain juga.

Aksioma pilihan digunakan ketika ada koleksi "benda" dan Anda memilih satu elemen untuk setiap "benda". Jika hanya ada satu hal dalam koleksi, itu bukan aksioma pilihan. Dalam kasus kami, kami hanya memiliki satu ruang metrik dan kami "memilih" titik di dalamnya. Sehingga tidak aksioma pilihan selain penghapusan bilangan eksistensial, yaitu, kita memiliki hipotesis dan kita mengatakan "biarkan x ∈ A menjadi sedemikian rupa sehingga ϕ ( x ) ". Sayangnya, orang sering mengatakan "$\exists x \in A . \phi(x)$$x \in A$$\phi(x)$ $x \in A$ ", yang kemudian terlihat seperti penerapan aksioma pilihan.$\phi(x)$

Untuk referensi, berikut adalah bukti konstruktif dari teorema titik tetap Banach.

Teorema: Kontraksi pada ruang metrik lengkap yang dihuni memiliki titik tetap yang unik.

Bukti. Misalkan adalah ruang metrik lengkap yang dihuni dan f : M → M adalah kontraksi. Karena f adalah kontraksi ada α sehingga 0 < α < 1 dan d ( f ( x ) , f ( y ) ) ≤ α ⋅ d ( x , y ) untuk semua 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$.

Misalkan dan v adalah titik tetap f . Maka kita memiliki d ( u , v ) = d ( f ( u ) , f ( v ) ) ≤ α d ( u , v ) yang merupakan asal dari 0 ≤ d ( u , v ) ≤ ( α - 1 ) d ( u , v ) $u$$v$$f$

$$d(u,v) = d(f(u), f(v)) \leq \alpha d(u,v)$$ , maka d ( u , v ) = 0 dan u = v . Ini membuktikan bahwa f memiliki paling banyak satu titik tetap.$0 \leq d(u,v) \leq (\alpha - 1) d(u,v) \leq 0$$d(u,v) = 0$$u = v$$f$

Tetap membuktikan keberadaan titik tetap. Karena dihuni terdapat x 0 ∈ M . Tentukan urutan ( x i ) secara rekursif dengan x i + 1 = f ( x i ) . Kita dapat membuktikan dengan induksi bahwa d ( x i , x i + 1 ) ≤ α i ⋅ d ( x 0 , x 1 ) . Dari sini dapat disimpulkan$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)$ adalah urutan Cauchy. Karena M selesai, urutannya memiliki batas y = lim i x i . Karena f adalah kontraksi, maka kontinu seragam dan sehingga komutasi dengan batas urutan: 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$ Jadi y adalah titik tetap dari f . QED $$f(y) = f(\lim_i x_i) = \lim_i f(x_i) = \lim_i x_{i+1} = \lim_i x_i = y.$$ $y$$f$

Catatan:

1. Saya berhati-hati untuk tidak mengatakan "pilih " dan "pilih x 0 ". Adalah umum untuk mengatakan hal-hal seperti itu, dan mereka hanya menambah kebingungan yang mencegah matematikawan biasa untuk dapat mengetahui apa yang bisa dan tidak merupakan aksioma pilihan.$\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$

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

6. Akhirnya, teorema titik tetap berikut memiliki versi konstruktif:

   • Teorema titik tetap Knaster-Tarski untuk peta monoton pada kisi lengkap
   • Teorema titik tetap Banach untuk kontraksi pada ruang metrik lengkap
   • Teorema titik tetap Knaster-Tarski untuk peta monoton pada dcpos (dibuktikan oleh Pataraia)
   • Berbagai teorema titik-tetap dalam teori domain biasanya memiliki bukti konstruktif
   • Teoresi rekursi adalah bentuk teorema titik tetap dan memiliki bukti konstruktif
   • Saya membuktikan bahwa teorema titik tetap Knaster-Tarski untuk peta monoton pada poset rantai-lengkap tidak memiliki bukti konstruktif. Demikian pula, teorema titik tetap Bourbaki-Witt untuk peta progresif pada poset lengkap rantai gagal secara konstruktif. Contoh tandingan untuk yang berikutnya berasal dari topos efektif: dalam ordinal topos efektif (didefinisikan dengan tepat) membentuk satu set dan peta penerusnya progresif dan tidak memiliki titik tetap. Ngomong-ngomong, peta penerus pada ordinals bukanlah monoton dalam topos yang efektif.

Nah, itu lebih banyak informasi daripada yang Anda minta.