О существовании единственного объекта и о формализации

[nikov]

Допустим, что в какой-то теории нам удалось доказать, что существует единственный объект, удовлетворяющий некоторому предикату. После этого иногда применяется такой прием: этому объекту дается имя, которое в дальнейшем используется в определениях, формулировках теорем и т.д.
Вопрос в следующем: если мы зададимся целью полностью формализовать эти рассуждения, то во что превратится имя этого объекта? Ведь оно не входит в список знаков этой формальной теории. В формализации, используемой Бурбаки, для этого служит специальный символ $\tau$. А какие есть способы помимо этого?

[rishelie]

можно заранее запастись счетным набором символов $x',x'',x''',\dots$ и забирать их по мере надобности. можно сам предикат использовать как обозначение. чтобы не путать, можно использовать подчеркнутый предикат просто так не делают, ибо это неудобочитаемо, но всегда имеется ввиду, что можно строго формализовать. впрочем, если пускаться во все тяжкие, то придется позаботиться об определении символа (графического или электронного), а тут можно залезть совсем уж в ненужные дебри

[AGu]

nikov в сообщении #232958 писал(а):

Допустим, что в какой-то теории нам удалось доказать, что существует единственный объект, удовлетворяющий некоторому предикату. После этого иногда применяется такой прием: этому объекту дается имя, которое в дальнейшем используется в определениях, формулировках теорем и т.д.
Вопрос в следующем: если мы зададимся целью полностью формализовать эти рассуждения, то во что превратится имя этого объекта? Ведь оно не входит в список знаков этой формальной теории. В формализации, используемой Бурбаки, для этого служит специальный символ $\tau$. А какие есть способы помимо этого?

Мне известны два способа.

(1) Пополняем сигнатуру новой константой, а аксиоматику -- соответствующей аксиомой.
(2) Определяем расширенный язык формул с новой константой и алгоритм перевода формул с расширенного языка на исходный.

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

[epros]

AGu в сообщении #233027 писал(а):

Мне известны два способа.

(1) Пополняем сигнатуру новой константой, а аксиоматику -- соответствующей аксиомой.

А как после этого убедиться, что мы получили не совершенно новую теорию?

AGu в сообщении #233027 писал(а):

(2) Определяем расширенный язык формул с новой константой и алгоритм перевода формул с расширенного языка на исходный.

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

[AGu]

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

AGu в сообщении #233027 писал(а):

Мне известны два способа.
(1) Пополняем сигнатуру новой константой, а аксиоматику -- соответствующей аксиомой.

А как после этого убедиться, что мы получили не совершенно новую теорию?

С помощью доказательства.

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

AGu в сообщении #233027 писал(а):

(2) Определяем расширенный язык формул с новой константой и алгоритм перевода формул с расширенного языка на исходный.

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

Есть.

[epros]

AGu в сообщении #237848 писал(а):

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

AGu в сообщении #233027 писал(а):

Мне известны два способа.
(1) Пополняем сигнатуру новой константой, а аксиоматику -- соответствующей аксиомой.

А как после этого убедиться, что мы получили не совершенно новую теорию?

С помощью доказательства.

Доказательство чего?
Наверное, сначала надо было бы определить, какая теория является "совершенно новой". Впрочем, с моей стороны это, пожалуй, излишнее буквоедство: кажется я догадываюсь каким должно быть такое определение.

AGu в сообщении #237848 писал(а):

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

AGu в сообщении #233027 писал(а):

(2) Определяем расширенный язык формул с новой константой и алгоритм перевода формул с расширенного языка на исходный.

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

Есть.

Ладно, верю.

[AGu]

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

Доказательство чего?
Наверное, сначала надо было бы определить, какая теория является "совершенно новой". Впрочем, с моей стороны это, пожалуй, излишнее буквоедство: кажется я догадываюсь каким должно быть такое определение.

Ответ на этот вопрос уже звучал:

AGu в сообщении #233027 писал(а):

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

Если что, см. Conservative extension.

[epros]

AGu в сообщении #238049 писал(а):

см. Conservative extension.

Я догадался, что Вы именно это посчитаете за теорию, которая не является "совершенно новой". Просто в плане буквоедства: Вас не смущает, что могут появиться новые теоремы, в формулировке которых присутствует новая константа? Это ведь не противоречит определению консервативного расширения: для него важно только то, чтобы не появились новые теоремы в старом языке. А требование, чтобы все такие новые теоремы "переводились" на старый язык, Вы не сформулировали...

[Профессор Снэйп]

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

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

Ну вот пусть $c$ --- новая константа. Как Вы переведёте теорему, утверждающую, что $c=c$, на старый язык?

[epros]

Профессор Снэйп в сообщении #238089 писал(а):

Ну вот пусть $c$ --- новая константа. Как Вы переведёте теорему, утверждающую, что $c=c$, на старый язык?

Я-то даже и не возьмусь никак переводить. Я просто вижу, что формально - это новая теорема и нет никакой процедуры проверки того, что это - на самом деле нечто из уже ранее известного. Вот если бы был какой-то механизм "перевода" формул нового языка на старый (заметьте, это не я первый предложил, а AGu в своём варианте № 2), тогда можно было бы убедиться в том, что мы имеем всего лишь "переведённую" на другой язык старую теорему.

Кстати, один из достаточно убедительных способов перевода - доказать, что $\varphi_{new} \leftrightarrow \varphi_{old}$, где $\varphi_{old}$ некое высказывание старого языка, а $\varphi_{new}$ - переводимая новая теорема. Но я сильно не уверен, что существование такового высказывания доказуемо для любой новой теоремы.

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

[AGu]

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

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

Похоже, что кто-то из нас кого-то из нас недопонимает. Возможно, это я себя недопонимаю, но, как мне казалось, вариант (2) предусматривает наличие алгоритма перевода по определению. Например, если $T\vdash(\exists!\,x)\,\varphi(x)$, то можно раширить язык теории $T$ новой константой $c$ и определить алгоритм перевода так, чтобы атомарные формулы $p(t_1,\dots,t_n)$ переводились в виде $(\exists\,x)\Bigl(\varphi(x)\ \&\ p\bigl(t_1|^c_x,\dots, t_n|^c_x\bigr)\Bigr)$, где $x$ — переменная, не входящая в термы $t_i$.

[epros]

AGu в сообщении #238160 писал(а):

как мне казалось, вариант (2) предусматривает наличие алгоритма перевода по определению

К варианту 2 нет вопросов. Речь была о том, что в варианте 1 про наличие алгоритма перевода формул ничего не было сказано. Поэтому непонятно, новые теоремы соответствуют чему-то старому или являются "существенно новыми".

[AGu]

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

К варианту 2 нет вопросов. Речь была о том, что в варианте 1 про наличие алгоритма перевода формул ничего не было сказано. Поэтому непонятно, новые теоремы соответствуют чему-то старому или являются "существенно новыми".

Теперь понял, спасибо.
Кстати, на мой взгляд, вариант (1) является «ленивой версией» варианта (2). По сути дела в (1) новая константа вводится исключительно как синтаксическое средство для упрощения (сокращения) выкладок. Определимость этой новой константы (по Бету), само собой, позволяет организовать «перевод», т.е. элиминацию этой константы, и тем самым считать формулы расширенной теории «сокращениями» формул исходной. Но это дело вкуса. И я согласен с тем, что Ваше замечание было сделано «в плане буквоедства» , так как никаких проблем тут, конечно же, нет.