Теорема Дьяконеску

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

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

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

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

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

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

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

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

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

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

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

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

и

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

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

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

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

${\displaystyle f(U)\in U\,\land \,f(V)\in V.}$

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

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

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

Обсуждение

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

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

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

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

Конечность

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

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

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

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

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

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

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

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

В топосах

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

Примечания

1. Диаконеску, Раду (1975). «Аксиома выбора и дополнения». Труды Американского математического общества . 51 (1): 176–178. doi : 10.1090/S0002-9939-1975-0373893-X . MR  0373893.
2. Гудман, Северная Дакота; Майхилл, Дж. (1978). «Выбор подразумевает исключенное среднее». Zeitschrift für Mathematische Logik und Grundlagen der Mathematik . 24 (25–30): 461. doi :10.1002/malq.19780242514.
3. Э. Бишоп, Основы конструктивного анализа , McGraw-Hill (1967)