Если Вы приведете свою версию определения понятия «определимость в теории», то я, возможно, просеку Вашу позицию. Пока же мне приходится лишь гадать. Что ж, попробую.
...
Итак, пытаюсь гадать... Здесь, видимо, идет речь совсем о другой определимости -- не в теории, а в модели -- стандартной модели
арифметики.
Тоже попробую погадать.
Во-первых, я бы сказал не "определимость", а "определённость" (как состоявшийся факт).
Вот так поворотец! Выходит, мы говорили о совершенно разных понятиях.
epros писал(а):
Это то, что меня не устраивает в Вашем определении: оно говорит о возможности добавить понятие в язык, в котором его не было, а я хотел бы говорить о том понятии, которое в теории уже есть (например, о сложении в арифметике).
Не удивительно. От «определимости» (т.е. возможности выразить в заданных терминах) до «определенности» (т.е. в каком-то смысле «уникальности», «единственности») расстояньице еще то. (Впрочем, мне сейчас грех жаловаться: я сам недавно допустил довольно существенную оговорку подобного рода.
) OK, пусть будет «определенность».
epros писал(а):
Во-вторых, определённость понятия в модели меня не очень устраивает - именно зависимостью от модели. Но от этого легко избавится, начав определение с фразы: "Существует такая модель
теории
, что ...".
Поэтому можно сформулировать так:
Будем говорить, что бинарная операция
определена в теории
, если
Например, для арифметики такой моделью будет:
Ох, опять загадка. Вы о столь многом умолчали, что приведенное Вами определение можно счесть бессмысленным или осмысленным, тривиальным или глубоким, неадекватным или предельно точным в зависимости от силы телепатических способностей. Боюсь, что моих способностей тут маловато, но все же вновь попробую погадать.
(1) Коль скоро «я хотел бы говорить о том понятии, которое в теории уже есть», я делаю вывод, что операция
входит в сигнатуру
рассматриваемой теории
.
(2) Наблюдение (1) навевает грусть: получается, что определенным может быть лишь функциональный символ, вынесенный в сигнатуру. По-моему, это требование неадекватно ограничивает общность (даже несмотря на то, что предлагаемое определение можно распространить на случай предикатных символов). К слову, известное мне классическое определение представимости и определимости, связанное со стандартными моделями арифметики, такого ограничения не имеет.
(3) Наблюдая записи
,
и
, я заключаю, что строка
принадлежит
, т.е. является формулой сигнатуры
.
(4) Из принадлежности
следует, что
,
и
являются термами сигнатуры
.
(5) Из (4) следует, что модель
состоит не из абы чего, а именно из термов сигнатуры
.
(6) Наличие записи
наталкивает на мысль, что
,
и
-- не просто термы, а замкнутые термы, т.е. не содержат вхождения переменных.
(7) Из (5) и (6) следует, что
состоит из замкнутых термов сигнатуры
.
(8) Пустые модели традиционно не рассматриваются, а значит, сигнатура
обеспечивает наличие замкнутых термов.
(9) Из (8) следует, что
содержит хотя бы одну константу.
(10) Как и (1), заключение (9) позволяет усомниться в общности предлагаемого определения, поскольку сигнатуры массы традиционных теорий не содержат констант. К числу таковых относятся та же теория групп (в которую далеко не всегда включают константу нейтрального элемента), теория множеств (в которую вообще никогда не включают констант -- даже для пустого множества), теория упорядоченных множеств и многие другие. Получается, что к таким теориям понятие «определенности» неприменимо -- разве что в этом случае предполагается дополнительное введение каких-либо изначально отсутствующих констант (причем, способом, заведомо отличным от предлагаемого сейчас).
(11) Впрочем, как бы я ни грустил по поводу (2) и (10), я готов счесть эти ограничения специфическими для выбранного подхода и продолжить гадание.
(12) Из
вовсе не следует
, поскольку об интерпретации сигнатуры
в модели
ничего сказано не было. Например, на множестве
мы можем интерпретировать
и
так, что получится, например,
и
. Едва ли подобные вольности была задуманы, а если это так, то от нас опять-таки что-то скрыли. Видимо, было скрыто условие
. (Такую модель, наверное, можно назвать «синтаксической».)
(13) Если интерпретация равенства в
предполагается стандартной, то знак единственности в условии
избыточен. Но это мелочь.
(Синтаксическую модель
удовлетворяющую условию
предлагаю назвать «точной».)
Теперь -- замечание по существу. Предлагаемое определение мне не кажется адекватным. Более того, оно напрочь противоречит моему восприятию слов «определенность в теории». Делюсь своими сомнениями.
Рассмотрим теорию
с сигнатурой
и единственной специальной аксиомой
. Спрашивается, является ли операция сложения
определенной в теории
? По обсуждаемому сейчас определению -- да, является (синтаксическая модель
является точной). Но моя интуиция вопит: сложение в
не является определенным (уникальным, единственным)! Ну скажите на милость, -- уверяет меня моя интуиция, -- о какой определенности сложения может идти речь, если все, что мы знаем о сложении -- это то, что
? Да, замкнутых термов в рассматриваемой сигнатуре немного, всего-то
и т.п. И точных синтаксических моделей тоже мало (все они одноэлементны). Но разве это говорит в пользу определенности сложения «в теории»? Сложение будет единственным только в одноэлементных моделях теории
, а в любой другой -- нет. Т.е. мы имеем дело не с «определенностью в теории», а с «определенностью в точных моделях теории». По сути мы совсем недалеко ушли от определимости в стандартной модели и всего лишь заменили стандартную модель набором точных, причем по ходу дела ввели довольно сильные ограничения, изгнав из рассмотрения массу традиционных теорий и еще большую массу функций и отношений, об определимости/определенности которых можно было бы говорить.
Заранее прошу меня извинить, если что-то неверно угадал, но что взять с телепата-любителя?
epros писал(а):
epros писал(а):
Отсюда вопрос: для какой теории тогда определяется сложение?
Видимо, все же не в теории, а в модели? Ну а если в модели, то, например, в
, т.е. в модели натуральных чисел с инкрементом и делимостью [Робинсон].
Это, конечно, ответ, но он не подойдёт по одной простой причине: Определять сложение через делимость ничуть не лучше, чем просто заявить, что оно "неопределяемое понятие"
Этот ответ не подойдет по другой простой причине: я говорил об определимости, а Вы думали об определенности.
P.S. Надеюсь, моя лукавая наглость Вас не задела. Это все были игрушки-развлекушки. (Просто я был искренне удивлен возникшим перепрыгом с одного понятия к напрочь другому.
)
-- 2009.07.15 17:26 --я предпочитаю считать символы и строки базовыми (неопределяемыми) понятиями, а не пытаться определить их через множества.
Не поделитесь соответствующей метатеорией? Мне было бы любопытно взглянуть. (Не подумайте чего, я искренне интересуюсь.
)
epros писал(а):
Кстати, в этом плане под "моделью" я также предлагаю понимать не множество, а некий способ приписать каждому объекту теории уникальный строковый идентификатор.
Тоже было бы интересно увидеть, как этот «способ» формализуется в Вашей метатеории. (В случае метатеории множеств этот способ является функцией. Интересно, что это будет в Вашем случае.)
-- 2009.07.15 18:21 --AGu, никто не спорит, что теория множеств может использоваться в качестве метатеории для теории групп.
Хмм...
Возьмем, к примеру, теорию групп (с операцией сложения), определенную в метатеории множеств.
Ох, не кажется мне эта фраза достаточно аккуратной…
Если это не было сомнением в том, что теорию множеств можно использовать в качестве метатеории для теории групп, то что это было?
Выходит, «X можно определить в метатеории Y» еще не означает, что «Y можно использовать как метатеорию для X»? Т.е. использование в качестве средства для определения -- это не использование? Любопытная трактовка понятий.
(Мой легкомысленный наезд можно спокойно игнорировать. Это я так мстю.
)
luitzen писал(а):
Но не на тех основаниях, на которых Вам кажется. Метатеория — это то место, где что-то утверждается, а то и доказывается по поводу предметной теории.
С последним -- полностью согласен.
luitzen писал(а):
Если же с использованием языка теории просто формулируется другая теория, то первая теория не может быть названа метатеорией по отношению ко второй.
Осмелюсь заявить, что метатеория множеств позволяет «что-то утверждать и доказывать по поводу предметной теории» (теории групп в том числе). Например, она может утверждать/доказывать противоречивость/непротиворечивость, разрешимость/неразрешимость, полноту/неполноту, категоричность/некатегоричность и т.д./и т.п. этой теории, может сравнивать эту теорию с другими по силе, доказывать существование/отсутствие моделей данной теории, обладающих теми или иными свойствами, доказывать, что из данной теории что-то выводится или не выводится и вообще может делать практически все, что способно прийти в голову.
luitzen писал(а):
Формально, безусловно, теория множеств может выступать в качестве метатеории для теории групп. Но формулируемые в такой метатеории утверждения будут чаще всего тривиальны.
Тут я, пожалуй, отвечу Вашими словами: «Ох, не кажется мне эта фраза достаточно аккуратной…»
luitzen писал(а):
Я тоже усомнился в своей адекватности и отправил запрос одному товарищу. Вот какой был ответ:
Цитата:
По вопросу о метатеории: смотря что понимать под ТМ. Вспомни парадокс Сколема: множество не счетно в «объектной» ТМ, но счетно «фактически», т. е. с точки зрения метаязыка, который в свою очередь существенным образом привлекает теоретико-множественные понятия, т. е. основан на некоторой ТМ «второго уровня».
Если обращаться к ТГ, то очевидно, что это одна из теорий в первопорядковой логике. Наряду с ней могут быть построены другие теории, например первопорядковая ЗФ. Из того, что в этой ЗФ могут быть «эмулированы» некоторые или даже все структуры ТГ, конечно, не следует, что ЗФ является метатеорией для ТГ. С другой стороны, семантика первопорядковой логики, в которой строится ТГ, на сегодня насквозь пронизана теоретико-множественными понятиями, и от этой «метатеории множеств» ТГ естественно зависит. Так что вопрос «является ли ТМ метатеорией для ТГ» плохо поставлен. Он обретает смысл (и одновременно становится тривиальным) после того как уточняется, о какой именно ТМ идет речь.
AGu, с чем в приведённом пассаже Вы согласитесь, а с чем нет?
Со всем согласен. В том числе, с тем, что "вопрос «является ли ТМ метатеорией для ТГ» плохо поставлен." Подобных высказываний я никогда себе не позволял и говорил лишь о том, что теория множеств «может быть использована» (причем в очень сильном понимании слова «использована») в качестве метатеории для теории групп.
-- 2009.07.15 18:37 --И хочу заметить, что "аксиоматический" способ, о котором Вы говорите, этому не противоречит. На самом деле определение сложения в арифметике Пеано ("аксиоматическое") является ничем иным, как примитивно рекурсивным определением через заранее известную функцию инкремента
Хочу заметить, что все же не «аксиоматическое», а «семантическое» и не «в арифметике Пеано», а в «стандатной модели арифметики Пеано» (или, если угодно, «семантическое определение в точных синтаксических моделях арифметики Пеано»
).
И я это буду замечать до тех пор, пока меня в этом не переубедят (что, разумеется, вполне возможно при должном старании
).