Последовательность выбора - Choice sequence

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

Законные и беззаконные последовательности

Различают беззаконный и законопослушный последовательности. А законопослушный Последовательность может быть описана полностью - это законченная конструкция, которую можно полностью описать. Например, натуральные числа ${displaystyle mathbb {N}}$ можно рассматривать как закономерную последовательность: последовательность может быть полностью конструктивно описана единственным элементом 0 и функция преемника. Учитывая эту формулировку, мы знаем, что ${displaystyle i}$ -м элементом в последовательности натуральных чисел будет число ${displaystyle i-1}$ . Аналогично функция ${displaystyle f: mathbb {N} mapsto mathbb {N}}$ преобразование натуральных чисел в натуральные числа эффективно определяет значение любого принимаемого аргумента и, таким образом, описывает закономерную последовательность.

А беззаконный (также, свободный) последовательность, с другой стороны, не предопределена. Это следует рассматривать как процедуру генерации значений для аргументов 0, 1, 2, .... То есть незаконную последовательность ${displaystyle alpha}$ это процедура для генерации ${displaystyle alpha _ {0}}$ , ${displaystyle alpha _ {1}}$ , ... (элементы последовательности ${displaystyle alpha}$ ) такой, что:

В любой момент построения последовательности ${displaystyle alpha}$ , известен только начальный сегмент последовательности, и никаких ограничений на будущие значения ${displaystyle alpha}$ ; и
Можно заранее указать начальный отрезок ${displaystyle langle alpha _ {0}, alpha _ {1}, ldots, alpha _ {k} angle}$ из ${displaystyle alpha}$ .

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

Каноническим примером беззаконной последовательности является серия бросков умри. Мы указываем, какой кристалл использовать и, при желании, заранее указываем значения первого ${displaystyle k}$ роллы (для ${displaystyle kin mathbb {N}}$ ). Далее мы ограничиваем значения последовательности нахождением в множестве ${displaystyle {1,2,3,4,5,6}}$ . Эта спецификация содержит процедуру создания рассматриваемой незаконной последовательности. Следовательно, какое-либо конкретное будущее значение последовательности неизвестно.

Аксиоматизация

Есть два аксиомы в частности, что мы ожидаем соблюдения последовательности выбора, как описано выше. Позволять ${displaystyle alpha in n}$ обозначим отношение "последовательность ${displaystyle alpha}$ начинается с начальной последовательности ${displaystyle n}$ "для выбора последовательности ${displaystyle alpha}$ и конечный отрезок ${displaystyle n}$ (более конкретно, ${displaystyle n}$ вероятно будет целым числом кодирование конечная начальная последовательность).

Мы ожидаем следующего, называемого аксиома открытых данных, чтобы удерживать все беззаконные последовательности:

{displaystyle A (alpha) ightarrow существует n [alpha in n, land, forall eta in n [A (eta)]]}

где ${displaystyle A}$ это одноместный предикат. Интуитивное обоснование этой аксиомы состоит в следующем: в интуиционистской математике проверка того, что ${displaystyle A}$ имеет место последовательность ${displaystyle alpha}$ дается как процедура; в любой момент выполнения этой процедуры мы будем исследовать только конечный начальный отрезок последовательности. Таким образом, интуитивно эта аксиома утверждает, что, поскольку в любой момент проверки этого ${displaystyle A}$ удерживает ${displaystyle alpha}$ , мы только проверим, что ${displaystyle A}$ выполняется для конечной начальной последовательности ${displaystyle alpha}$ ; таким образом, должно быть так, что ${displaystyle A}$ также верно для любой беззаконной последовательности ${displaystyle eta}$ разделяя эту начальную последовательность. Это потому, что на любом этапе процедуры проверки ${displaystyle A (альфа)}$ , для любого такого ${displaystyle eta}$ разделяя начальный префикс ${displaystyle alpha}$ закодировано ${displaystyle n}$ что мы уже рассмотрели, если запустить аналогичную процедуру на ${displaystyle eta}$ , мы получим тот же результат. Аксиома может быть обобщена для любого предиката с произвольным числом аргументов.

Другая аксиома требуется для беззаконных последовательностей. В аксиома плотности, предоставленный:

{displaystyle forall n, существует альфа [альфа в n]}

утверждает, что для любого конечного префикса (закодированного) ${displaystyle n}$ , есть последовательность ${displaystyle alpha}$ начиная с этого префикса. Эта аксиома нужна нам, чтобы не было «дыр» в множестве последовательностей выбора. Эта аксиома является причиной того, что мы требуем, чтобы произвольно длинные конечные исходные последовательности беззаконных последовательностей выбора могли быть определены заранее; без этого требования аксиома плотности не обязательно гарантируется.

использованная литература

Даммит, М. 1977. Элементы интуиционизма, Oxford University Press.
Жакетт, Дейл. 2002 г. Компаньон философской логики, Blackwell Publishing. С. 517.
Kreisel, Георг. 1958 г. Замечание о последовательностях свободного выбора и доказательствах топологической полноты, Журнал символической логики, том 23. стр. 269
Троэльстра, А. 1977. Последовательности выбора. Глава интуиционистской математики. Кларендон Пресс.
Троэльстра, А. 1983 г. Анализ последовательности выбора, Journal of Philosophical Logic, 12: 2 с. 197.
Troelstra, A.S .; Д. ван Дален. 1988. Конструктивизм в математике: Введение. Северная Голландия.