2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему На страницу 1, 2, 3  След.
 
 Что значит "предъявить объект" в смысле BHK?
Сообщение08.04.2018, 12:51 
Заслуженный участник
Аватара пользователя


28/09/06
10414
Согласно интерпретации Брауэра-Гейтинга-Колмогорова (сокращённо - 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)$ оказывается неразрешимым! Т.е. неизвестно, каким образом его можно "предъявить".

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение08.04.2018, 14:54 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение08.04.2018, 17:03 
Заслуженный участник
Аватара пользователя


28/09/06
10414
arseniiv в сообщении #1302567 писал(а):
Мне всегда казалось, что BHK (по крайней мере, сейчас) считается просто интуитивными неформальными соображениями
Да я не против. Просто мне казалось, что понять интуитивные неформальные соображения - это значит формализовать их. Или, если не получилось, то убедиться в том, что эти соображения - чушь.

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение08.04.2018, 17:16 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение08.04.2018, 22:14 
Заслуженный участник
Аватара пользователя


28/09/06
10414
Ну, как ещё? Готов рассмотреть вариант № 5 :roll:

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение08.04.2018, 23:58 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение09.04.2018, 03:34 


06/04/18

323
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$.

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение09.04.2018, 07:39 
Заслуженный участник


31/12/15
922
Номер 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$.

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение09.04.2018, 20:00 
Заслуженный участник
Аватара пользователя


28/09/06
10414
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.

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение10.04.2018, 00:21 


06/04/18

323
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)$.

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение10.04.2018, 01:14 
Заслуженный участник


27/04/09
28128
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. Ваша теория им не удовлетворяет — ну что ж, она и не видится неформально «конструктивной» — два объекта, о которых она говорит, никак нельзя маркировать, они взаимозаменяемы.

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение10.04.2018, 01:53 


06/04/18

323

(Оффтоп)

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

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение10.04.2018, 03:14 
Заслуженный участник


27/04/09
28128

(Оффтоп)

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

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение10.04.2018, 09:33 
Заслуженный участник
Аватара пользователя


28/09/06
10414
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 писал(а):
Ваша теория им не удовлетворяет — ну что ж, она и не видится неформально «конструктивной» — два объекта, о которых она говорит, никак нельзя маркировать, они взаимозаменяемы.
Мне видится так, что если теория не определяет ни одной константы или не определяет равенства, но при этом использует квантор существования, то конструктивной она быть не может. В частности, в этом примере теории с двумя "взаимозаменяемыми" объектами, если мы попытаемся сказать "возьмём один из объектов", то правильный конструктивист должен спросить: "Какой именно"? И на этот вопрос невозможно будет дать ответа.

 Профиль  
                  
 
 Re: Что значит "предъявить объект" в смысле BHK?
Сообщение10.04.2018, 16:25 
Заслуженный участник


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 42 ]  На страницу 1, 2, 3  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group