Барная индукция - Bar induction

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

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

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

Определение

Учитывая последовательность выбора ${displaystyle x_{0},x_{1},x_{2},x_{3},ldots }$, любая конечная последовательность элементов ${displaystyle x_{0},x_{1},x_{2},x_{3},ldots ,x_{i}}$ этой последовательности называется начальный сегмент этой последовательности выбора.

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

Индукция разрешимого стержня (BI_D)

Учитывая два предиката ${displaystyle R}$ и ${displaystyle A}$ на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:

• каждая последовательность выбора содержит хотя бы один начальный сегмент, удовлетворяющий ${displaystyle R}$ в какой-то момент (это выражается в том, что ${displaystyle R}$ это бар);
• ${displaystyle R}$ является разрешимый (т.е. наш бар разрешимый);
• каждая конечная последовательность, удовлетворяющая ${displaystyle R}$ также удовлетворяет ${displaystyle A}$ (так ${displaystyle A}$ выполняется для любой последовательности выбора, начинающейся с вышеупомянутой конечной последовательности);
• если все расширения конечной последовательности одним элементом удовлетворяют ${displaystyle A}$, то эта конечная последовательность также удовлетворяет ${displaystyle A}$ (иногда это называют ${displaystyle A}$ существование восходящий наследственный);

то мы можем сделать вывод, что ${displaystyle A}$ выполняется для пустой последовательности (т.е. A выполняется для всех последовательностей выбора, начинающихся с пустой последовательности).

Этот принцип индукции стержня одобрен в работах, A. S. Troelstra, С. К. Клини и Драгалин.

Индукция тонкого стержня (BI_Т)

Учитывая два предиката ${displaystyle R}$ и ${displaystyle A}$ на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:

• каждая последовательность выбора содержит не менее уникальный начальный сегмент, удовлетворяющий ${displaystyle R}$ в какой-то момент (т.е. наш бар тонкий);
• каждая конечная последовательность, удовлетворяющая ${displaystyle R}$ также удовлетворяет ${displaystyle A}$;
• если все расширения конечной последовательности одним элементом удовлетворяют ${displaystyle A}$, то эта конечная последовательность также удовлетворяет ${displaystyle A}$;

то мы можем сделать вывод, что ${displaystyle A}$ выполняется для пустой последовательности.

Этот принцип индукции стержня одобрен в работах Джоан Мощовакис и (интуитивно) доказуемо эквивалентен разрешимой индукции стержня.

Монотонная индукция стержня (BI_M)

Учитывая два предиката ${displaystyle R}$ и ${displaystyle A}$ на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:

• каждая последовательность выбора содержит хотя бы один начальный сегмент, удовлетворяющий ${displaystyle R}$ в какой-то момент;
• когда конечная последовательность удовлетворяет ${displaystyle R}$, то каждое возможное расширение этой конечной последовательности также удовлетворяет ${displaystyle R}$ (т.е. наш бар монотонный);
• каждая конечная последовательность, удовлетворяющая ${displaystyle R}$ также удовлетворяет ${displaystyle A}$;
• если все расширения конечной последовательности одним элементом удовлетворяют ${displaystyle A}$, то эта конечная последовательность также удовлетворяет ${displaystyle A}$;

то мы можем сделать вывод, что ${displaystyle A}$ выполняется для пустой последовательности.

Этот принцип индукции стержня используется в работах A. S. Troelstra, С. К. Клини, Драгалин и Джоан Мощовакис. Обычно это происходит из индукции тонких стержней или монотонных стержней. (Даммит 1977)

Связь между этими схемами и другой информацией

Следующие результаты об этих схемах могут быть интуитивно доказано:

${displaystyle {egin{aligned}B_{M}&vdash B_{D}[3pt]B_{D}&vdash B_{T}[3pt]B_{T}&vdash B_{D}end{aligned}}}$

(Символ "${displaystyle ,vdash ,}$" это "турникет ".

Неограниченная индукция стержня

Дополнительная схема индукции стержня была первоначально дана в виде теоремы Брауэр (1975), не содержащие «лишних» ограничений на R под названием Теорема бара. Однако доказательство этой теоремы было ошибочным, и неограниченная индукция стержня не считается интуиционистски обоснованной (см. Dummett 1977, стр. 94–104, где объясняется, почему это так). Схема неограниченного индукционного стержня приведена ниже для полноты картины.

Учитывая два предиката ${displaystyle R}$ и ${displaystyle A}$ на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:

• каждая последовательность выбора содержит хотя бы один начальный сегмент, удовлетворяющий ${displaystyle R}$ в какой-то момент;
• каждая конечная последовательность, удовлетворяющая ${displaystyle R}$ также удовлетворяет ${displaystyle A}$;
• если все расширения конечной последовательности одним элементом удовлетворяют ${displaystyle A}$, то эта конечная последовательность также удовлетворяет ${displaystyle A}$;

то мы можем сделать вывод, что ${displaystyle A}$ выполняется для пустой последовательности.

Отношения к другим полям

В классическом обратная математика, "барная индукция" (${displaystyle BI_{D}}$) обозначает связанный принцип, утверждающий, что если отношение ${displaystyle R}$ это в порядке, то у нас есть схема трансфинитная индукция над ${displaystyle R}$ для произвольных формул.

Рекомендации

• Л. Э. Дж. Брауэр Брауэр, Л. Э. Дж. Собрание сочинений, 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)