Поток (интуиционизм)

Пото́к — одно из основных понятий интуиционистской математики.

Определение

Поток $M$ определяется как совокупность двух законов $\Lambda _{M}$ и $\Gamma _{M}$ , называемых законом потока и дополнительным законом соответственно. Закон потока $\Lambda _{M}$ делит кортежи натуральных чисел на допустимые и недопустимые и должен обладать следующими свойствами:

Пустой кортеж $\langle \rangle$ является допустимым.
Для любого допустимого кортежа $\langle a_{1},\ldots ,a_{n}\rangle$ найдётся по меньшей мере одно натуральное число $k$ , для которого кортеж $\langle a_{1},\ldots ,a_{n},k\rangle$ также будет допустимым.
Для любого допустимого кортежа вида $\langle a_{1},\ldots ,a_{n},k\rangle$ кортеж $\langle a_{1},\ldots ,a_{n}\rangle$ также является допустимым.

Дополнительный закон $\Gamma _{M}$ сопоставляет допустимым кортежам произвольные математические объекты.

Свободно становящиеся последовательности натуральных чисел $\{a_{k}\}_{k=1}^{\infty }$ , для которых при любом $n$ кортеж $\langle a_{1},\ldots ,a_{n}\rangle$ является допустимым по закону потока $M$ , называются допустимыми свободно становящимися последовательностями. Отвечающие им последовательности $\{\Gamma _{M}(a_{k})\}_{k=1}^{\infty }$ (где $\Gamma _{M}$ — дополнительный закон потока $M$ ) называются элементами потока $M$ .

Образно поток может быть представлен как дерево, из каждой вершины которого выходит по меньшей мере одна ветвь, и на каждую вершину которого «навешен» тот или иной математический объект. Допустимые свободно становящиеся последовательности натуральных чисел можно представлять в виде бесконечных путей в таком дереве.

Применение в интуиционистской математике

На понятии потока основаны многие конструкции интуиционистского анализа. Так, континуум $[0,1]$ нередко рассматривается в интуиционистской математике как следующий поток рациональных отрезков:

допустимыми по закону потока считаются кортежи, все элементы которых равны $1$ или $2$ ;
если допустимому кортежу $\langle a_{1},\ldots ,a_{n}\rangle$ дополнительным законом сопоставлен отрезок $[a,b]$ , то кортежу $\langle a_{1},\ldots ,a_{n},1\rangle$ сопоставляется отрезок $[a,(a+b)/2]$ , а кортежу $\langle a_{1},\ldots ,a_{n},2\rangle$ — отрезок $[(a+b)/2,b]$ .

Элементы этого потока считаются вещественными числами, лежащими на отрезке $[0,1]$ .

Запирающие условия и бар-индукция

Пусть ${\mathcal {K}}$ — некоторое условие, накладываемое на допустимые кортежи. Такое условие называется запирающим поток, если для любой допустимой по закону потока свободно становящейся последовательности $\{a_{n}\}_{n=1}^{\infty }$ найдётся номер $n$ , для которого кортеж $\langle a_{1},\ldots ,a_{n}\rangle$ удовлетворяет условию ${\mathcal {K}}$ . В интуиционистской математике считается приемлемым следующий способ умозаключения:

Пусть условие ${\mathcal {K}}$ запирает поток $M$ , и пусть условие ${\mathcal {T}}$ , накладываемое на допустимые кортежи потока $M$ , обладает следующими свойствами:

Любой допустимый кортеж, удовлетворяющий условию ${\mathcal {K}}$ , удовлетворяет условию ${\mathcal {T}}$ .
Если все допустимые кортежи вида $\langle a_{1},\ldots ,a_{n},k\rangle$ удовлетворяют условию ${\mathcal {T}}$ , то допустимый кортеж $\langle a_{1},\ldots ,a_{n}\rangle$ также удовлетворяет условию ${\mathcal {T}}$ .

В таком случае пустой кортеж удовлетворяет условию ${\mathcal {T}}$ .

Такой способ умозаключения называется бар-индукцией.

Одним из характерных примеров применения бар-индукции является принадлежащая Л. Э. Я. Брауэру теорема о веере:

Если поток $M$ финитарен (то есть из каждой его вершины выходит лишь конечное число ветвей) и условие ${\mathcal {K}}$ запирает поток $M$ , то найдётся такое натуральное число $N$ , что для любой допустимой свободно становящейся последовательности $\{a_{k}\}_{k=1}^{\infty }$ найдётся удовлетворяющий условию ${\mathcal {K}}$ кортеж $\langle a_{1},\ldots ,a_{n}\rangle$ со свойством $n<N$ .

В теоретико-множественной математике аналогичное утверждение известно под именем «лемма Кёнига о бесконечном пути».

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.