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

[epros]

Согласно интерпретации Брауэра-Гейтинга-Колмогорова (сокращённо - BHK) существование объекта $x$ со свойством $\varphi(x)$ может быть доказано только предъявлением такового объекта. Вопрос заключается в том, что формально означает "предъявление" объекта, для которого мы потом доказываем, что он обладает указанным свойством?

Я рассмотрел такие варианты:

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

2. Определение константы в языке теории. Например, можно считать, что существование числа "нуль" доказано уже в силу того, что в языке арифметики Пеано определена константа $0$. Этот вариант я полагаю приемлемым, но недостаточно общим, ибо есть множество теоретических объектов, для обозначения которых никогда не вводились и скорее всего никогда не будут вводиться константы.

3. Предъявление формулы теории, для которой доказана единственность соответствующего объекта. Т.е. мы должны записать формулу $\psi$ и доказательства $\exists x \forall y~\psi[y|x] \leftrightarrow x=y$ (где $\psi[y|x]$ - результат подстановки $y$ вместо всех свободных вхождений $x$ в формулу $\psi$, причём если имелись связанные вхождения $y$ в формулу $\psi$, во избежание конфликтов они должны быть заменены на какую-нибудь новую переменную) - единственности объекта со свойством $\psi$, и $\forall x~\psi \to \varphi$ - наличия у этого объекта свойства $\varphi$.

Этот вариант представляется мне наиболее подходящим, хотя:
а) Он требует, чтобы в теории было определено отношение равенства, удовлетворяющее соответствующим аксиомам.
б) Доказательство единственности предполагает доказательство существования объекта $x$ со свойством $\forall y~\psi[y|x] \leftrightarrow x=y$, которое, в свою очередь, должно соответствовать BHK. В принципе, это может породить рекурсию доказательств, которая не будет иметь конца. Но я полагаю, что в некоторых случаях эту рекурсию можно будет закончить сведением к пункту 2 - когда доказательство единственности сведётся к доказательству равенства константе: Например, единственность $x$ со свойством $x=0$ очевидна в силу того, что при подстановке в указанную выше формулу единственности мы получим тавтологию $\exists x \forall y~y=0 \leftrightarrow x=y$.

4. Предъявление класса эквивалентности объектов $x$, обладающих свойством $\varphi(x)$. Например, объект арифметики "число два" можно трактовать как множество $\{x | x=SS0\}$ (здесь в качестве отношения эквивалентности выступает арифметически доказанное равенство числу, обозначенному замкнутым термом $SS0$).

Этот вариант представляется мне несоответствующим BHK. Например, действительное число мы должны трактовать как класс эквивалентности фундаментальных последовательностей рациональных чисел. Нетрудно записать какую-нибудь формулу $f(n)$, определяющую фундаментальную последовательность рациональных чисел. И нетрудно определить, что последовательности рациональных чисел $f(n)$ и $g(n)$ "эквивалентны" ($f(n) \sim g(n)$) тогда и только тогда, когда их разность имеет пределом нуль. Но класс эквивалентности для $f(n)$ оказывается неразрешимым! Т.е. неизвестно, каким образом его можно "предъявить".

[arseniiv]

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

[epros]

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

Мне всегда казалось, что BHK (по крайней мере, сейчас) считается просто интуитивными неформальными соображениями

Да я не против. Просто мне казалось, что понять интуитивные неформальные соображения - это значит формализовать их. Или, если не получилось, то убедиться в том, что эти соображения - чушь.

[arseniiv]

Фишка в том, что формализовать бывает можно разными способами (я кэп).

[epros]

Ну, как ещё? Готов рассмотреть вариант № 5

[arseniiv]

Не, я про то, что вы хотите выбрать лишь один «самый» вариант. А раз есть неэквивалентные формализации, это сделать не получится.

[Qlin]

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

$\exists x \forall y~\psi[y|x] \leftrightarrow x=y$ (где $\psi[y|x]$ - результат подстановки $y$ вместо всех свободных вхождений $x$ в формулу $\psi$

Боюсь, формулу $(\exists x \forall y~\psi[y|x]) \leftrightarrow x=y$ доказать невозможно, поскольку в ней есть свободные переменные. Кроме того, непонятно, зачем квантифицировать $\psi[y|x]$ по переменной $x$, если там все $x$ заменены на $y$.

[george66]

Номер 3. Если можно доказать $\exists x\varphi(x)$, то должно быть можно доказать $\exists ! x \psi(x)$, где свойство $\psi(x)$ не слабее $\varphi(x)$ (то есть $\forall x(\psi(x)\Rightarrow\varphi(x))$
Если мы доказали, что нечто существует, можно указать его точно, усилив определяющее условие.

-- 09.04.2018, 07:42 --

Если в языке достаточно много термов, можно проще. Если доказуемо $\exists x\varphi(x)$, должно быть доказуемо $\varphi(t)$ для некоторого терма $t$.

[epros]

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

Боюсь, формулу $(\exists x \forall y~\psi[y|x]) \leftrightarrow x=y$ ...

А зачем ставить скобки там, где их явно быть не должно?

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

Номер 3.

Спасибо. Я так и предполагал.

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

Если в языке достаточно много термов, можно проще. Если доказуемо $\exists x\varphi(x)$, должно быть доказуемо $\varphi(t)$ для некоторого терма $t$.

Как я понимаю, это частный случай номера 3.

[Qlin]

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

А зачем ставить скобки там, где их явно быть не должно?

А смысл не меняется, если поставить эти скобки. Формула $(\exists x \forall y~\psi[y|x]) \leftrightarrow x=y$ эквивалентна вашей $\exists x \forall y~\psi[y|x] \leftrightarrow x=y$.

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

Если можно доказать $\exists x\varphi(x)$, то должно быть можно доказать $\exists ! x \psi(x)$, где свойство $\psi(x)$ не слабее $\varphi(x)$ (то есть $\forall x(\psi(x)\Rightarrow\varphi(x))$
Если мы доказали, что нечто существует, можно указать его точно, усилив определяющее условие.

Мне кажется, не должно и не можно. Пусть сигнатура теории включает в себя двуместный предикатный символ равенства и ничего больше. Пусть собственная аксиоматика теории состоит из единственной аксиомы следующего вида: $\forall x,y,z \ (x \neq y \rightarrow (x=z \lor y=z))$. В роли вашей $\varphi(x)$ выберем $x=x$ (равенство объекта самому себе). Усильте это свойство до $\psi(x)$, чтобы можно было доказать $\exists ! x \psi(x)$.

[arseniiv]

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

А смысл не меняется, если поставить эти скобки. Формула $(\exists x \forall y~\psi[y|x]) \leftrightarrow x=y$ эквивалентна вашей $\exists x \forall y~\psi[y|x] \leftrightarrow x=y$.

Зависит от соглашения о расстановке скобок.

-- Вт апр 10, 2018 03:28:59 --

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

Мне кажется, не должно и не можно.

В общем случае в классике да. Но здесь это фигурирует как формулировка требований BHK. Ваша теория им не удовлетворяет — ну что ж, она и не видится неформально «конструктивной» — два объекта, о которых она говорит, никак нельзя маркировать, они взаимозаменяемы.

[Qlin]

(Оффтоп)

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

Зависит от соглашения о расстановке скобок.

Ну, если зависит, значит нужны оговорки. Но мне казалось, что для области действия квантора и скобочных расстановок существуют некие общепринятые стандарты. Разве кто-то способен прочитать $\forall x \varphi \rightarrow \exists x \varphi $ как $\forall x (\varphi \rightarrow \exists x \varphi)$? Разве такой вариант тоже встречается в литературе?

[arseniiv]

(Оффтоп)

В неформальном рассмотрении скобки могут вообще опускаться не по простой схеме (которую и можно формализовать, но обычно лень) с оглядкой на семантику. В любом случае, часто кванторы считаются связывающими слабее, чем слабейшая из связок $\leftrightarrow$. Тогда $\forall x\varphi\rightarrow\exists x\varphi$ или действительно надо читать как $\forall x(\varphi\rightarrow(\exists x\varphi))$, или надо счесть такую запись некорректной, а вместо неё должна быть $\forall x\varphi\rightarrow(\exists x\varphi)$.

[epros]

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

А смысл не меняется, если поставить эти скобки. Формула $(\exists x \forall y~\psi[y|x]) \leftrightarrow x=y$ эквивалентна вашей $\exists x \forall y~\psi[y|x] \leftrightarrow x=y$.

Я полагаю более "общепринятым" правило, согласно которому любая логическая связка имеет приоритет выше кванторов. По-моему, с точки зрения "экономии скобок" это самое правильное соглашение. А вот в $\forall x \varphi \rightarrow (\exists x \varphi)$ или в $(\forall x \varphi) \rightarrow (\exists x \varphi)$ я бы скобки как раз расставил. Хотя $\forall x (\varphi \rightarrow \exists x \varphi)$ тоже понятно. Но только не $\forall x \varphi \rightarrow \exists x \varphi$.

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

Ваша теория им не удовлетворяет — ну что ж, она и не видится неформально «конструктивной» — два объекта, о которых она говорит, никак нельзя маркировать, они взаимозаменяемы.

Мне видится так, что если теория не определяет ни одной константы или не определяет равенства, но при этом использует квантор существования, то конструктивной она быть не может. В частности, в этом примере теории с двумя "взаимозаменяемыми" объектами, если мы попытаемся сказать "возьмём один из объектов", то правильный конструктивист должен спросить: "Какой именно"? И на этот вопрос невозможно будет дать ответа.

[arseniiv]

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