WikiDer > Барная индукция
Барная индукция это принцип рассуждения, используемый в интуиционистская математика, представлен Л. Э. Дж. Брауэр. Основное применение стержневой индукции - интуиционистский вывод теорема вентилятора, ключевой результат, использованный при выводе теорема о равномерной непрерывности.
Это также полезно в предоставлении конструктивных альтернатив другим классический полученные результаты.
Цель принципа - доказать свойства всех бесконечных последовательностей натуральных чисел (называемых последовательность выбора в интуиционистской терминологии), индуктивно сводя их к свойствам конечных списков. Индукцию с помощью стержня можно также использовать для доказательства свойств всех последовательность выбора в распространять (особый вид набор).
Определение
Учитывая последовательность выбора , любая конечная последовательность элементов этой последовательности называется начальный сегмент этой последовательности выбора.
В настоящее время в литературе существует три формы индукции столбцов, каждая из которых накладывает определенные ограничения на пару предикатов, а ключевые различия выделены жирным шрифтом.
Индукция разрешимого стержня (BID)
Учитывая два предиката и на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:
- каждая последовательность выбора содержит хотя бы один начальный сегмент, удовлетворяющий в какой-то момент (это выражается в том, что это бар);
- является разрешимый (т.е. наш бар разрешимый);
- каждая конечная последовательность, удовлетворяющая также удовлетворяет (так выполняется для любой последовательности выбора, начинающейся с вышеупомянутой конечной последовательности);
- если все расширения конечной последовательности одним элементом удовлетворяют , то эта конечная последовательность также удовлетворяет (иногда это называют существование восходящий наследственный);
то мы можем сделать вывод, что выполняется для пустой последовательности (т.е. A выполняется для всех последовательностей выбора, начинающихся с пустой последовательности).
Этот принцип индукции стержня одобрен в работах, A. S. Troelstra, С. К. Клини и Драгалин.
Индукция тонкого стержня (BIТ)
Учитывая два предиката и на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:
- каждая последовательность выбора содержит не менее уникальный начальный сегмент, удовлетворяющий в какой-то момент (т.е. наш бар тонкий);
- каждая конечная последовательность, удовлетворяющая также удовлетворяет ;
- если все расширения конечной последовательности одним элементом удовлетворяют , то эта конечная последовательность также удовлетворяет ;
то мы можем сделать вывод, что выполняется для пустой последовательности.
Этот принцип индукции стержня одобрен в работах Джоан Мощовакис и (интуитивно) доказуемо эквивалентен разрешимой индукции стержня.
Монотонная индукция стержня (BIM)
Учитывая два предиката и на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:
- каждая последовательность выбора содержит хотя бы один начальный сегмент, удовлетворяющий в какой-то момент;
- когда конечная последовательность удовлетворяет , то каждое возможное расширение этой конечной последовательности также удовлетворяет (т.е. наш бар монотонный);
- каждая конечная последовательность, удовлетворяющая также удовлетворяет ;
- если все расширения конечной последовательности одним элементом удовлетворяют , то эта конечная последовательность также удовлетворяет ;
то мы можем сделать вывод, что выполняется для пустой последовательности.
Этот принцип индукции стержня используется в работах A. S. Troelstra, С. К. Клини, Драгалин и Джоан Мощовакис. Обычно это происходит из индукции тонких стержней или монотонных стержней. (Даммит 1977)
Связь между этими схемами и другой информацией
Следующие результаты об этих схемах могут быть интуитивно доказано:
(Символ "" это "турникет".
Неограниченная индукция стержня
Дополнительная схема индукции стержня была первоначально дана в виде теоремы Брауэр (1975), не содержащие «лишних» ограничений на R под названием Теорема бара. Однако доказательство этой теоремы было ошибочным, и неограниченная индукция стержня не считается интуиционистски обоснованной (см. Dummett 1977, стр. 94–104, где объясняется, почему это так). Схема неограниченного индукционного стержня приведена ниже для полноты картины.
Учитывая два предиката и на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:
- каждая последовательность выбора содержит хотя бы один начальный сегмент, удовлетворяющий в какой-то момент;
- каждая конечная последовательность, удовлетворяющая также удовлетворяет ;
- если все расширения конечной последовательности одним элементом удовлетворяют , то эта конечная последовательность также удовлетворяет ;
то мы можем сделать вывод, что выполняется для пустой последовательности.
Отношения к другим полям
В классическом обратная математика, "барная индукция" () обозначает связанный принцип, утверждающий, что если отношение это в порядке, то у нас есть схема трансфинитная индукция над для произвольных формул.
Рекомендации
- Л. Э. Дж. Брауэр Брауэр, Л. Э. Дж. Собрание сочинений, Vol. I, Амстердам: Северная Голландия (1975).
- Драгалин, А.Г. (2001) [1994], «Барная индукция», Энциклопедия математики, EMS Press
- Майкл Даммит, Элементы интуиционизма, Clarendon Press (1977)
- С. К. Клини, Р. Э. Веслей, Основы интуиционистской математики: особенно в отношении рекурсивных функций, Северная Голландия (1965)
- Майкл Ратьен, Роль параметров в линейке и индукции стержня, Журнал символической логики 56 (1991), вып. 2. С. 715–730.
- A. S. Troelstra, Последовательности выбора, Clarendon Press (1977)
- A. S. Troelstra и Дирк Ван Дален, Конструктивизм в математике, исследования по логике и основам математики, Эльзевир (1988)
Этот логика-связанная статья является заглушка. Вы можете помочь Википедии расширяя это. |