Что значит "предъявить объект" в смысле BHK?

[epros]

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

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

Вот, вот, я как раз сильно сомневаюсь в её праве называться конструктивной. Ибо независимо от используемой логики, наличие аксиомы, утверждающей существование пустого множества, с точки зрения интерпретации BHK не может быть законным, ибо оное пустое множество никоим образом не было "предъявлено".

[epros]

Хм. Кстати, а вот интересно, можно ли вообще доказать существование и единственность чего-то невыразимого замкнутым термом, если в теории нет аксиом, выражающих существование?

[arseniiv]

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

Вот, вот, я как раз сильно сомневаюсь в её праве называться конструктивной. Ибо независимо от используемой логики, наличие аксиомы, утверждающей существование пустого множества, с точки зрения интерпретации BHK не может быть законным, ибо оное пустое множество никоим образом не было "предъявлено".

Но в ней ведь можно будет определить $\varnothing$, раз в ней $\vdash\exists!e\forall x\;x\notin e$, и полученная теория уже будет подходить.

[epros]

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

Но в ней ведь можно будет определить $\varnothing$, раз в ней $\vdash\exists!e\forall x\;x\notin e$, и полученная теория уже будет подходить.

Тут есть какой-то непонятный момент. Классическая аксиома пустого множества - о существовании, а не о единственности. Единственность доказывается с использованием аксиомы объёмности. Но аксиому существования, вроде как, принимать неконструктивно. А как без неё доказать единственность? Замкнутый круг?

Хотя... Если взять формулу $\forall y~y \notin x$ (обозначим её $\psi$), которая означает "$x$ является пустым множеством", то $\psi[x_1|x] \wedge \psi[x_2|x] \to (\forall y~y \in x_1 \leftrightarrow y \in x_2)$, а в силу аксиомы объёмности $\psi[x_1|x] \wedge \psi[x_2|x] \to x_1=x_2$. Т.е. для любого $x$ верно $\forall y~\psi[y|x] \to x=y$. В итоге получаем, что безо всяких аксиом существования можно доказать $\forall x~\delta$, где $\delta$ обозначает формулу $\forall y~\psi[y|x] \to x=y$.

Далее можно от $\forall x~\delta$ перейти к $\exists x~\delta$. Как я понимаю, способ такой: Сначала применяем правило конкретизации всеобщности $\forall x~\delta \vdash \delta[y|x]$, а потом правило абстракции до существования $\delta[y|x] \vdash \exists x~\delta$. В итоге получим $\exists x \forall y~\psi[y|x] \to x=y$, что означает "если пустое множество существует, то оно единственно". Увы, существование так и остаётся недоказанным, ибо импликацию в обратную сторону доказать не получается...

[Qlin]

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

Но аксиому существования, вроде как, принимать неконструктивно.

Аксиома существования пустого множества является избыточной. Зачем принимать ее, если можно использовать схему выделения?

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

если теория не определяет ни одной константы или не определяет равенства

Что вы подразумеваете под теорией, определяющей равенство? Аксиомы равенства — присоединяемые, и как их присоединить к собственной аксиоматике теории — известно для каждой конкретной сигнатуры.

[epros]

Qlin в сообщении #1303102 писал(а):

Аксиома существования пустого множества является избыточной
. Зачем принимать ее, если можно использовать схему выделения?

Во-первых, там сказано, что "из схемы выделения следует существование хотя бы одного множества", что для стандартной схемы выделения (Axiom 3 of [Kunen] p. 11) неверно (и про это там тоже сказано).
Во- вторых, схема выделения тоже является утверждением о существовании, которое согласно BHK должно сопровождаться каким-то "предъявлением" множества. И мне было бы интересно понять каким.

Qlin в сообщении #1303102 писал(а):

Что вы подразумеваете под теорией, определяющей равенство? Аксиомы равенства — присоединяемые, и как их присоединить к собственной аксиоматике теории — известно для каждой конкретной сигнатуры.

Вы говорите о логике с равенством, а я - про то, что есть ещё логика без равенства, в которой могут быть сформулированы теории без равенства.

P.S. Всё же у меня остаётся сильное подозрение, что если аксиоматика строго следует BHK, т.е. не содержит утверждений о существовании, то доказать единственность можно только для того, что выражается замкнутым термом. Например, в арифметике Пеано - только $0, S0, SS0$ и т.д. А какой тогда смысл во всём этом? Вся "конструктивность" сведётся к тому, что каждый объект должен иметь "имя собственное".

[Qlin]

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

для стандартной схемы выделения (Axiom 3 of [Kunen] p. 11) неверно

А потому что стандарт запрещает выделять по той же переменной, которая связана существованием. На metamath такое ограничение не применяется. Но поскольку Kunen формализует ZFC, а не какую-то более общую теорию, то у него можно вывести существование из других соображений.

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

Во- вторых, схема выделения тоже является утверждением о существовании, которое согласно BHK должно сопровождаться каким-то "предъявлением" множества. И мне было бы интересно понять каким.

Схема выделения не является утверждением. Это бесконечная совокупность утверждений. Тогда может быть каждое из них должно сопровождаться "предъявлением" своего множества?

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

Вы говорите о логике с равенством, а я - про то, что есть ещё логика без равенства, в которой могут быть сформулированы теории без равенства.

Я не говорю о логике с равенством. Я спрашиваю о том, как теория может определять равенство. Чисто конкретно вот этот момент неясен.

[Qlin]

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

доказать единственность можно только для того, что выражается замкнутым термом. Например, в арифметике Пеано - только $0, S0, SS0$ и т.д. А какой тогда смысл во всём этом? Вся "конструктивность" сведётся к тому, что каждый объект должен иметь "имя собственное".

Тут еще придется разбираться, сколько имен собственных может быть у одного объекта. Скажем, ноль может быть обозначен и как $0$, и как $00$, и как $0.0$. Это разные символы, обозначающие одно и то же. И когда в сигнатуре несколько константных символов, следует обосновать в качестве отдельной теоремы, почему они не взаимозаменяемы.

[epros]

Qlin в сообщении #1303131 писал(а):

Схема выделения не является утверждением. Это бесконечная совокупность утверждений. Тогда может быть каждое из них должно сопровождаться "предъявлением" своего множества?

Может быть. Это же не я придумал, а BHK. А я пытаюсь понять что это значит.

Qlin в сообщении #1303131 писал(а):

Я не говорю о логике с равенством. Я спрашиваю о том, как теория может определять равенство. Чисто конкретно вот этот момент неясен.

Обыкновенно. Могут быть теории с равенством (в стандартном смысле) или без него. При этом относить ли определение равенства к логике или к теории - вопрос терминологический.

Qlin в сообщении #1303139 писал(а):

Тут еще придется разбираться, сколько имен собственных может быть у одного объекта. Скажем, ноль может быть обозначен и как $0$, и как $00$, и как $0.0$. Это разные символы, обозначающие одно и то же. И когда в сигнатуре несколько константных символов, следует обосновать в качестве отдельной теоремы, почему они не взаимозаменяемы.

Это без разницы. Важно, что есть замкнутый терм $0$, а значит существование (как и единственность) такого $x$, что $x=0$, тривиально обосновывается. А то, что у нуля есть "другие имена" типа $0+0$ или $0 \times S0$, нас уже не должно беспокоить.

[arseniiv]

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

Единственность доказывается с использованием аксиомы объёмности. Но аксиому существования, вроде как, принимать неконструктивно.

Ну зачем так-то сразу. Если принимать то, что написал george66, то по крайней мере насчёт пустого множества всё будет соблюдено: мы можем доказать существование аксиомой, но можем доказать и единственность, притом даже не усиливая свойство (за это нам точно должны где-нибудь поставить плюсик). Вот не могли бы доказать единственность — тогда эту аксиому долой.

То же со многими другими аксиомами типа существования пары, объединения, аксиомы выделения и т. д. — даже усиливать свойство не нужно. Вот аксиома бесконечности уже не такая хорошая, но и она проходит тест. Остаётся разобраться с остатками аксиом и всеми другими теоремами о существовании. Понятно, аксиома выбора как раз идёт лесом.

[epros]

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

Вот не могли бы доказать единственность — тогда эту аксиому долой.

Мне этот подход кажется странным. Получается, что если у нас уже есть аксиомы, из которых следует "если существует, то единственно", то мы можем смело принимать аксиому существования? По-моему, правильнее уж тогда сразу добавить константу. И с точки зрения BHK выглядит логичнее - так мы сначала "предъявляем" объект (по крайней мере, его "имя"), а уж потом утверждаем существование, а не наоборот.

-- Ср апр 11, 2018 16:31:59 --

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

Вот аксиома бесконечности уже не такая хорошая, но и она проходит тест.

Какой-то слишком лёгкий тест. Получается, что "предъявить бесконечность" означает, например, доказать единственность какого-нибудь минимального индуктивного множества?

-- Ср апр 11, 2018 16:43:32 --

О, а давайте я Вам таким образом "обосную" существование нечётного совершенного числа: Для начала примем существование нечётных совершенных чисел за аксиому. Поскольку среди них есть минимальное, доказано, что минимальное нечётное совершенное число единственно. Поскольку доказательством единственности мы "предъявили" пример нечётного совершенного числа, мы можем считать аксиому о существовании нечётных совершенных чисел "конструктивной".

Мне такой способ рассуждения не представляется убедительным.

[arseniiv]

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

Мне этот подход кажется странным. Получается, что если у нас уже есть аксиомы, из которых следует "если существует, то единственно", то мы можем смело принимать аксиому существования? По-моему, правильнее уж тогда сразу добавить константу. И с точки зрения BHK выглядит логичнее - так мы сначала "предъявляем" объект (по крайней мере, его "имя"), а уж потом утверждаем существование, а не наоборот.

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

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

Получается, что "предъявить бесконечность" означает, например, доказать единственность какого-нибудь минимального индуктивного множества?

Ну, кто ж виноват, что эту аксиому так назвали. Индуктивное множество предъявим, а если не нравится звать его бесконечным, это делать не обязательно. Или я вас вообще не понял.

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

О, а давайте я Вам таким образом "обосную" существование нечётного совершенного числа: Для начала примем существование нечётных совершенных чисел за аксиому. Поскольку среди них есть минимальное, доказано, что минимальное нечётное совершенное число единственно. Поскольку доказательством единственности мы "предъявили" пример нечётного совершенного числа, мы можем считать аксиому о существовании нечётных совершенных чисел "конструктивной".

Мне такой способ рассуждения не представляется убедительным.

Я даже не знаю, есть ли смысл в понятии «конструктивная (даже в контексте остальных аксиом) аксиома». Будем ждать…

-- Ср апр 11, 2018 19:45:21 --

Эх, мне-то хорошо, мой любимый теоретико-типовой формализм не различает конструктивные доказательства и конструктивные объекты. Притом любой такой объект есть терм некоторой алгебры термов, или, иначе говоря, любому объекту соответствует «вывод». Однако элементарные конструкции вовсе не обязаны отвечать операциям над чем-то, что нам удобнее считать конечным.

[epros]

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

я видел интуиционистскую теорию множеств без констант и функциональных символов для остального

Ну, может они ошиблись в том, что они интуиционисты. А может наоборот - Брауэр с Гейтингом и Колмогоровым слишком много от них требуют.

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

Индуктивное множество предъявим

Как предъявим? Мы тут, вроде, пришли к тому, что "предъявить" - это значит написать такую формулу, которой соответствует единственный объект. Далее мнения разошлись в том, считать ли доказательство единственности этого объекта предусловием или послеусловием принятия соответствующей аксиомы существования. Как я понял, Вы за второй вариант. Т.е. если из аксиом ZF (включая аксиому бесконечности) доказывается единственность минимального индуктивного множества, значит с аксиомой бесконечности "всё в порядке".

Я не считаю это "предъявлением" минимального индуктивного множества, потому что по совершенно такой же схеме можно "предъявить" и минимальное нечётное совершенное число, что уж явно неконструктивно.

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

а если не нравится звать его бесконечным

Дело не в названии. Оно вполне адекватно, ибо индуктивное множество - и есть бесконечное.

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

Я даже не знаю, есть ли смысл в понятии «конструктивная (даже в контексте остальных аксиом) аксиома».

Я здесь употребляю слово "конструктивно" в смысле "соответствует BHK". Аксиома - это утверждение, которое можно неформально проверить на соответствие BHK. Вопрос только в том, как эту проверку формализовать.

[arseniiv]

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

Ну, может они ошиблись в том, что они интуиционисты. А может наоборот - Брауэр с Гейтингом и Колмогоровым слишком много от них требуют.

Ситуация мне видится так: голая интуиционисткая логика отвечает только конструктивности доказательств, а конструктивность объектов теорий на её основе — отдельный вопрос. Я не знаю, есть ли какое-то название для теорий, в которых всё ещё не выводятся никакие тавтологии кроме интуиционистских, но при этом что-то неладно с конструктивностью объектов (в любом её понимании), но можно было бы не отказывать им в конструктивности уж целиком.

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

Далее мнения разошлись в том, считать ли доказательство единственности этого объекта предусловием или послеусловием принятия соответствующей аксиомы существования. Как я понял, Вы за второй вариант. Т.е. если из аксиом ZF (включая аксиому бесконечности) доказывается единственность минимального индуктивного множества, значит с аксиомой бесконечности "всё в порядке".

Я больше за вариант не рассматривать аксиоматику теории. Просто есть теория, и если она обладает свойством, она конструктивная, а если нет — неконструктивная. Пользы в понятии конструктивности отдельной аксиомы я почему-то пока не вижу.

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

Я не считаю это "предъявлением" минимального индуктивного множества, потому что по совершенно такой же схеме можно "предъявить" и минимальное нечётное совершенное число, что уж явно неконструктивно.

Просто потому что мы не будем знать, какому терму $S^n0$ оно равно? Существование у всех термов нормальной формы некоторого вида — отдельное от конструктивности требование, насколько я в курсе.

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

Аксиома - это утверждение, которое можно неформально проверить на соответствие BHK. Вопрос только в том, как эту проверку формализовать.

Я предлагаю не проверять отдельные аксиомы.

[epros]

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

Я больше за вариант не рассматривать аксиоматику теории. Просто есть теория, и если она обладает свойством, она конструктивная, а если нет — неконструктивная. Пользы в понятии конструктивности отдельной аксиомы я почему-то пока не вижу

Это тот же смысл, о котором говорите Вы: Если добавление к конструктивной теории аксиомы делает её неконструктивной, то эта аксиома - неконструктивна, если оставляет теорию конструктивной - то конструктивна.

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

Просто потому что мы не будем знать, какому терму $S^n0$ оно равно?

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