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

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

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

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

Определение [ править ]

Для данной последовательности выбора любая конечная последовательность элементов этой последовательности называется начальным сегментом этой последовательности выбора.${\ 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}$

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

Этот принцип индукции стержня одобрен в работах AS Troelstra , SC Kleene и Dragalin.

Индукция тонкого стержня (BI _T ) [ править ]

Даны два предиката и конечные последовательности натуральных чисел такие, что выполняются все следующие условия:${\ 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}$

Этот принцип индукции стержня используется в работах AS Troelstra , SC Kleene , Dragalin и Joan Moschovakis . Обычно это происходит от индукции тонких стержней или монотонных стержней. (Даммит 1977)

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

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

${\ displaystyle {\ begin {align} B_ {M} & \ vdash B_ {D} \\ [3pt] B_ {D} & \ vdash B_ {T} \\ [3pt] B_ {T} & \ vdash B_ { D} \ end {выровнено}}}$

(Символ « » означает « турникет ».)${\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}$

Ссылки [ править ]

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