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

У этого термина существуют и другие значения, см. Поток.

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

Определение

Поток $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$.»

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

Для улучшения этой статьи по математике желательно?: Викифицировать статью. Проставить интервики в рамках проекта Интервики. Найти и оформить в виде сносок ссылки на авторитетные источники, подтверждающие написанное.