Жилой комплекс

В математике множество $A$ населен , если существует элемент $a\in A$ .

В классической математике свойство быть обитаемым эквивалентно непустоте . Однако эта эквивалентность недействительна в конструктивной или интуиционистской логике , поэтому эта отдельная терминология в основном используется в теории множеств конструктивной математики .

Определение [ править ]

На формальном языке логики первого порядка положим $A$ имеет свойство быть обитаемым , если

\exists z.(z\in A).

Связанные определения [ править ]

Множество $A$ имеет свойство быть пустым , если $\forall z.(z\notin A)$ или эквивалентно $\neg \exists z.(z\in A)$ . Здесь $z\notin A$ означает отрицание $\neg (z\in A)$ .

Множество $A$ непусто , если оно не пусто, т. е. если $\neg \forall z.(z\notin A)$ или эквивалентно $\neg \neg \exists z.(z\in A)$ .

Теоремы [ править ]

метод настройки Завершите $P\to ((P\to Q)\to Q)$ и принимая любое ложное суждение за $Q$ устанавливает, что $P\to \neg \neg P$ всегда действителен. Следовательно, любое обитаемое множество также доказуемо непусто.

Обсуждение [ править ]

В конструктивной математике принцип исключения двойного отрицания не действует автоматически. В частности, утверждение о существовании обычно сильнее, чем его двуотрицаемая форма. Последнее просто выражает, что существование нельзя исключить, в том смысле, что его нельзя последовательно отрицать. В конструктивном прочтении, чтобы $\exists z.\phi (z)$ придерживаться некоторой формулы $\phi$ , это необходимо для конкретного значения $z$ удовлетворяющий $\phi$ быть построенным или известным. Точно так же отрицание универсального кванторного высказывания в целом слабее, чем экзистенциальная квантификация отрицаемого высказывания. В свою очередь, можно доказать, что множество непусто, но невозможно доказать, что оно обитаемо.

Примеры [ править ]

Такие наборы как $\{2,3,4,7\}$ или $\mathbb {Q}$ населены, о чем свидетельствует, например, $3\in \{2,3,4,7\}$ . Набор $\{\}$ пусто и, следовательно, не заселено. Естественно, раздел примеров, таким образом, фокусируется на непустых множествах, которые не являются доказуемо заселенными.

Легко привести примеры любого простого теоретико-множественного свойства, поскольку логические утверждения всегда можно выразить как теоретико-множественные, используя аксиому разделения . Например, с подмножеством $S\subset \{0\}$ определяется как $S:=\{n\in \{0\}\mid P\}$ , предложение $P$ всегда может быть эквивалентно сформулировано как $0\in S$ . Двойное отрицание существования сущности с определенным свойством может быть выражено утверждением, что множество сущностей с этим свойством непусто.

Пример, относящийся к исключенному среднему [ править ]

Определить подмножество $A\subset \{0,1\}$ с помощью

A:=\{n\in \{0,1\}\mid (P\land n=0)\lor (\neg P\land n=1)\}

Четко $P\leftrightarrow 0\in A$ и $(\neg P)\leftrightarrow 1\in A$ , и из принципа непротиворечия заключаем $\neg (0\in A\land 1\in A)$ . Дальше, $(P\lor \neg P)\leftrightarrow (0\in A\lor 1\in A)$ и, в свою очередь

(P\lor \neg P)\to \exists !(n\in \{0,1\}).n\in A

Уже минимальная логика доказывает $\neg \neg (P\lor \neg P)$ , двойное отрицание для любого исключенного среднего оператора, что здесь эквивалентно $\neg (0\notin A\land 1\notin A)$ . Таким образом, выполнив два противопоставления предыдущей импликации, можно установить $\neg \neg \exists !(n\in \{0,1\}).n\in A$ . На словах: нельзя последовательно исключать, что именно одно из чисел $0$ и $1$ обитает $A$ . В частности, последнее можно ослабить до $\neg \neg \exists n.n\in A$ , говоря $A$ оказывается непустым.

В качестве примера утверждений для $P$ Возьмем, к примеру, печально известное, доказавшее свою независимость от теории утверждение, такое как гипотеза континуума , непротиворечивость существующей обоснованной теории или, неформально, непознаваемое утверждение о прошлом или будущем. По замыслу они выбраны как недоказуемые. Вариантом этого является рассмотрение математических утверждений, которые просто еще не установлены — см. также контрпримеры Брауэра . Знание обоснованности того или иного $0\in A$ или $1\in A$ эквивалентно знанию о $P$ как указано выше, и не могут быть получены. Учитывая ни $P$ ни $\neg P$ можно доказать в теории, это тоже не докажет $A$ быть населенным каким-то определенным числом. Кроме того, конструктивная основа со свойством дизъюнкции не может доказать $P\lor \neg P$ или. Нет никаких доказательств $0\in A$ , ни для $1\in A$ , и конструктивная недоказуемость их дизъюнкции отражает это. Тем не менее, поскольку доказано, что исключение исключенного третьего всегда противоречиво, также установлено, что $A$ не пуст. Классическая логика принимает $P\lor \neg P$ аксиоматически, портя конструктивное чтение.

Пример, относящийся к выбору [ править ]

Существуют различные легко охарактеризуемые множества, существование которых недоказуемо в ${\mathsf {ZF}}$ , но существование которых подразумевается полной аксиомой выбора ${\mathrm {AC} }$ . Таким образом, эта аксиома сама по себе не зависит от ${\mathsf {ZF}}$ . Фактически это противоречит другим потенциальным аксиомам теории множеств. Более того, это действительно противоречит конструктивным принципам в контексте теории множеств. Теория, не допускающая исключенного третьего, также не подтверждает принцип существования функции. ${\mathrm {AC} }$ .

В ${\mathsf {ZF}}$ , ${\mathrm {AC} }$ эквивалентно утверждению, что для каждого векторного пространства существует базис. Итак, более конкретно, рассмотрим вопрос о существовании гамелевских базисов действительных чисел над рациональными числами . Этот объект неуловим в том смысле, что они различны ${\mathsf {ZF}}$ модели , которые либо отрицают, либо подтверждают его существование. Таким образом, вполне логично просто постулировать, что существование здесь нельзя исключить, в том смысле, что его нельзя последовательно отрицать. Опять же, этот постулат можно выразить так: множество таких гамелевских базисов непусто. В отношении конструктивной теории такой постулат слабее, чем постулат простого существования, но (по замыслу) все еще достаточно силен, чтобы затем отрицать все утверждения, которые подразумевали бы отсутствие базиса Гамеля.

Теория моделей [ править ]

Поскольку обитаемые множества — это то же самое, что и непустые множества в классической логике, невозможно создать модель в классическом смысле, содержащую непустое множество. $X$ но не удовлетворяет» $X$ обитаем».

Однако можно построить модель Крипке. $M$ что отличает эти два понятия. Поскольку импликация истинна в каждой модели Крипке тогда и только тогда, когда она доказуема в интуиционистской логике, это действительно устанавливает, что нельзя интуиционистски доказать, что « $X$ непусто" подразумевает " $X$ обитаем».

См. также [ править ]

Пересечение (теория множеств) - набор элементов, общих для всех некоторых множеств.
Ничего – Полное отсутствие чего-либо; противоположность всему
Типовая среда обитания в теории типов .

Ссылки [ править ]

Д. Бриджес и Ф. Ричман. 1987. Разновидности конструктивной математики . Издательство Оксфордского университета. ISBN 978-0-521-31802-0

В эту статью включены материалы из набора Inhabited на сайте PlanetMath , который доступен под лицензией Creative Commons Attribution/Share-Alike License .