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

[arseniiv]

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

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

Но у меня в результате нет проблем с той же аксиомой бесконечности — она ведь оставляет теорию конструктивной.

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

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

Но «предъявить» — это же не обязательно предъявить терм какой-то особой формы.

[epros]

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

Но у меня в результате нет проблем с той же аксиомой бесконечности — она ведь оставляет теорию конструктивной.

Чем это можно подтвердить?

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

Но «предъявить» — это же не обязательно предъявить терм какой-то особой формы.

Ну вот, опять возвращаемся к исходному вопросу: Что значит "предъявить"? Мне такое "предъявление", когда мы из принятой от балды аксиомы существования доказываем единственность, не представляется убедительным.

[arseniiv]

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

Чем это можно подтвердить?

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

Вообще надо уже найти какую-нибудь конкретную интуиционистскую теорию множеств и посмотреть. Я думал, вам это интереснее, чем мне, а вы до сих пор этого не сделали(?).

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

Ну вот, опять возвращаемся к исходному вопросу: Что значит "предъявить"? Мне такое "предъявление", когда мы из принятой от балды аксиомы существования доказываем единственность, не представляется убедительным.

Как хотите.

Меня удовлетворяют теории типов, а что делать с интуиционистскими теориями, я не знаю.

[george66]

Конструктивность - это формальное свойство теории. Типа "если что-то доказали, то можем сразу вычислять". Оно не говорит, что теория отражает реальность в каком угодно смысле. Интуиционистская теория множеств (без аксиомы выбора) конструктивна, но ничуть не менее фантастична, чем классическая. Аксиому "существует нечётное совершенное число" добавлять опасно: если такого числа нет, теория может получиться противоречивой. Если же такого числа нет, но это очень трудно доказать (например, вдруг нельзя доказать в ZF), тогда такую аксиому добавлять можно, но полученная теория не будет конструктивной! Дело в том, что принцип "в каждом непустом множестве натуральных чисел есть наименьшее" не выводим в интуиционистской теории (он выводится от противного из математической индукции по натуральным числам)

[epros]

george66 в сообщении #1303423 писал(а):

Конструктивность - это формальное свойство теории. Типа "если что-то доказали, то можем сразу вычислять". Оно не говорит, что теория отражает реальность в каком угодно смысле.

Спасибо, про реальность я понимаю, поэтому первый вариант сразу отбросил. Мне хотелось бы понять, что все эти слова ("вычислить" или "предъявить") означают на деле, то бишь как именно мы должны проверять конструктивность теории или предъявлять объекты, существование которых она утверждает.

george66 в сообщении #1303423 писал(а):

Интуиционистская теория множеств (без аксиомы выбора) конструктивна, но ничуть не менее фантастична, чем классическая.

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

Вопрос в том, как проверить конструктивность. Например, я не понимаю, как можно в конструктивном смысле "предъявить" множество натуральных чисел (или если мы говорим о теории множеств - минимальное индуктивное множество). Неужели Вы согласны с тем, что можно сначала принять аксиому бесконечности (т.е. утверждающую существование некоторых объектов), потом с её помощью доказать единственность какого-то из них (минимального индуктивного множества), а потом сказать: "Вот видите, всё у нас получилось конструктивно"?

george66 в сообщении #1303423 писал(а):

Аксиому "существует нечётное совершенное число" добавлять опасно: если такого числа нет, теория может получиться противоречивой.

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

george66 в сообщении #1303423 писал(а):

полученная теория не будет конструктивной! Дело в том, что принцип "в каждом непустом множестве натуральных чисел есть наименьшее" не выводим в интуиционистской теории (он выводится от противного из математической индукции по натуральным числам)

О, вот это интересно. Т.е. Вы утверждаете, что разница между "конструктивной" теорией множеств с аксиомой бесконечности и "неконструктивной" арифметикой с аксиомой существования нечётных совершенных чисел заключается в том, что в первой выводимо существование минимального индуктивного множества, а во второй невыводимо существование минимального нечётного совершенного числа?

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

[epros]

george66 в сообщении #1303423 писал(а):

принцип "в каждом непустом множестве натуральных чисел есть наименьшее" не выводим в интуиционистской теории (он выводится от противного из математической индукции по натуральным числам)

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

А если множество не рекурсивно, то я не уверен в том, что утверждение о его существовании имеет какой-то конструктивный смысл.

[george66]

Чисто технически: возьмём некоторое множество натуральных чисел $\varphi(n)$. Предположим, что в нём нет наименьшего элемента и докажем $\forall n\neg\varphi(n)$. Берём формулу $\forall n\leqslant k\neg\varphi(n)$ обозначим её $\psi(k)$. Индукцией по $k$ докажем $\forall k\psi(k)$. Для нуля это верно, иначе $\varphi(0)$ и ноль был бы наименьшим элементом. Шаг индукции $\psi(k)\Rightarrow\psi(k+1)$ верен, иначе $k+1$ был бы наименьшим элементом. Это классическое доказательство от противного. По поводу рекурсивных множеств и алгоритма, перебирающего -- это дополнительная аксиома, называется "принцип Маркова".

[epros]

george66, принцип Маркова - это да, куда ж конструктивизму без него:

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

По-моему, без принципа Маркова даже про примитивно-рекурсивные функции не удастся сформулировать никаких общих утверждений. А как без них? Например, вот такая функция: $f(x) = x^{x^x}$. Если буквально следовать интерпретации BHK, то для каждого $x$ мы должны провести всю цепочку вычислений до конца, чтобы убедиться в наличии значения функции. Но уже при $x=10$ это становится технически затруднительно. Как известно, всюду определённость таких функций элементарно доказывается мат. индукцией. Но доказательство с использованием индукции с точки зрения BHK является "косвенным", т.е. мы продемонстрировали, что предположение о несуществовании значения функции противоречит аксиоме индукции, но конкретного значения у нас нет. Спасает только принцип Маркова...

К тому же, насколько я знаю, он является "допустимым" в арифметике Гейтинга и интуиционистском исчислении предикатов самом по себе.

Я тут пошарил, и выяснил, что теория проверяется на конструктивность посредством проверки наличия у неё как минимум двух свойств:
1) Свойство дизъюнкции: Если теория доказывает $\alpha \vee \beta$, то она доказывает либо $\alpha$, либо $\beta$.
2) Свойство существования: Если теория доказывает $\exists x~\varphi$, где формула $\varphi$ не имеет свободных переменных кроме $x$, то существует терм $t$, для которого теория доказывает $\varphi[t|x]$.

Есть ещё пара "конструктивных" свойств теории. Особенно интересно правило Чёрча, которое в одной из формулировок звучит: Если теория доказывает $\forall x \exists y~x \in \mathbb{N} \wedge y \in \mathbb{N} \to \varphi$, то она доказывает $\forall x~x \in \mathbb{N} \to \varphi[f(x)|y]$, где $f$ - некая общерекурсивная функция.

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

[epros]

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

2) Свойство существования: Если теория доказывает $\exists x~\varphi$, где формула $\varphi$ не имеет свободных переменных кроме $x$, то существует терм $t$, для которого теория доказывает $\varphi[t|x]$.

Вот что интересно, утверждается, что IZF обладает свойством существования. Но ведь в языке этой теории нет функциональных символов (включая константы). Т.е. все термы в ней представлены только переменными. А значит свойство существования для неё должно звучать так: Если IZF доказывает $\exists x~\varphi$, где формула $\varphi$ не имеет свободных переменных кроме $x$, то IZF доказывает $\varphi$. Т.е. из любого существования следует всеобщность?

Что я здесь понял не так?

[george66]

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

Вот что интересно, утверждается, что IZF обладает свойством существования. Но ведь в языке этой теории нет функциональных символов (включая константы). Т.е. все термы в ней представлены только переменными. А значит свойство существования для неё должно звучать так: Если IZF доказывает $\exists x~\varphi$, где формула $\varphi$ не имеет свободных переменных кроме $x$, то IZF доказывает $\varphi$. Т.е. из любого существования следует всеобщность?

Что я здесь понял не так?

Где такое утверждается? В такой форме это неверно. Или надо добавить много термов, или формулировать через $\exists!$

[epros]

george66 в сообщении #1303889 писал(а):

Где такое утверждается? В такой форме это неверно. Или надо добавить много термов, или формулировать через $\exists!$

Вот в этой статье википедии есть оба утверждения - и про то, что такое "свойство существования", и про то, что оно доказано для IZF.

[george66]

В такой форме это неверно.