очевидность понятия "равно".

[ewert]

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

Судя по синтаксису это утверждение теории под названием "арифметика рациональных чисел".

Нет-нет, не рациональных, а целых. Я просто не знаю, потому и спросил. С моей точки зрения -- это утверждение самой теории. А как по-учёному будет: определение рационального числа как некоторой структуры на множестве целых -- описывается ли формально средствами самой теории или надобно привлекать метатеорию?

[epros]

ewert в сообщении #228667 писал(а):

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

Судя по синтаксису это утверждение теории под названием "арифметика рациональных чисел".

Нет-нет, не рациональных, а целых.

Почему целых-то? В арифметике целых чисел дроби не определены .

ewert в сообщении #228667 писал(а):

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

"Самой теории" это какой? Если арифметики Пеано, то:
1. В её синтаксисе нет деления.
2. В ней можно доказать $\nexists x ~ x \cdot 3 = 2$, т.е. определить число 2/3 какой-либо формулой арифметики Пеано невозможно.

Но если "сама теория" - это арифметика рациональных чисел, то да, в ней числа определяются через пары натуральных чисел.

[ewert]

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

Почему целых-то? В арифметике целых чисел дроби не определены .

Очень даже определены как надстройка над этой арифметикой, причём определены средствами самой арифметики.

[epros]

ewert в сообщении #228679 писал(а):

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

Почему целых-то? В арифметике целых чисел дроби не определены .

Очень даже определены как надстройка над этой арифметикой, причём определены средствами самой арифметики.

Что Вы называете "надстройкой" над арифметикой и почему Вы уверены, что это не меняет арифметику?

[ewert]

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

Что Вы называете "надстройкой" над арифметикой и почему Вы уверены, что это не меняет арифметику?

Позвольте я сперва задам встречный вопрос. Определено ли в рамках самой арифметики понятие "делимость"?

[Инт]

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

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

При перечислении аксиом ZF логическая схема равенства обычно никак не упоминается, хотя неявно используется. Это я имел ввиду.

-- Вт июл 14, 2009 14:09:51 --

6675636b_new в сообщении #228563 писал(а):

Цитата:

Я спрашиваю о Критерии, по которому можно было бы строить достоверные суждения.

А критерии критериев и т.д. вам тоже подавай? Да поймите вы наконец, что теорий несколько (аксиомы у них РАЗНЫЕ), и ни одна из них достоверно не отражает действительность. Чего вы хотите? Создать теорию, которая достоверно отражает действительность? Так вот, такой не существует. То что нам людям кажется - это на самом деле не действительность, а лишь наши глюки. Вот у некоторых людей глюки совпадают и они придумывают аксиомы, но к действительности, это не имеет никакого отношения - нам просто КАЖЕТСЯ и не более.

Интересно, как Вы знаете о том, что нечто Вам кажется? И естественно, только Вы знаете, что есть реальность.

[MGM]

ewert в сообщении #228683 писал(а):

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

Что Вы называете "надстройкой" над арифметикой и почему Вы уверены, что это не меняет арифметику?

Позвольте я сперва задам встречный вопрос. Определено ли в рамках самой арифметики понятие "делимость"?

Во-во. Это уже ближе к натуральному моделированию.
А то всё пытаются арифметику строить под обратные элементы.
А простую сущность деления яблока на части забывать стали.

[AGu]

Всюду ниже я предполагаю, что в качестве метатеории рассматривается теория множеств $\mathcal T$ в какой-либо из ее классических версий (так называемая «наивная теория множеств») и для удобства (исключительно для удобства, или, если угодно, для уменьшения траффика ) фиксируется гипотетическая метамодель $\mathcal M$ этой метатеории, в которой и происходит вся дальнейшая возня (хотя на самом деле всю возню можно производить в самой метатеории $\mathcal T$). В рамках этой возни возникают, в том числе, разного рода теории. Каждая теория $T$ представляет собой некоторое множество формул, называемых также аксиомами теории $T$. В свою очередь, формула -- это элемент языка $L_T:=L(\Sigma_T)$ теории $T$, порождаемого (вполне конкретной, могу выписать) контекстно свободной грамматикой из атомарных формул, соответствующих сигнатуре $\Sigma_T$ теории $T$.

Например, (аддитивный) язык $L_G$ теории групп $G$ имеет сигнатуру $\Sigma_G=\{\text{\tt=},+\}$. (Обратите внимание на различие начертаний метаравенства $=$ и символа равенства $\text{\tt=}$. Кстати, символ равенства не всегда включают в сигнатуру, но это дело вкуса, пусть включается.) Этот язык $L_G$ порождается атомарными формулами вида $s\ \text{\tt=}\ t$, где $s$ и $t$ -- термы. Термы же порождаются атомарными термами $x$ и $x+y$, где $x$ и $y$ -- переменные. Переменные же порождаются... (тут я, пожалуй, продолжу, только если меня попросят ). Сама же теория $G$ является объединением теории предикатов первого порядка с равенством и множества формул вида $(x+y)+z\ \text{\tt=}\ x+(y+z)$ и т.д. (специальные аксиомы группы, надеюсь, известны).

На данном этапе я, кажется, ответил на вопрос luitzen:

luitzen в сообщении #228655 писал(а):

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

Возьмем, к примеру, теорию групп (с операцией сложения), определенную в метатеории множеств.

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

Из схематично описанного выше подхода видно, как теория групп $G$ определяется в рамках метатеории множеств $\mathcal T$. И это, насколько мне известно, классический подход. (В качестве ссылки на литературу я могу лукаво предложить любую монографию по теории групп, но здесь уместнее будет сослаться на любой традиционный курс классической логики. )

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

Интересно вообще понять, что означает словосочетание "определяется в теории".

Стремясь к точности, я должен был сказать «определяется в языке теории», а не «определяется в теории». (Вероятно, этой моей оговоркой и был вызван вопрос epros.) На самом деле определение -- это, разумеется, элемент метамодели, а вовсе не что-то там внутри теории. Итак, что же такое «определение»? Веселый вопрос. Я могу предложить следующее метаопределение понятия «определение».

Определением называется эффективное (в смысле теории алгоритмов) расширение $E\supset L_T$ языка $L_T$ рассматриваемой теории $T$, снабженное алгоритмом $A$ перевода формул с расширенного языка $E$ на исходный язык $L_T$.

Разумеется, в указанном смысле «определение» как пара $(E,A)$ является элементом метамодели $\mathcal M$. На практике расширение $E$ обычно задается расширением контекстно свободной грамматики языка $L_T$ за счет добавления конечного множества новых символов и конечного множества продукций, а алгоритм $A$ определяется семантическими правилами, так или иначе связанными с добавленными продукциями (но это, наверное, уже лишние детали).

Приведу пример (опуская техническую кутерьму). Допустим, в языке $L_{\rm ZFC}$ теории множеств ZFC мы хотим определить отношение включения $s\subseteq t$. С этой целью мы расширяем язык новыми атомарными формулами вида $s\subseteq t$ (тем самым автоматически расширяя язык формул $L_{\rm ZFC}$ до нового расширенного языка $E$) и определяем алгоритм $A$ перевода с $E$ на $L_{\rm ZFC}$ семантическим правилом $(s\subseteq t):=(\forall\, x)(x\in s\Rightarrow x\in t)$, т.е., грубо говоря, указываем, что всякое вхождение формулы вида $s\subseteq t$ при переводе следует заменить соответствующей формулой $(\forall\, x)(x\in s\Rightarrow x\in t)$.

epros писал(а):

Например, определяется ли операция сложения в арифметике (если в ней предусмотрен символ "+" и соответствующие аксиомы)? По-моему, можно сказать, что операция сложения определяется в арифметике. Хотя, конечно, и символ "+", и соответствующие аксиомы указаны как относящиеся к "арифметике" именно метатеорией.

Стало быть, в моем понимании сложение в арифметике (точнее, в языке арифметики) не определяется -- в том смысле, что оно не вводится с помощью определения: термы $s+t$ уже входят в исходный язык арифметики, и для их использования расширение языка не требуется.

Надеюсь, я достаточно подробно разъяснил свои туманные намеки. (Впрочем, готов разъяснить подробнее, если потребуется.)

[epros]

ewert в сообщении #228683 писал(а):

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

Что Вы называете "надстройкой" над арифметикой и почему Вы уверены, что это не меняет арифметику?

Позвольте я сперва задам встречный вопрос. Определено ли в рамках самой арифметики понятие "делимость"?

Имеется в виду целочисленная делимость? Конечно же формула для этого может быть записана:
$\exists x ~ a \times x = b$ читается как: "$b$ делится на $a$".

[ewert]

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

Имеется в виду целочисленная делимость? Конечно же формула для этого может быть записана:
$\exists x ~ a \times x = b$ читается как: "$b$ делится на $a$".

Но тогда и рациональные числа вполне могут быть определены внутри целочисленной арифметики как результат факторизации множества $\mathbb Z\times\mathbb N$ по соответствующему отношению эквивалентности. Разве нет? Чем это хуже?...

[AGu]

Инт в сообщении #228707 писал(а):

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

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

При перечислении аксиом ZF логическая схема равенства обычно никак не упоминается, хотя неявно используется. Это я имел ввиду.

Понял, успокоился. Спасибо.

[epros]

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

Определением называется эффективное (в смысле теории алгоритмов) расширение $E\supset L_T$ языка $L_T$ рассматриваемой теории $T$, снабженное алгоритмом $A$ перевода формул с расширенного языка $E$ на исходный язык $L_T$.

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

Стало быть, в моем понимании сложение в арифметике (точнее, в языке арифметики) не определяется -- в том смысле, что оно не вводится с помощью определения: термы $s+t$ уже входят в исходный язык арифметики, и для их использования расширение языка не требуется.

Понятно. Стало быть определением Вы считаете то, чего в теории изначально нет, но что может быть добавлено. А я называю определением то, что уже добавлено.

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

-- Вт июл 14, 2009 14:56:22 --

Инт в сообщении #228707 писал(а):

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

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

При перечислении аксиом ZF логическая схема равенства обычно никак не упоминается, хотя неявно используется. Это я имел ввиду.

Очевидно, что AGu имел в виду не то, что схема равенства "неявно используется", а то, что она выводима в ZF, хотя и не заложена непосредственно в аксиомы.

-- Вт июл 14, 2009 14:59:34 --

ewert в сообщении #228718 писал(а):

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

Имеется в виду целочисленная делимость? Конечно же формула для этого может быть записана:
$\exists x ~ a \times x = b$ читается как: "$b$ делится на $a$".

Но тогда и рациональные числа вполне могут быть определены внутри целочисленной арифметики как результат факторизации множества $\mathbb Z\times\mathbb N$ по соответствующему отношению эквивалентности. Разве нет? Чем это хуже?...

Какого "множества"? Откуда у Вас вообще всплыла теория множеств, если речь была о целочисленной арифметике - куда более бедной теории?

[luitzen]

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

[…]
На данном этапе я, кажется, ответил на вопрос luitzen:

luitzen в сообщении #228655 писал(а):

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

Возьмем, к примеру, теорию групп (с операцией сложения), определенную в метатеории множеств.

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

Из схематично описанного выше подхода видно, как теория групп $G$ определяется в рамках метатеории множеств $\mathcal T$. И это, насколько мне известно, классический подход. (В качестве ссылки на литературу я могу лукаво предложить любую монографию по теории групп, но здесь уместнее будет сослаться на любой традиционный курс классической логики. )

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

Интересно вообще понять, что означает словосочетание "определяется в теории".

Стремясь к точности, я должен был сказать «определяется в языке теории», а не «определяется в теории». (Вероятно, этой моей оговоркой и был вызван вопрос epros.)

AGu, пруфлинк с точностью до страницы, и я от Вас отстану. Кажется, моя претензия в чём-то сродни той, которую Вы увидели у epros.

[AGu]

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

Стало быть определением Вы считаете то, чего в теории изначально нет, но что может быть добавлено. А я называю определением то, что уже добавлено.

Если Вы приведете свою версию определения понятия «определимость в теории», то я, возможно, просеку Вашу позицию. Пока же мне приходится лишь гадать. Что ж, попробую.

epros писал(а):

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

Итак, пытаюсь гадать... Здесь, видимо, идет речь совсем о другой определимости -- не в теории, а в модели -- стандартной модели $\mathbb N$ арифметики. В этой модели есть стандартное сложение и оно неопределимо (в некотором строгом смысле) в терминах упомянутой бедной сигнатуры [Лангфорд].

epros писал(а):

Отсюда вопрос: для какой теории тогда определяется сложение?

Видимо, все же не в теории, а в модели? Ну а если в модели, то, например, в $(\mathbb N, (\cdot)',{|})$, т.е. в модели натуральных чисел с инкрементом и делимостью [Робинсон]. Может, и еще где-нибудь. Но это все мимо, это определимость в моделях. (Мы же до сих пор про теории говорили.) Если же я промазал со своими догадками, и Вам известно более адекватное определение определимости в теории, то, пожалуйста, поделитесь.

epros писал(а):

Инт в сообщении #228707 писал(а):

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

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

При перечислении аксиом ZF логическая схема равенства обычно никак не упоминается, хотя неявно используется. Это я имел ввиду.

Очевидно, что AGu имел в виду не то, что схема равенства "неявно используется", а то, что она выводима в ZF, хотя и не заложена непосредственно в аксиомы.

Спасибо за лестный телепатический сеанс , но тут я действительно впадал в тупую непонятку -- включать аксиомы равенства в ZF, или не включать. Теперь -- мое телепатическое алаверды. Подозреваю, что epros намекает на следующее: все аксиомы равенства доказуемы из одних лишь специальных аксиом ZF. Честно признаюсь, я не знаю, так ли это. Во всяком случае, мне с наскока не удается доказать аксиому $x\in y\land x=z\Rightarrow z\in y$. (А все остальные -- удается, причем вообще без специальных аксиом. ) Я даже собрался было применить какую-нибудь ординальную кумулятивную иерархию, но потому вдруг подумал: а откуда мне знать, не разрушится ли она без (еще не доказанных) аксиом равенства. Короче, продолжаю тупить.

luitzen в сообщении #228732 писал(а):

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

Из схематично описанного выше подхода видно, как теория групп $G$ определяется в рамках метатеории множеств $\mathcal T$. И это, насколько мне известно, классический подход. (В качестве ссылки на литературу я могу лукаво предложить любую монографию по теории групп, но здесь уместнее будет сослаться на любой традиционный курс классической логики. )

AGu, пруфлинк с точностью до страницы, и я от Вас отстану.

Обижать изволите? Вам мало моей демонстрации того, что теорию групп (как, кстати, и массу других теорий) можно определить в рамках теории множеств (как метатеории), и требуете ссылку на больший авторитет, чем ваш покорный? А вот не дам. Из вредности.

Не, ну серьезно: разве теория множеств -- не лучший кандидат на метатеорию, позволяющую говорить о множествах? А ведь теория (и теория групп в том числе) -- это множество формул. И формула -- это множество (точнее, последовательность) символов. И символы образуют множество -- алфавит. Это настолько естественно, что в учебниках об этом даже не пишут (разве что, в каких-нибудь махрово занудных или очень древних). Впрочем, интернет нам в помощь -- погуглите по "metatheory" в сочетании с "set theory" и, как и я, наверняка натолкнетесь на фразы типа «Metatheory: The totality of mathematical methods and means intended for the description and definition of some formal axiomatic theory [...]. This may be a complicated theory [...] (e.g. it may be set theory [...]).»

[luitzen]

AGu, я позволю себе восстановить Ваши купюры.

Цитата:

The totality of mathematical methods and means intended for the description and definition of some formal axiomatic theory, as well as for the investigation of its means.

Обратите внимание, что помимо «definition» там ещё какие-то слова произносятся. Собственно, я утверждаю, что они являются самыми важными. Одной только способности «определять» объекты предметной теории недостаточно.

Цитата:

Suppose that one is interested in some meaningful mathematical theory . This may be a complicated theory, the semantics of which is intuitively not sufficiently clear (e.g. it may be set theory, mathematical analysis, second-order arithmetic, etc.)

То «it», которое «may be set theory», относится не к метатеории, а к предметной теории. Приведите, пожалуйста, пример употребления, который не нужно допиливать многочисленными «[…]».