Введение
Свойство множеств, используемое в конструктивной математике В математике множество обитается, если существует элемент В классической математике свойство обитаемости эквивалентно непустому. Однако это эквивалентность не является действительной в конструктивной или интуиционистской логике, и поэтому эта отдельная терминология в основном используется в теории множеств конструктивной математики.
In mathematics, a set is inhabited if there exists an element
In classical mathematics, the property of being inhabited is equivalent to being non empty. However, this equivalence is not valid in constructive or intuitionistic logic, and so this separate terminology is mostly used in the set theory of constructive mathematics.
Сопутствующие определения
Множество имеет свойство быть пустым, если , или эквивалентно Здесь стоит за отрицание множество не пустое, если оно не пустое, то есть, если , или эквивалентно.
A set is non empty if it is not empty, that is, if , or equivalently .
Теоремы
Modus ponens подразумевает, и принимая любое ложное предложение для устанавливает, что всегда действительна. Следовательно, любая обитаемая совокупность также не пуста.
Обсуждение
В конструктивной математике принцип устранения двойного отрицания не является автоматически действительным. В частности, утверждение о существовании, как правило, сильнее, чем его двойная отрицательная форма. Последнее просто выражает, что существование не может быть исключено, в том сильном смысле, что оно не может быть последовательно отрицано. В конструктивном чтении, для того чтобы придерживаться некоторой формулы , необходимо, чтобы было построено или известно определенное значение удовлетворяющего. Аналогичным образом, отрицание универсального количественного утверждения, как правило, слабее, чем экзистенциальное количественное отрицание отрицательного утверждения. В свою очередь, множество может быть доказано непустым, без того, чтобы кто-то мог доказать, что оно населено.
Примеры
Набор, такой как или населен, как, например, свидетельствуют Набор пуст и, следовательно, не населен. Естественно, в примерах мы сосредоточимся на непустых множествах, которые не являются обитаемыми. Легко привести примеры любого простого теоретического свойства множества, потому что логические утверждения всегда могут быть выражены как теоретические, используя аксиому разделения. Например, с подмножеством, определенным как , предложение всегда может быть эквивалентно заявлено как: "Требование о двойном отрицании существования сущности с определенным свойством может быть выражено путем заявления, что множество сущностей с этим свойством не пусто".
Пример, связанный с выбором
Существуют различные легко характеризуемые множества, существование которых не доказано в теории множеств, но которые подразумеваются как существующие по полной аксиоме выбора. Как таковая, эта аксиома сама по себе независима от теории множеств. Фактически она противоречит другим потенциальным аксиомам теории множеств. Кроме того, это действительно противоречит конструктивным принципам в контексте теории множеств. Теория, которая не допускает исключенного середины, также не подтверждает принцип существования функции In , эквивалентная утверждению о том, что для каждого векторного пространства существует основа. Так что более конкретно, рассмотрим вопрос о существовании оснований Гамеля реальных чисел над рациональными числами. Этот объект неуловим в том смысле, что существуют различные модели, которые либо отрицают, либо подтверждают его существование. Так что также логично предположить, что существование не может быть исключено здесь, в том смысле, что оно не может быть последовательно отрицано. Опять же, этот постулат может быть выражен как утверждение, что множество таких оснований Гамеля не пусто. В конструктивной теории такой постулат слабее постулата простого существования, но (по замыслу) все еще достаточно силен, чтобы затем опровергнуть все положения, которые подразумевали бы отсутствие основы Гамеля.
In , the is equivalent to the statement that for every vector space there exists basis. So more concretely, consider the question of existence of a Hamel bases of the real numbers over the rational numbers. This object is elusive in the sense that are different models that either negate and validate its existence. So it is also consistent to just postulate that existence cannot be ruled out here, in the sense that it cannot consistently be negated. Again, that postulate may be expressed as saying that the set of such Hamel bases is non empty. Over a constructive theory, such a postulate is weaker than the plain existence postulate, but (by design) is still strong enough to then negate all propositions that would imply the non existence of a Hamel basis.
Теория моделей
Поскольку обитаемые множества то же самое, что и непустые множества в классической логике, невозможно создать модель в классическом смысле, которая содержит непустое множество, но не удовлетворяет "обитается". Однако можно построить модель Крипке, которая дифференцирует эти два понятия. Поскольку следствие истинно в каждой модели Крипке, если и только если оно доказуемо в интуиционистской логике, это действительно устанавливает, что нельзя интуитивно доказать, что "непусто" подразумевает "населен".