Ограниченный принцип всеведения - Limited principle of omniscience

В конструктивная математика, то ограниченный принцип всеведения (LPO) и менее ограниченный принцип всеведения (LLPO) являются аксиомами, которые неконструктивны, но слабее, чем полная закон исключенного среднего (Мосты и Ричман 1987 ). Аксиомы LPO и LLPO используются для измерения степени неконструктивности, необходимой для аргумента, как в конструктивная обратная математика. Они также связаны с слабые контрпримеры в смысле Брауэра.

Определения

Ограниченный принцип всеведения гласит (Мосты и Ричман 1987, п. 3):

LPO: Для любой последовательности а0, а1, ... такие, что каждый ая равно 0 или 1, выполняется следующее: либо ая = 0 для всех я, или есть k с аk = 1.[1]

Менее ограниченный принцип всеведения гласит:

LLPO: Для любой последовательности а0, а1, ... такие, что каждый ая либо 0, либо 1, и такое, что не более одного ая отлична от нуля, выполняется следующее: либо а2я = 0 для всех я, или же а2я+1 = 0 для всех я, куда а2я и а2я+1 - записи с четным и нечетным индексами соответственно.

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

Термин «всеведение» происходит от мысленного эксперимента относительно того, как математик может сказать, какой из двух случаев в заключении LPO имеет место для данной последовательности (ая). Отвечая на вопрос "есть ли k с аk = 1? "Отрицательно, предполагая, что ответ отрицательный, кажется, требует изучения всей последовательности. Поскольку это потребовало бы изучения бесконечного числа терминов, аксиома, утверждающая, что это определение возможно, была названа" принципом всеведения " Епископ (1967).

Рекомендации

  1. ^ Шахты, Рэй (1988). Курс конструктивной алгебры. Ричман, Фред и Руйтенбург, Вим. Нью-Йорк: Springer-Verlag. С. 4–5. ISBN  0387966404. OCLC  16832703.
  • Епископ, Эрретт (1967). Основы конструктивного анализа. ISBN  4-87187-714-0.CS1 maint: ref = harv (связь)
  • Бриджес, Дуглас; Ричман, Фред (1987). Разновидности конструктивной математики. ISBN  0-521-31802-5.CS1 maint: ref = harv (связь)

внешняя ссылка