Ограниченный принцип всеведения

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

Определения

Ограниченный принцип всеведения гласит ( Bridges & Richman 1987 , стр. 3):

LPO : Для любой последовательности $a_{0}$, $a_{1}$, ... такой, что каждый $a_{i}$ либо $0$ или $1$, имеет место следующее: либо $a_{i}=0$ для всех $i$, или есть $k$ с $a_{k}=1$.

Второй дизъюнкт можно выразить как $\exists k.a_{k}\neq 0$ и конструктивно сильнее отрицания первого, $\neg \forall k.a_{k}=0$. Слабая схема , в которой первое заменяется вторым, называется WLPO и представляет собой частные случаи исключенного среднего.

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

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

Здесь $a_{2i}$ и $a_{2i+1}$ — это записи с четным и нечетным индексом соответственно.

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

Терминология

Термин «всезнание» возник в результате мысленного эксперимента, посвященного тому, как математик мог определить, какой из двух случаев в заключении LPO справедлив для данной последовательности. $(a_{i})$. Отвечая на вопрос «есть ли $k$ с $a_{k}=1$«Отрицательно», предполагая, что ответ отрицательный, по-видимому, требует рассмотрения всей последовательности. Поскольку это потребовало бы изучения бесконечного числа терминов, аксиома, утверждающая, что такое определение возможно, была названа Бишопом (1967 ) «принципом всезнания». ) .

Варианты

Логические версии

Эти два принципа можно выразить как чисто логические принципы, выражая их в терминах разрешимых предикатов естественных явлений. Т.е. $P$ для чего $\forall n.P(n)\lor \neg P(n)$ держится.

Меньший принцип соответствует предикатной версии закона Де Моргана , которая не выполняется интуиционистски , т.е. дистрибутивности отрицания конъюнкции.

Аналитические версии

Оба принципа имеют аналогичные свойства в теории действительных чисел . Аналитический LPO утверждает, что каждое действительное число удовлетворяет трихотомии. $x<0$ или $x=0$ или $x>0$ . Аналитический LLPO утверждает, что каждое действительное число удовлетворяет дихотомии. $x\geq 0$ или $x\leq 0$, а аналитический принцип Маркова гласит, что если $x\leq 0$ ложно, то $x>0$.

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

См. также

• Конструктивный анализ

Ссылки

• Бишоп, Эрретт (1967). Основы конструктивного анализа . ISBN  4-87187-714-0 .
• Бриджес, Дуглас; Ричман, Фред (1987). Разновидности конструктивной математики . ISBN  0-521-31802-5 .

Внешние ссылки

• «Конструктивная математика» Статья Дугласа Бриджеса в Стэнфордской энциклопедии философии.