Бар индукции

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

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

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

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

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

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

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

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

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

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

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

то мы можем заключить, что справедливо для пустой последовательности.${\displaystyle А}$

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

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

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

то мы можем заключить, что справедливо для пустой последовательности.${\displaystyle А}$

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

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

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

(Символ « » — это « турникет ».)${\displaystyle \,\vdash \,}$

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

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

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

то мы можем заключить, что справедливо для пустой последовательности.${\displaystyle А}$

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

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

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

• в
• т
• е