Теорема Диаконеску

В математической логике теорема Диаконеску или теорема Гудмана-Майхилла утверждает, что полной аксиомы выбора достаточно, чтобы вывести закон исключенного среднего или его ограниченные формы.

Теорема была открыта в 1975 году Раду Дьяконеску. и позже Гудманом и Майхиллом . Уже в 1967 году Эрретт Бишоп предложил эту теорему в качестве упражнения (задача 2 на странице 58 книги « Основы конструктивного анализа»). ).

В теории множеств

Теорема является предрешенным выводом классической логики, где предполагается закон исключенного третьего. Поэтому нижеприведенное доказательство дается с использованием средств конструктивной теории множеств . Из доказательства видно, что теорема опирается на аксиому спаривания, а также на аксиому разделения , которые имеют заметные вариации. Решающую роль в теоретико-множественном доказательстве играет также аксиома экстенсиональности . Тонкости, которые вносят последние две аксиомы, обсуждаются ниже.

Закрепление терминологии для доказательства: Назовем множество конечным, если существует биекция с натуральным числом , т.е. конечный ординал фон Неймана . В частности, напишите $0:=\{\}$, $1:=\{0\}$ и $2:=\{0,1\}$. Например, множество конечно с мощностью один (населенный одноэлементный элемент) тогда и только тогда, когда доказано существует биективная функция вне множества. $1$. Приведенное ниже доказательство является простым, поскольку оно не требует патологических различий относительно пустого множества. Для набора $X$ иметь выбор означает, что если все его члены обитаемы , $X$ является областью определения функции выбора . Наконец, для жилых $X$, обозначим $X\leq ^{*}Y$ предложение о том, что $Y$ сюръектируется на $X$.

Стратегия доказательства состоит в том, чтобы связать данное предложение $P$ в область потенциального выбора $X$. И в конечном итоге приходится использовать лишь довольно сдержанную форму полного выбора. Для конкретности и простоты в этом разделе предполагается конструктивная теория множеств с полным разделением, т. е. мы допускаем понимание любого предложения. $P$. В этом контексте следующая лемма более четко изолирует основную идею:

Закон исключенного третьего эквивалентен выбору во всех обитаемых множествах. $X\leq ^{*}2$.

Если обратное направление этой эквивалентности задано, то аксиома выбора , в частности, предоставляющая функцию выбора на всех множествах этой формы, подразумевает исключенное среднее для всех предложений.

Доказательство леммы

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

Чтобы доказать обратное направление, рассматриваются два подмножества любого дублетона с двумя различимыми членами. Как $0\neq 1$, удобный выбор снова $\{0,1\}$. Итак, используя разделение, пусть

$U=\{x\in \{0,1\}\mid (x=0)\vee P\}$

и

$V=\{x\in \{0,1\}\mid (x=1)\lor P\}.$

Оба $U$ и $V$ населены, о чем свидетельствует $0\in U$ и $1\in V$. Если предложение $P$ можно доказать, то оба этих множества равны $\{0,1\}$. В частности, $P\,\to \,U=V$ по экстенсиональности. В свою очередь, для любой математической функции $g$ который может принять оба этих набора в качестве аргумента, можно найти $P\,\to \,g(U)=g(V)$, противоположностью которого является $g(U)\neq g(V)\,\to \,\neg P$.

Остальная часть доказательства относится к паре $X:=\{U,V\}$, набор обитаемых множеств. (Действительно, $X$ сам по себе обитаем и даже подтверждает $X\leq ^{*}2$, что означает, что он конечно индексирован . Однако обратите внимание, что если не предполагать исключенное среднее, $X$ не обязательно должно быть доказуемо конечным в смысле биекции.)

Функция выбора $f$ на $X$ по определению должен отображаться в общий союз $\{0,1\}$ и выполнить

$f(U)\in U\,\land \,f(V)\in V.$

Используя определение двух подмножеств и установленного кодомена функции, это сводится к

${\big (}f(U)=0\lor P{\big )}\land {\big (}f(V)=1\lor P{\big )}.$

Используя закон дистрибутивности , это, в свою очередь, означает $P\lor {\big (}f(U)\neq f(V){\big )}$. Таким образом, согласно предыдущему комментарию о функциях, существование функции выбора на этом множестве влечет за собой дизъюнкцию $P\lor \neg P$. На этом доказательство леммы завершается.

Обсуждение

Как отмечается, $P$ подразумевает, что оба определенных множества равны $\{0,1\}$. В этом случае пара $\{U,V\}$ равно одноэлементному набору $\{\{0,1\}\}$ и в этой области есть две возможные функции выбора: либо $0$ или $1$. Если вместо этого $P$ может быть отклонено, т.е. если $\neg P$ держится, тогда $U=\{0\}$ и $V=\{1\}$. Так что в таком случае $U\neq V$, и на соответствующей паре $\{\{0\},\{1\}\}$ существует только одна возможная функция выбора, выбирающая уникального жителя каждого одноэлементного множества. Это последнее задание» $U\mapsto 0$ и $V\mapsto 1$"нежизнеспособно, если $P$ выполняется, поскольку тогда два входных параметра фактически одинаковы. Аналогично, первые два назначения нежизнеспособны, если $\neg P$ выполняется, поскольку тогда эти два входа не имеют общего члена. Можно сказать, что если функция выбора вообще существует, то существует и функция выбора, выбирающая $0$ от $U$и одна (возможно, одна и та же функция), выбирающая $1$ от $V$.

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

Некоторые множества можно определить в терминах предложения $P$ и, используя исключенное третье, в классической теории множеств докажите, что эти множества представляют собой функции выбора. $f\colon \{U,V\}\to \{0,1\}$. Такой набор представляет собой присвоение, обусловленное тем, $P$ держит. Если $P$ может быть признано истинным или ложным, тогда такой набор явно упрощается до одного из трех вышеупомянутых кандидатов.

Но в любом случае ни $P$ ни $\neg P$ обязательно может быть установлено. Более того, они могут даже быть независимы от рассматриваемой теории. Поскольку каждый из первых двух явных кандидатов несовместим с третьим, обычно невозможно идентифицировать оба возвращаемых значения функции выбора. $f(U)$ и $f(V)$, среди терминов $0$ и $1$. Таким образом, это не функция в том смысле этого слова, которую можно было бы явно вычислить в ее кодомене различимых значений.

Конечность

В теории, не допускающей дизъюнкции $P\lor \neg P$ или какой-либо принцип, подразумевающий его, невозможно даже доказать, что дизъюнкция приведенных выше утверждений о равенстве множеств должна иметь место. Фактически, конструктивно также два множества $U$ и $V$ даже не доказуемо конечны . (Однако любой конечный ординал вводится в любое дедекиндово-бесконечное множество, и поэтому подмножество конечного ординала действительно подтверждает логически негативное понятие дедекиндовой конечности. Это справедливо как для обоих, так и для $U$ и $V$, в который $\{0,1,2\}$ нельзя вводить. Кстати, это согласуется и с классической ${\mathsf {ZF}}$ что существуют множества, которые не являются ни дедекиндово-бесконечными, ни конечными.)

В свою очередь, спаривание $\{U,V\}$ также неуловим. Это в сюръективном образе области $2$, но что касается присвоений выбора, неизвестно, насколько явные присвоения значений для обоих $U$ и $V$ можно сделать, или даже сколько различных назначений нужно будет указать. Таким образом, обычно не существует определения (множества), такого, чтобы конструктивная теория доказывала бы, что совместное присвоение (множество) является функцией выбора с областью определения. $\{U,V\}$. Обратите внимание, что такая ситуация не возникает с областью выбора функций, предоставляемой более слабыми принципами счетного и зависимого выбора , поскольку в этих случаях областью выбора всегда является просто $\mathbb {N}$, тривиально счетный первый бесконечный кардинал.

Принятие полной аксиомы выбора или классической логики формально подразумевает, что мощность $\{U,V\}$ либо $1$ или $2$, что, в свою очередь, означает, что оно конечно. Но такой постулат, как эта аксиома существования простой функции, все еще не решает вопрос, какую именно мощность имеет эта область, а также не определяет мощность множества возможных выходных значений этой функции.

Роль разделения

Таким образом, функции связаны с равенством (по определению уникальности существования, используемому в функциональности), равенство связано с членством (непосредственно через аксиому экстенсиональности, а также через формализацию выбора в множествах), а членство связано с предикатами (через аксиома разделения). Используя дизъюнктивный силлогизм , утверждение $P$ оказывается эквивалентным экстенсиональному равенству двух множеств. И исключенное среднее для него эквивалентно существованию некоторой функции выбора на $\{U,V\}$. Оба проходят всякий раз, когда $P$ может использоваться в принципе разделения множеств.

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

Другие фреймворки

В конструктивной теории типов или в арифметике Гейтинга, расширенной конечными типами, обычно вообще не существует принципа разделения — подмножества типа обрабатываются по-разному. Там формой аксиомы выбора является теорема, а исключенное третье - нет.

В топои

В оригинальной статье Дьяконеску теорема представлена ​​в терминах топос-моделей конструктивной теории множеств.