Теорема Банаха о неподвижной точке говорит, что если у нас есть непустое полное метрическое пространство , то любая равномерно сжимающая функция имеет единственную неподвижную точку . Однако доказательство этой теоремы требует аксиомы выбора - нам нужно выбрать произвольный элемент чтобы начать итерацию , чтобы получить последовательность Коши . f : A → A μ ( f ) a ∈ A f a , f ( a ) , f 2 ( a ) , f 3 ( a ) , …
- Как формулируются теоремы о неподвижной точке в конструктивном анализе?
- Кроме того, есть ли краткие ссылки на конструктивные метрические пространства?
Причина, по которой я спрашиваю, состоит в том, что я хочу построить модель Системы F, в которой типы дополнительно несут метрическую структуру (среди прочего). Весьма полезно, что в конструктивной теории множеств мы можем составить семейство множеств , такое, что замкнуто относительно произведений, экспонент и семейств, индексированных по , что упрощает создание модели системы F.U U
Было бы очень хорошо, если бы я мог создать аналогичное семейство конструктивных ультраметрических пространств. Но поскольку добавление выбора в конструктивную теорию множеств делает ее классической, очевидно, мне нужно быть более осторожным в отношении теорем о неподвижной точке и, возможно, других вещей.
Ответы:
Аксиома выбора используется, когда существует набор «вещей», и вы выбираете один элемент для каждой «вещи». Если в коллекции есть только одна вещь, это не аксиома выбора. В нашем случае у нас есть только одно метрическое пространство, и мы «выбираем» точку в нем. Так что это не аксиома выбора, а исключение экзистенциальных кванторов, т. Е. У нас есть гипотеза и мы говорим "пусть таково, что ". К сожалению, люди часто говорят « выберите такой что », что тогда выглядит как применение аксиомы выбора.x ∈ A ϕ ( x ) x ∈ A ϕ ( x )∃ х ∈ . ϕ ( x ) x ∈ A ϕ ( x ) x ∈ A ϕ ( x )
Для справки приведем конструктивное доказательство теоремы Банаха о неподвижной точке.
Теорема: сжатие на обитаемом полном метрическом пространстве имеет единственную неподвижную точку.
Доказательство. Предположим, что - обитаемое полное метрическое пространство, а - сжатие. Поскольку является сокращением, существует такое, что и для всех ,f : M → M f α 0 < α < 1 d ( f ( x ) , f ( y ) ) ≤ α ⋅ d ( x , y ) x , y ∈ M( М, д) е: M→ М е α 0 < α < 1 d( ф( х ) , ф( у) ) ≤ α ⋅ d( х , у) х , у∈ M
Предположим, что и - фиксированная точка . Тогда имеем из чего следует, что , следовательно, и . Это доказывает, что имеет не более одной фиксированной точки.v f d ( u , v ) = d ( f ( u ) , f ( v ) ) ≤ α d ( u , v ) 0 ≤ d ( u , v ) ≤ ( α - 1 ) d ( u , v ) ≤ 0 d ( u , v ) = 0 uU v е
Осталось доказать существование неподвижной точки. Поскольку населен существует . Определите последовательность рекурсивно с помощьюПо индукции мы можем доказать, что . Отсюда следует, что - последовательность Коши. Поскольку завершена, последовательность имеет предел . Поскольку - сокращение, оно равномерно непрерывно и поэтому коммутирует с пределами последовательностей: Таким образом, является фиксированной точкойx 0 ∈ M ( x i ) x i + 1 = f ( x i ) . d ( x i , x i + 1 ) ≤ α i ⋅ d ( x 0 , x 1 ) ( x i ) M y = lim i x i f f ( y ) = f (M x0∈M (xi)
Примечания:
Я был осторожен, чтобы не сказать «выбрать » и «выбрать ». Такие вещи часто говорят, и они только добавляют путаницы, которая мешает обычным математикам определять, что является аксиомой выбора, а что нет.α x0
В части единственности доказательства люди часто без необходимости предполагают, что существуют две разные фиксированные точки, и получают противоречие. Таким образом, им удалось только доказать, что если и являются неподвижными точками то . Так что теперь им нужно исключить середину, чтобы добраться до . Даже для классической математики это неоптимально и просто показывает, что автор доказательства не придерживается хорошей логической гигиены.u v f ¬¬(u=v) u=v
В доказательственной части доказательства последовательность зависит от экзистенциального свидетеля мы получим, исключив предположение . Там нет ничего плохого. Мы делаем такие вещи постоянно. Мы ничего не выбрали. Подумайте об этом так: кто-то еще дал нам свидетельство о населенности , и мы можем что-то с этим сделать.(xi) x0 ∃x∈M.⊤ x0 M
Классически « обитаем» ( ) и « непусто» ( ) эквивалентны. Конструктивно первое имеет больше смысла и полезно.∃ х ∈ М . ⊤ М ¬ ∀ х ∈ М . ⊥M ∃x∈M.⊤ M ¬∀x∈M.⊥
Поскольку мы показали уникальность фиксированных точек, мы фактически получаем оператор с фиксированными точками из сокращений в точки , а не просто оператор . MM∀∃fixM M M ∀∃
Наконец, следующие теоремы о неподвижной точке имеют конструктивные версии:
Теперь это гораздо больше информации, чем вы просили.
источник