Поиски суслика в пустом множестве

[epros]

_Ivana в сообщении #1111541 писал(а):

определяю на нем бинарное отношение равенства всегда ложным для любых его элементов (вроде как имею право)

Только если приобретёте индульгенцию право игнорировать аксиомы эквивалентности.

_Ivana в сообщении #1111541 писал(а):

А насчет боттома и значения булевского типа, по крайней мере в программизме языка моего примера это совершенно разные вещи.

А каково значение символа $\perp$ в языке Вашего примера?

[_Ivana]

Так вот чтобы не возникали подобные вопросы с аксиомами эквивалентности и правом их игнорирования, и предлагается ввести простейшую конструкцию - всегда_ложный_предикат_на_любом_аргументе (R)

Насчет боттома - все достаточно сложно, чтобы я смог это понять и тем более грамотно объяснить. Это такое волшебное значение, которое может принимать любой тип (и конкретно в языке, и, насколько я понимаю, в теории типов как таковой, но в последнем не уверен), которое было введено в язык и сразу на многое повлияло (на тотальность/нетотальность как минимум, вроде), которое является минимальной неподвижной точкой любого типа, которые в свою очередь сами могут быть определены как неподвижные точки алгебр функторов (если ничего не путаю в терминах). В общем, страх, ужас и красота. Повторно прошу извинить мой невнятный ответ вследствие отсутствия у меня понимания данного вопроса.

[arseniiv]

epros в сообщении #1111488 писал(а):

Предлагаю упростить до $\varnothing=\{x|\perp\}$.

Это запросто, но обычно почему-то пропозиционную константу для противоречия не включают.

-- Сб апр 02, 2016 22:00:05 --

Несколько комментариев:
1.

_Ivana в сообщении #1111551 писал(а):

и конкретно в языке, и, насколько я понимаю, в теории типов как таковой, но в последнем не уверен

Не во всех теориях типов оно есть. В HoTT, например, тип $\mathbf0$ не содержит ничего, т. е., если теория непротиворечива (не помню, известно ли это сейчас), не выводимо ни одно из $x:\mathbf 0$ для любого терма $x$, так что $\perp$ там нет.

2. Типичными значениями, равными $\perp$, являются функции, генерирующие исключение, содержащие бесконечный цикл или не определённые на нужном наборе аргументов.

3. Пример _Ivana с «неправильным» инстансом работает только по двум причинам:
• почему-то в документации к классу Eq на его методы не наложены ограничения, эквивалентные хоть какому-то ослаблению аксиом равенства (я даже не увидел условия a == b = not (a /= b) для случаев, когда a == b и a /= b оба определены);
• если бы они и были наложены, их нельзя выразить на самом хаскеле. Их записывают в документации и надеются на разумность писателей инстансов.
То есть, по-хорошему, он не работает.

[epros]

_Ivana в сообщении #1111551 писал(а):

Так вот чтобы не возникали подобные вопросы с аксиомами эквивалентности и правом их игнорирования, и предлагается ввести простейшую конструкцию - всегда_ложный_предикат_на_любом_аргументе (R)

Тут я совершенно с Вами согласен. Есть такой подход к формализации логики, согласно которому упомянутый "всегда_ложный_предикат_на_любом_аргументе" (иногда его называют "абсурд") является первичным ("неопределяемым") понятием. В таком подходе аксиома $(p \to \perp) \to \neg p$ рассматривается как определение отрицания (то бишь, отрицание рассматривается уже как "определяемое" понятие ).

Тем не менее, некоторые злые люди сочли наличие данного символа в языке логики излишним, ибо его, вроде как, всегда можно заменить каким-нибудь $p \wedge \neg p$ (вопрос только в том, что ставить на место $p$). К тому же в прикладных теориях всегда найдётся что записать в качестве абсурда. Например, в арифметике Пеано за признанный абсурд считается $0=1$. Ну, а некоторые пошли дальше и предложили рассматривать аксиомы эквивалентности не в качестве прикладных, а включить их в логику. Отсюда появилось ещё одно признанное написание абсурда - пресловутое $x \ne x$.

Но я считаю, что всё же в логике нужно иметь отдельный символ для абсурда. А символу "$=$" и сопутствующим ему аксиомам эквивалентности - место в прикладных теориях.

[_Ivana]

arseniiv в сообщении #1111553 писал(а):

я даже не увидел условия a == b = not (a /= b) для случаев, когда a == b и a /= b оба определены

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

-- 02.04.2016, 20:29 --

epros в сообщении #1111559 писал(а):

А символу "$=$" и сопутствующим ему аксиомам эквивалентности - место в прикладных теориях.

Кстати, на множестве может быть вообще не определено отношение эквивалентности - и такие примеры есть, и вполне признанные, в отличие от моего смущающего инстанса. Но и из таких множеств разумеется можно выделять пустое подмножество. Весь вопрос в предикате абсурда - согласен, что это не самая существенная вещь в определении, и решается просто, но стандартное /= все-таки немного сужает определение.

[arseniiv]

_Ivana в сообщении #1111560 писал(а):

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

Верно — если определить что-то одно, оно выполняется. А если оба, не обязательно!

_Ivana в сообщении #1111560 писал(а):

А требовать соблюдение аксиом эквивалентности имхо - нарушение общности.

Почему? Если аккуратно учесть $\perp$, что обычно делают в нужных случаях, всё будет прекрасно и в прикладном смысле тоже: вроде, если равенство значений типа только приближённое, инстанс для Eq для него не определяют? Хотя это человеческий фактор, надо конкретные пакеты рассматривать.

_Ivana в сообщении #1111560 писал(а):

Кстати, на множестве может быть вообще не определено отношение эквивалентности - и такие примеры есть, и вполне признанные

Ну, теории множеств обычно комплектуются всё-таки символом $=$ и аксиомами равенства. Без этого плохо. Отношения эквивалентности — это уже элементы этих теорий, другая история.

[_Ivana]

arseniiv например, дли типа (->) инстанс Eq не определен. И именно для этого типа я и определил его в своем примере. И без отношения равенства множество элементов данного типа вполне можно определить в языке (и в его аксиоматике), нумеровать\выбирать его элементы, объединять.... И не особо плохо получается. Ну нельзя вычислять пересечения/дополнения, да.

[arseniiv]

_Ivana в сообщении #1111565 писал(а):

например, дли типа (->) инстанс Eq не определен

Для типов a -> b (это можно назвать «инстансосхемой» по аналогии со схемами аксиом — одно определение соответствует целой куче инстансов), т. к. у (->) нет значений, но да.

Я всё-таки имел в виду математическую теорию, и я не вижу, как в теории для хаскеля можно было бы тоже обойтись без равенства. Конечно, это не было бы равенство как метод Eq, то метод типа Eq a => a -> a -> Bool, а значения Bool — это элементы области интерпретации теории, и лучше нам их не путать со значениями формул теории.

[Someone]

Geen в сообщении #1111338 писал(а):

(Someone)

Someone в сообщении #1111314 писал(а):

anderlo в сообщении #1111311 писал(а):

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

Потому что конструкция $X=\{x:\Phi(x)\}$ — это сокращение высказывания $x\in X\Leftrightarrow\Phi(x)$. По-моему, Вам об этом уже писали.

Someone в сообщении #1111289 писал(а):

Anton_Peplov в сообщении #1111287 писал(а):

Но про двухтомник Фреге - это было, точно было. Известная история.

Я Фреге не читал, но, насколько я знаю, у него была неограниченная аксиома свёртывания, разрешавшая образование множества $\{x:\Phi(x)\}$ для любого высказывания $\Phi(x)$. Из этой аксиомы получить множество всех множеств — плёвое дело.

Немного напрягает...

(Оффтоп)

Я не совсем понял, что именно Вас напрягает. У меня две гипотезы.

1) Вы увидели противоречие в моих высказываниях.
На обсуждаемую конструкцию можно смотреть по-разному.
а) То, что обсуждается в данной теме: способ определить терм, являющийся множеством. В этом случае требуется доказательство того, что получается действительно множество. Если высказывание $\Phi(x)$ имеет некоторый специальный вид, это делается легко с помощью аксиомы выделения или аксиомы подстановки; можно заранее ограничить допустимые высказывания, чтобы не иметь проблем, либо не признавать этот терм множеством и запретить его использовать, если нет доказательства, что получается действительно множество.
б) Можно использовать эту конструкцию как способ ввести классы в ZFC. Подробности можно посмотреть в статье Джозефа Р. Шенфильда "Аксиомы теории множеств", опубликованной в сборнике "Справочная книга по математической логике. Часть II.Теория множеств", Москва, "Наука", 1982.

2) (Неприятный для меня вариант.) Вы увидели знаменитое "Не читал, но осуждаю". Нет, не осуждаю. Но эта история довольно известная.
Увидев ваше сообщение, я разыскал первую часть работы Фреге, на которую обычно ссылаются по этому поводу, и стал разбираться. Надо сказать, что Фреге характеризуется как "математик, логик, философ", и далеко не очевидно, кого там больше. На меня этот текст объёмом 64 страницы и 109 параграфов произвёл тягостное впечатление из-за того, что формул там практически нет, но зато масса философских рассуждений. Цель работы — обоснование арифметики. В связи с этим речь идёт о "понятиях" ("свойствах"), которые я формализовал бы с помощью конструкции, обсуждаемой в данной теме, но у Фреге каких-либо обозначений для этого нет. Какие-либо ограничения на допустимые "понятия" или "свойства" не рассматриваются, никакие аксиомы явно не формулируются. Вводится понятие "равночисленности понятий", которое соответствует понятию равномощности в теории множеств. С помощью этого определяются натуральные числа, а также рассматриваются "бесконечные числа", соответствующие кардиналам в теории множеств. Фреге также сравнивает свой подход с подходом Кантора и отмечает, что Кантор больше интересуется порядковыми числами (ординалами). Аксиоматизацией теории множеств или арифметики Фреге не занимается, да и вообще идея аксиоматизации теории множеств появилась, видимо, позже.