Можно ли официально ввести нотацию конструктора наборов в ZFC?

Если совсем формально, то ZFC можно сформулировать как набор формул первого порядка над сигнатурой л "=" { е } состоящий только из одного бинарного отношения е . Тогда на этом формальном языке можно сформулировать обычные аксиомы ZFC.

Недавно я узнал о концепции расширения по определению . Основная идея такова: на практике мы не работаем на языке, состоящем только из е , но мы постоянно вводим новые символы! Например, сначала мы замечаем, что существует уникальное множество, вообще не имеющее элементов, и это оправдывает возможность присвоения этому уникальному множеству специального символа — мы выбираем ∅ для этого. Аналогично можно ввести символ Н для натуральных чисел. Но та же концепция работает, когда мы вводим новые символы функций и отношений: например, мы можем определить операцию ∪ путем доказательства того, что для каждого A, B существует уникальный набор А ∪ Б с собственностью ∀ Икс ( Икс е А ∪ Б ⟺ Икс е А ∨ Икс е Б ) (после доказательства того, что это уникально для двух множеств A, B ); также можно определить отношение ⊆ установив А ⊆ Б :⇔ ∀ Икс ( Икс е А ⟹ Икс е Б ) .

Формальное определение этой концепции «расширения по определению» см. в связанной статье в Википедии. Я думаю:

Можно ли аналогичным образом ввести нотацию построения множеств в формальный язык теории множеств? Я имею в виду что-то вроде этого: заданный символ набора А и формула ф ( Икс ) с одной свободной переменной можно определить множество { Икс е А : ф ( Икс ) } быть уникальным набором всех элементов A, которые удовлетворяют свойству ф . Это просто человеческое обозначение или его можно сделать точным, как понятие расширения по определению?

Видимо недостаточно хорошо. Извини.
@Arthur: я спрашиваю, можно ли добавить такое выражение, как { Икс е А ∣ ф ( Икс ) } к формальному синтаксису ZFC, например, можно добавить ⊆ и ∪ и ∅ к формальному синтаксису. Мой вопрос немного глупый и наивный, но в лучшем случае есть чему поучиться :-)
Я так и не уловил большую часть интуиции в строжайшей математической логике, но мне кажется, ф является препятствием. Поэтому понимание и замена - это не аксиомы, а схемы аксиом. Я думаю, вы могли бы сделать схему для нотации конструктора наборов. Или я могу быть не в себе.
Для всех, кто наткнется на этот пост, формальный способ сделать это — через определение расширения . Это строгий способ поддержки так называемой нотации построителя множеств (которая, по сути, является постоянным символом, свидетельствующим об экзистенциальных утверждениях), а также ∪ (бинарная функция-символ) и ⊆ (бинарный предикат-символ). Обратите внимание, что последние два не представлены никакими объектами (наборами) в ZFC.
@user21820 user21820: Я дал ответ ниже на ваш вопрос в соответствии с определением расширения, но до прочтения вашего комментария. Ты прав. Обозначение построителя множеств, применяемое к данной формуле с одной свободной переменной, можно интерпретировать как новый символ унарной функции, который необходимо добавить в язык теории множеств.
@Transcendental: Да, и у вас есть альтернативный способ думать об этом, а именно, что аксиома спецификации дает определимую функцию на множествах для каждой формулы, которая вырезает подмножество, указанное формулой. У меня было просто более общее представление о том, что любую экзистенциальную аксиому можно механически преобразовать в определяемую константу. "="

Ответы (3)

Вот подход, который не использует оператор описания Рассела я .

Дана формула первого порядка ф с одной свободной переменной г на языке теории множеств ( л О С Т ), вы можете добавить (i) новый унарный функциональный символ Ф ф к л О С Т и (ii) следующую новую аксиому Z Ф :

( ∀ Икс ) ( ∀ у ) ( у "=" Ф ф ( Икс ) ⟺ ( ∀ г ) ( г е у ⟺ ( г е Икс ∧ ф ) ) ) . ( ⋆ )
С помощью хорошо известного метода расширения по определениям в логике первого порядка эти дополнения дают консервативное расширение Z Ф потому что, с одной стороны, схема спецификации аксиом гарантирует, что
( ∀ Икс ) ( ∃ у ) ( ∀ г ) ( г е у ⟺ ( г е Икс ∧ ф ) ) ,
а с другой стороны, аксиома экстенсиональности гарантирует, что
( ∀ Икс ) ( ∃ ! у ) ( ∀ г ) ( г е у ⟺ ( г е Икс ∧ ф ) ) .
Поэтому вы можете думать о Ф ф как формализованная версия нотации построителя множеств, применяемая к ф .

Нотация построителя множества является оператором «формирования терминов», т. е. символом, который при «входе» формулы дает в качестве «выхода» терм , как у Рассела. я для определенных описаний .

Для того, чтобы «расширить» язык с помощью я , мы должны :

1) доказать: ( ∃ ! г ) Вопрос ( г , Икс 1 , … , Икс н )

2) добавить аксиому: у "=" ( я г ) Вопрос ( г , Икс 1 , … , Икс н ) ↔ Вопрос ( у , Икс 1 , … , Икс н ) .

Точно так же в теории множеств мы должны доказать:

( ∃ ! г ) ( ∀ Икс ) ( Икс е г ↔ ф ( Икс ) )

а затем добавить аксиому:

{ Икс : ф ( Икс ) } "=" ( я г ) ( ∀ Икс ) ( Икс е г ↔ ф ( Икс ) ) .

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

Да названия в развитии форсинга можно посмотреть так и определение конструируемой вселенной л можно и так сформулировать.

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

Можно ли официально ввести нотацию конструктора наборов в ZFC?
СпросиСетьПолитика конфиденциальности1y, 0v