Бар индукционный
Барная индукция – это принцип рассуждения, используемый в интуиционистской математике , введенный Л. Дж. Брауэром . Основное применение индукции бара — это интуиционистский вывод теоремы веера, ключевого результата, используемого при выводе теоремы о равномерной непрерывности.
Это также полезно для предоставления конструктивных альтернатив другим классическим результатам.
Цель принципа — доказать свойства всех бесконечных последовательностей натуральных чисел (называемых последовательностями выбора в интуиционистской терминологии) путем индуктивного сведения их к свойствам конечных списков. Индукция бара также может использоваться для доказательства свойств всех последовательностей выбора в развороте (особый вид набора ).
Определение [ править ]
Учитывая последовательность выбора , любая конечная последовательность элементов этой последовательности называется начальным сегментом этой последовательности выбора.
В настоящее время в литературе существует три формы индукции столбца, каждая из которых накладывает определенные ограничения на пару предикатов, а ключевые различия выделены жирным шрифтом.
Разрешимая индукция бара (BI D ) [ править ]
Учитывая два предиката и на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:
- каждая последовательность выбора содержит по крайней мере один начальный сегмент, удовлетворяющий в какой-то момент (это выражается в том, что это бар );
- разрешима ; (т.е. наша полоса разрешима )
- каждая конечная последовательность, удовлетворяющая также удовлетворяет (так справедливо для каждой последовательности выбора, начиная с вышеупомянутой конечной последовательности);
- если все расширения конечной последовательности одним элементом удовлетворяют , то эта конечная последовательность также удовлетворяет (иногда это называют наследственность по восходящей линии );
тогда мы можем заключить, что выполняется для пустой последовательности (т. е. A выполняется для всех последовательностей выбора, начиная с пустой последовательности).
Этот принцип индукции штанги отдается предпочтение в работах А.С. Троелстра , С.К. Клини и Альберта Драгалина.
Индукция тонкого стержня (BI T ) [ править ]
Учитывая два предиката и на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:
- каждая последовательность выбора содержит уникальный начальный сегмент, удовлетворяющий в какой-то момент (т.е. наша полоса тонкая );
- каждая конечная последовательность, удовлетворяющая также удовлетворяет ;
- если все расширения конечной последовательности одним элементом удовлетворяют , то эта конечная последовательность также удовлетворяет ;
тогда мы можем заключить, что справедливо для пустой последовательности.
Этот принцип индукции бара отдается предпочтение в работах Джоан Мошовакис и (интуиционистски) доказуемо эквивалентен индукции разрешимого бара.
Монотонная барная индукция (BI M ) [ править ]
Учитывая два предиката и на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:
- каждая последовательность выбора содержит по крайней мере один начальный сегмент, удовлетворяющий в какой-то момент;
- как только конечная последовательность удовлетворяет , то каждое возможное расширение этой конечной последовательности также удовлетворяет (т.е. наш бар монотонный );
- каждая конечная последовательность, удовлетворяющая также удовлетворяет ;
- если все расширения конечной последовательности одним элементом удовлетворяют , то эта конечная последовательность также удовлетворяет ;
тогда мы можем заключить, что справедливо для пустой последовательности.
Этот принцип наведения штанги используется в работах А. С. Троелстра , С. К. Клини , Драгалина и Джоан Мошовакис .
Отношения между этими схемами и другой информацией [ править ]
Следующие результаты об этих схемах могут быть доказаны интуиционистски :
(Символ « " - это " турникет ".)
Неограниченное введение бара [ править ]
Дополнительная схема индукции бара была первоначально представлена в виде теоремы Брауэра (1975), не содержащей «дополнительных» ограничений на под названием «Теорема Бара» . Однако доказательство этой теоремы было ошибочным, и индукция неограниченного стержня не считается интуиционистски обоснованной (краткое изложение того, почему это так, см. в Dummett 1977, стр. 94–104). Схема наведения неограниченного бара для полноты приведена ниже.
Учитывая два предиката и на конечных последовательностях натуральных чисел таких, что выполняются все следующие условия:
- каждая последовательность выбора содержит по крайней мере один начальный сегмент, удовлетворяющий в какой-то момент;
- каждая конечная последовательность, удовлетворяющая также удовлетворяет ;
- если все расширения конечной последовательности одним элементом удовлетворяют , то эта конечная последовательность также удовлетворяет ;
тогда мы можем заключить, что справедливо для пустой последовательности.
Связь с другими полями [ править ]
В классической обратной математике «барная индукция» ( ) обозначает связанный принцип, утверждающий, что если отношение является полным порядком , то мы имеем схему трансфинитной индукции по для произвольных формул.
Ссылки [ править ]
- ЛЭЙ Брауэр Брауэр, Собрание сочинений LEJ , Vol. Я, Амстердам: Северная Голландия (1975).
- Драгалин, Альберт Г. (2001) [1994], «Индукция бара» , Энциклопедия математики , EMS Press
- Майкл Даммит , Элементы интуиционизма , Clarendon Press (1977)
- С. К. Клини , Р. Э. Весли, Основы интуиционистской математики: особенно в отношении рекурсивных функций , Северная Голландия (1965).
- Майкл Ратьен, Роль параметров в правиле бара и индукции бара , Журнал символической логики 56 (1991), вып. 2, стр. 715–730.
- А. С. Троелстра , Последовательности выбора , Clarendon Press (1977)
- А.С. Трёльстра и Дирк ван Дален , Конструктивизм в математике, Исследования по логике и основам математики , Elsevier (1988)