Формализация математических текстов

[hurtsy]

Alexandr Gavrichenko в сообщении #1480762 писал(а):

Идеи передаются обычным (естественным) языком и никак не формализуются.

Никак не формализуется следует понимать, что идеи чем то защищены от формализации, типа комментариев в программировании Продемонстрируйте, пожалуйста если это возможно, на примере текста "Квантового анализа". Как действует формализация на доказательства?.

Хомский в Википедии писал(а):

Наиболее сложные — языки с фразовой структурой (сюда можно отнести естественные языки), далее — КЗ-языки, КС-языки и самые простые — регулярные языки.

Куда попадает Ваш "объект формализации"?

[Alexandr Gavrichenko]

hurtsy в сообщении #1480922 писал(а):

идеи чем то защищены от формализации

Нет, но при попытке ввести формализованный текст в компьютер это пришлось бы сделать. В конспектах часть высказываний на естественном языке взята в скобки.
Выше писали про то, что кроме теорем и доказательств математический текст содержит идеи, дающие читателю интуитивное понимание этих теорем.
Например, в тексте "Квантового анализа" упоминается "выбор шаров" (§7, Th. 4), а не расписываются формальные соотношения в произвольных конечных множествах. Соответствующий фрагмент текста оставлен на естественном языке. "Выбор шаров" - феноменологический образ, дающий понимание читателю.
Напротив, фраза "всякий простой идеал содержится в максимальном" (книга "Введение в теорию схем...") содержит лишь математические понятия и допускает формальную запись

$$\forall I \in PRM \quad \exists I' \in MAX \quad (I \subset I' \subset R)$$

.

Alexandr Gavrichenko в сообщении #1480949 писал(а):

Как действует формализация на доказательства?

Доказательства записываются преимущественно формально (см. конспекты).

hurtsy в сообщении #1480922 писал(а):

объект формализации

Не объект, а способ формализации. Вероятно, ближе всего к регулярным языкам.
Речь идёт о том, что теоремы и доказательства допускают регулярную запись, но на практике этой записью часто пренебрегают. Здесь сделана попытка формальную запись воссоздать.

[Alexandr Gavrichenko]

hurtsy в сообщении #1480922 писал(а):

Как действует формализация на доказательства?.

"Квантовый анализ", §7, теорема 7.1 - доказательство по существу формальное изложено в книге на естественном языке, а в конспекте (§7, Th. 3 - в нумерации конспекта) в виде формул.

[pogulyat_vyshel]

Праздная, бесполезная, бессодержательная деятельность. Никаких шансов скормить это математическому сообществу у вас нет. Даже у Бурбаков не прижилось. Развлекайтесь дальше.

-- 27.08.2020, 18:26 --

(Оффтоп)

Ну конечно. Он еще в "Космопоиска" состоит https://twitter.com/gavrichen

[Red_Herring]

Alexandr Gavrichenko
А почему бы Вам свои сообщения о формализации математических текстов не писать бы в формализованном виде? Мы бы увидели и прониклись (чем бы прониклись, вопрос другой)

[Alexandr Gavrichenko]

pogulyat_vyshel в сообщении #1480974 писал(а):

Никаких шансов скормить это математическому сообществу у вас нет.

Формулы эстетически привлекательны.

Red_Herring в сообщении #1480976 писал(а):

А почему бы Вам свои сообщения о формализации математических текстов не писать бы в формализованном виде?

Потому что сообщения о формализации не являются математическим текстом. Метаматематика.

[Red_Herring]

Alexandr Gavrichenko в сообщении #1480986 писал(а):

Потому что сообщения о формализации не являются математическим текстом. Метаматематика.

Т.е. метаматематику вы формализовать не можете, а вот на математику претендуете? А вот я ваше всообщение легко формализую:
BALDERDASH
И вот эта формула эстетически привлекательна

[Alexandr Gavrichenko]

Red_Herring в сообщении #1480994 писал(а):

метаматематику вы формализовать не можете

$$ (\text{всякий простой идеал содержится в максимальном}) = \forall I \in PRM \quad \exists I' \in MAX \quad (I \subset I' \subset R)$$

Red_Herring в сообщении #1480994 писал(а):

на математику претендуете?

$True$

$ \text {BALDERDASH} = (\text {True} \wedge \neg \text {True})$

$ (\text {Формализация} = \text {BALDERDASH}) = \; ?$

[Sycamore]

Alexandr Gavrichenko в сообщении #1480986 писал(а):

Red_Herring в сообщении #1480976 писал(а):

А почему бы Вам свои сообщения о формализации математических текстов не писать бы в формализованном виде?

Потому что сообщения о формализации не являются математическим текстом. Метаматематика.

ага, скажите это Гёделю

[kotenok gav]

Alexandr Gavrichenko в сообщении #1480996 писал(а):

"всякий простой идеал содержится в максимальном" = $\forall I \in PRM \; \exists I' \in MAX \; (I \subset I' \subset R)$

Неясно, что такое $PRM$ (мне очень не нравится ваша идея обозначать простые идеалы и простые числа одинаково), $MAX$, и $R$.

[Alexandr Gavrichenko]

kotenok gav в сообщении #1481009 писал(а):

что такое $PRM$

$I = \text {идеал (фиксированный)}$

$I' =\text {другой идеал} $

$R = \text {кольцо}$


$IDL = \text {идеалы (множество идеалов)}$

$IDL.R = IDL(R) = \text {множество идеалов кольца} \; R$

$RNG = \text {кольца}$

$PRM = \text {простые (объекты) } $

$MAX = \text { максимальные (объекты) }$

Запись $ ( I \in PRM.IDL(R) )$, означающая, что " $I$ - простой идеал кольца $R$ " избыточна, так как в силу условленного $I $ уже обозначает идеал.
Поэтому используется краткая запись $ ( I \in PRM )$, означающая " $I$ прост ".
То, что $I$ находится в кольце $R$ указано в этом фрагменте формулы: $(I \subset I' \subset R)$. Нет нужды повторять в остальных частях формулы.

kotenok gav в сообщении #1481009 писал(а):

мне очень не нравится ваша идея обозначать простые идеалы и простые числа одинаково

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

[kotenok gav]

Alexandr Gavrichenko в сообщении #1481010 писал(а):

так как в силу условленного I уже обозначает идеал.

Кем это было условленно? Никем.

Alexandr Gavrichenko в сообщении #1481010 писал(а):

Запись $ I \in PRM.IDL(R)$

Что значит точка?

Alexandr Gavrichenko в сообщении #1481010 писал(а):

Здесь я шёл от традиции естественного языка:

Зря.

[Alexandr Gavrichenko]

kotenok gav в сообщении #1481011 писал(а):

Кем это было условленно? Никем.

Мной. В стартовом сообщении темы этот пример указан (раздел "буквы"). Также это отмечено в моём конспекте книги Ю. И. Манина "Введение в теорию схем..."

kotenok gav в сообщении #1481011 писал(а):

Что значит точка?

Сужение класса до подкласса (множества до подмножества).
Из всех идеалов $ IDL$ выбираются простые идеалы $PRM.IDL$

kotenok gav в сообщении #1481011 писал(а):

Зря.

Можно использовать для простых чисел аббревиатуру $IRD$ - неприводимые, по аналогии с неприводимыми многочленами, неприводимыми топологическими пространствами.
Соотношение для простых идеалов

$$ab \in I \Rightarrow (a \in I \vee b \in I)$$

соответствует соотношению для неприводимых топологических пространств

$$(X = V_1\cup V_2) \wedge (V_1, V_2\in (closed\; sets))\Rightarrow (V_1 = X \vee V_2 = X)$$

.

[kotenok gav]

Alexandr Gavrichenko в сообщении #1481015 писал(а):

Мной.

А если бы вы просто сказали $\forall R\in rings$, предварительно определив $rings$ как множество колец?

Alexandr Gavrichenko в сообщении #1481015 писал(а):

Сужение класса до подкласса (множества до подмножества).
Из всех идеалов IDL выбираются простые идеалы PRM.IDL

Да просто назовите $primeideals(R)$ множество простых идеалов кольца $R$.

Alexandr Gavrichenko в сообщении #1481015 писал(а):

Соотношение для простых идеалов
$ab \in I \Rightarrow (a \in I \vee b \in I)$
соответствует соотношению для неприводимых топологических пространств
$(X = V_1\cup V_2) \wedge (V_1, V_2\in (closed\; sets))\Rightarrow (V_1 = X \vee V_2 = X)$.

Ничего не соответствует. и не надо

[Alexandr Gavrichenko]

kotenok gav в сообщении #1481021 писал(а):

А если бы вы просто сказали $\forall R\in rings$

Дело в том, что в тексте фиксированное кольцо встречается в разных контекстах: иногда "для любого кольца $R$", иногда "существует кольцо $R$". А в Вашем варианте уже навешен квантор всеобщности.

kotenok gav в сообщении #1481021 писал(а):

$primeideals(R)$ множество простых идеалов кольца $R$.

По Вашему
$Commutativerings$ для коммутативных колец,
$Commutativegroups$ для абелевых групп.
Длинновато получается. $COM.RNG$ и $COM.GRP$ более кратко и (пока ещё) прозрачно для восприятия.

kotenok gav в сообщении #1481021 писал(а):

Ничего не соответствует.

Здесь я с Вами не соглашусь, как и математическая традиция.