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

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

Определение

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

1. Пустой кортеж $\langle \rangle$ является допустимым.
2. Для любого допустимого кортежа $\langle a_{1},\ldots ,a_{n}\rangle$ найдётся по меньшей мере одно натуральное число $k$, для которого кортеж $\langle a_{1},\ldots ,a_{n},k\rangle$ также будет допустимым.
3. Для любого допустимого кортежа вида $\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. допустимыми по закону потока считаются кортежи, все элементы которых равны $1$ или $2$;
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$.

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