Распространение (интуиционизм)

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

История

Понятие распространения было впервые предложено Л. Дж. Брауэром (1918B) и использовалось для определения континуума . По мере развития его идей использование расширений стало обычным явлением в интуиционистской математике , особенно при работе с последовательностями выбора и интуиционистским анализом (см. Даммет 77, Трульстра 77). В последнем случае действительные числа представлены разбросами натуральных или целых чисел.

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

Определения

Обзор

В современной терминологии спред — это обитаемый замкнутый набор последовательностей. Спреды определяются с помощью функции распространения , которая выполняет ( разрешимую ) «проверку» конечных последовательностей. Если все конечные начальные части бесконечной последовательности удовлетворяют «проверке» функции распространения, то мы говорим, что бесконечная последовательность допустима для распространения .Понятие спреда и его функция распространения в литературе взаимозаменяемы. Теоретически граф можно рассматривать как корневое ориентированное дерево числовыми с метками вершин .Веер , также известный как финитный спред, представляет собой особый тип спреда. В терминах графа это конечное ветвление.Наконец, одетый разворот — это разложение некоторой функции, действующей на конечные последовательности.

Предварительные обозначения и терминология

В этой статье используется " $\langle$" и " $\rangle$" для обозначения начала и конца последовательности. Последовательность без элементов, так называемая пустая последовательность, обозначается $\langle \rangle$.

Дана бесконечная последовательность $\langle x_{1},x_{2},\ldots \rangle$, мы говорим, что конечная последовательность $\langle y_{1},y_{2},\ldots ,y_{i}\rangle$ является начальным сегментом $\langle x_{1},x_{2},\ldots \rangle$ тогда и только тогда, когда $x_{1}=y_{1}$ и $x_{2}=y_{2}$ и... и $x_{i}=y_{i}$.

Функция распространения

Функция распространения $s$ — функция на конечных последовательностях, которая удовлетворяет следующим свойствам:

• Учитывая любую конечную последовательность $\langle x_{1},x_{2},\ldots ,x_{i}\rangle$ или $s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0$ или $s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=1$. Другими словами, проверяемое свойство должно быть разрешимо через $s$.
• $s(\langle \rangle )=0$.
• Учитывая любую конечную последовательность $\langle x_{1},x_{2},\ldots ,x_{i}\rangle$ такой, что $s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0$, существуют некоторые $k$ такой, что $s(\langle x_{1},x_{2},\ldots ,x_{i},k\rangle )=0$.

Учитывая конечную последовательность, если $s$ возвращает 0, последовательность допустима для разброса, заданного через $s$, а иначе недопустимо . Пустая последовательность допустима и поэтому является частью каждого разворота. Каждую конечную последовательность в развороте можно расширить до другой конечной последовательности в развороте, добавив дополнительный элемент в конец последовательности. Таким образом, функция распространения действует как характеристическая функция, допускающая множество длинных конечных последовательностей.

Мы также говорим, что бесконечная последовательность $\langle x_{1},x_{2},\ldots \rangle$ допустимо для спреда, определяемого функцией спреда $s$ тогда и только тогда, когда каждый начальный сегмент $\langle x_{1},x_{2},\ldots \rangle$ допустимо $s$. Например, для предиката, характеризующего закономерную бесконечную последовательность чисел, можно проверить, что он допустим по отношению к некоторой функции распространения.

Фанат

Неформально, функция распространения $s$ определяет веер, если для данной конечной последовательности, допустимой для разброса, существует только конечное число возможных значений, которые мы можем добавить в конец этой последовательности так, чтобы наша новая расширенная конечная последовательность была допустимой для разброса. В качестве альтернативы мы можем сказать, что существует верхняя граница значения для каждого элемента любой последовательности, допустимой для разброса. Формально:

• Функция распространения $s$ определяет веер тогда и только тогда, когда задана любая последовательность, допустимая для распространения $\langle x_{1},x_{2},\ldots ,x_{i}\rangle$, то существует некоторый $k$ такой, что при любом $j>k$ затем $s(\langle x_{1},x_{2},\ldots ,x_{i},j\rangle )=1$

Таким образом, учитывая последовательность, допустимую для веера, мы имеем только конечное число возможных расширений, которые также допустимы для веера, и мы знаем максимальный элемент, который мы можем добавить к нашей допустимой последовательности так, чтобы расширение оставалось допустимым.

Примеры

Спреды

Простые примеры спредов включают в себя

• Набор последовательностей четных чисел
• Набор последовательностей целых чисел 1–6
• Набор последовательностей допустимых команд терминала.

Фанаты

• Набор последовательностей допустимых шахматных ходов.
• Набор бесконечных двоичных последовательностей
• Набор последовательностей букв

Ниже приведены два разворота, обычно используемые в литературе.

Всеобщее распространение ( континуум )

Учитывая любую конечную последовательность $\langle x_{1},x_{2},\ldots ,x_{i}\rangle$, у нас есть $s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0$. Другими словами, это разворот, содержащий все возможные последовательности. Этот разворот часто используется для представления совокупности всех последовательностей выбора .

Бинарный спред

Учитывая любую конечную последовательность $\langle x_{1},x_{2},\ldots ,x_{i}\rangle$, если все наши элементы ( $x_{1},x_{2},\ldots ,x_{i}$) равны 0 или 1, тогда $s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0$, в противном случае $s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=1$. Другими словами, это разворот, содержащий все двоичные последовательности .

Одетые развороты

Примером «одетого» разворота является разброс целых чисел такой, что $s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0$ тогда и только тогда, когда

$\forall y.(0<y\leq i)\to {\big (}(x_{i}=0)\lor (x_{i}=2\cdot x_{y-1}\pm 1){\big )}$,

вместе с функцией $f(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=x_{i}\cdot 2^{2-i}$. Это реальные цифры .

См. также

• Бар индукционный
• Последовательность выбора
• Конструктивный анализ

Ссылки

• Л. Дж. Брауэр. Обоснование теории множеств, независимой от логической теоремы об исключенных третьих сторонах. Первая часть, Общая теория множеств , KNAW Verhandelingen, 5: 1–43 (1918A)
• Майкл Даммит Элементы интуиционизма , Oxford University Press (1977)
• Последовательности выбора А.С. Троэльстры : глава интуиционистской математики , Clarendon Press (1977)