Бар индукционный

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

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

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

Определение

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

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

Разрешимая индукция бара (BI _D )

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

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

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

Этот принцип индукции штанги отдается предпочтение в работах А.С. Троелстра , С.К. Клини и Альберта Драгалина.

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

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

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

тогда мы можем заключить, что $A$ справедливо для пустой последовательности.

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

Монотонная барная индукция (BI _M )

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

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

тогда мы можем заключить, что $A$ справедливо для пустой последовательности.

Этот принцип наведения штанги используется в работах А. С. Троелстра , С. К. Клини , Драгалина и Джоан Мошовакис .

Отношения между этими схемами и другой информацией

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

${\begin{aligned}BI_{M}&\vdash BI_{D}\\[3pt]BI_{D}&\vdash BI_{T}\\[3pt]BI_{T}&\vdash BI_{D}\end{aligned}}$

(Символ " $\,\vdash \,$" - это " турникет ".)

Неограниченное введение бара

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

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

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

тогда мы можем заключить, что $A$ справедливо для пустой последовательности.

Связь с другими полями

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

Ссылки

• ЛЭЙ Брауэр Брауэр, Собрание сочинений LEJ , Vol. Я, Амстердам: Северная Голландия (1975).
• Драгалин, Альберт Г. (2001) [1994], «Индукция бара» , Энциклопедия математики , EMS Press
• Майкл Даммит , Элементы интуиционизма , Clarendon Press (1977)
• С. К. Клини , Р. Э. Весли, Основы интуиционистской математики: особенно в отношении рекурсивных функций , Северная Голландия (1965).
• Майкл Ратьен, Роль параметров в правиле бара и индукции бара , Журнал символической логики 56 (1991), вып. 2, стр. 715–730.
• А. С. Троелстра , Последовательности выбора , Clarendon Press (1977)
• А.С. Троэльстра и Дирк ван Дален , Конструктивизм в математике, Исследования по логике и основам математики , Elsevier (1988)