WikiDer > Барная индукция

Bar induction

Барная индукция это принцип рассуждения, используемый в интуиционистская математика, представлен Л. Э. Дж. Брауэр. Основное применение стержневой индукции - интуиционистский вывод теорема вентилятора, ключевой результат, использованный при выводе теорема о равномерной непрерывности.

Это также полезно в предоставлении конструктивных альтернатив другим классический полученные результаты.

Цель принципа - доказать свойства всех бесконечных последовательностей натуральных чисел (называемых последовательность выбора в интуиционистской терминологии), индуктивно сводя их к свойствам конечных списков. Индукцию с помощью стержня можно также использовать для доказательства свойств всех последовательность выбора в распространять (особый вид набор).

Определение

Учитывая последовательность выбора , любая конечная последовательность элементов этой последовательности называется начальный сегмент этой последовательности выбора.

В настоящее время в литературе существует три формы индукции столбцов, каждая из которых накладывает определенные ограничения на пару предикатов, а ключевые различия выделены жирным шрифтом.

Индукция разрешимого стержня (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)