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

[kotenok gav]

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

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

Ну так меняйте квантор в утверждении.

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

По Вашему
Commutativerings для коммутативных колец,
Commutativegroups для абелевых групп.

Вы можете сократить хоть до crng и cgrp.

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

COM.RNG и COM.GRP более кратко и (пока ещё) прозрачно для восприятия.

Но зато это формально неправильно.

[Alexandr Gavrichenko]

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

формально неправильно.

Почему? Подробнее, пожалуйста.

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

Ну так меняйте квантор в утверждении.

И тогда получится, что надо много раз в тексте его повторять вместе с указанием $rings$. А отметив однократно в списке обозначений "$R$ - кольцо", можно воспользоваться краткой записью $\forall R$ и $\exists R$.

[kotenok gav]

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

А отметив однократно в списке обозначений "R - кольцо", можно воспользоваться краткой записью $\forall R$ и $\exists R$.

Это тоже неправильно с формальной точки зрения.

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

Почему? Подробнее, пожалуйста.

Потому что вы не определили (и не сможете определить) оператор "точка".

[Sycamore]

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

Sycamore в сообщении #1480757 писал(а):

серьёзными ошибками при интуитивной/содержательной интерпретации чужих мышлению формальных текстов.

Остаётся возможность, что эта интерпретация будет не ошибочной, а альтернативной.

интерпретация нами заведомо корректного формализма должна быть строго единственной и потому будет или правильной, или ошибочной, то бишь вводящей в заблуждение по части математической истины; если надеемся, что компьютер найдёт некоторые новые теоремы и мы узнаем о них читая (с большим, мучительным трудом) формальную абракадабру на выходе компа, то это гиблое дело: подавляющее большинство формальных выкладок будет тривиальным и неинтересным, только машинно-обученному (deep learning) искуственному интеллекту в принципе может удасться набрести на и решить действительно важные задачи, но вряд ли кто-то станет заниматься таким статистическим по существу обучением компов даже ограниченным разделам математики - успех такого начинания никак не гарантирован и вряд ли стоит усилий. Другими словами, чтение и интерпретация формальных дедуктивных выводов не стоят свеч за исключением машинной верификации/проверки особо громоздких и запутанных результатов.

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

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

это неверно, формализовать можно всё, что угодно, но ... толку будет мало даже если забыть про Гёделеву неполноту и отсутствие разрешающих алгоритмов для мало-мальски интересных проблем: формализму в большущем океане математики не сдобровать, увязнет в мелочах и утонет.

[Alexandr Gavrichenko]

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

Это тоже неправильно с формальной точки зрения.

Когда пишут $\forall x$ обычно подразумевают $\forall x \in \mathbb{R}$.
Запись $x $ в качестве неизвестного может быть воспринята компьютером (символьные вычисления). Это означает, что есть формальная система, которую понимает компьютер и в которой $x $ - действительное число. При этом указаний, что $x \in \mathbb{R}$ не потребуется.
Если условиться, что $R$ означает кольцо, то не потребуется записывать $R \in rings$, а формальное (в том числе компьютерное понимание сохранится).

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

Потому что вы не определили (и не сможете определить) оператор "точка"

В большинстве случаев $XXX.YYY \equiv \left\lbrace Z \mid z \in Z \Rightarrow (z \in YYY \wedge \mathcal{XXX}(z))\right\rbrace$

$\mathcal{XXX}(z) = \text { предикат, соответствующий аббревиатуре} \; XXX$


$\mathcal{COM}(z) = (\forall a, b \in z (ab = ba))$

В этой ситуации для различных понятий называемых "простыми" придётся вводить свой предикат (и, возможно, как Вы и хотели, вводить свой сокращающий символ). А возможно, при реализации на компьютере, сокращающий символ будет "перегружен": записываться будет одинаково, а компьютером восприниматься по разному. Так $a \cdot b$ означает умножение, но компьютер различает случаи умножения целых и действительных чисел, хотя знак $\cdot$ одинаков, но компьютер "догадывается" по контексту, как правильно этот знак $ \cdot $ трактовать. Таким образом, формальная запись понятная компьютеру является по существу неоднозначной.

Возможно, в конспектах встречается иное понимание оператора точка. Они записаны не на предельном уровне строгости, а так чтобы их мог воспринимать человек. Тогда при дорабатывании конспекта до строгой формальной системы эти случаи следует исправить в ущерб краткости. Конспекты задумывались не только как строгое, но и как краткое изложение.

Sycamore в сообщении #1481063 писал(а):

чтение и интерпретация формальных дедуктивных выводов не стоят свеч

Тем не менее кто-то этим занимается.

Sycamore в сообщении #1481063 писал(а):

формализовать можно всё, что угодно

Всё, что угодно, мне формализовать не удалось.

[kotenok gav]

С вами бесполезно разговаривать. Отвечаю в последний раз.

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

Когда пишут $\forall x$ обычно подразумевают $\forall x \in \mathbb{R}$.

И это неправильно. Формально, всегда должно быть указано множество.

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

$XXX.YYY \equiv \left\lbrace Z \mid z \in Z \Rightarrow (z \in YYY \wedge \mathcal{XXX}(z))\right\rbrace$

Ага, значит, простые идеалы они простые и идеалы. А простые числа просты и числа. И что же тогда значит "простота"?

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

$\mathcal{COM}(z) = (\forall a, b \in z (ab = ba))$

Замечательно. Коммутативные операции обрадовались.

[Alexandr Gavrichenko]

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

Формально, всегда должно быть указано множество.

Такая запись тоже недостаточна, Вы же не выписываете аксиоматическое определение множества $\mathbb{R}$, а отделываетесь одной буквой.
Это некоторая условность, к которой уже привыкли.

Можно условиться буквой $x$ всегда (внутри данного текста) обозначать действительное число.

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

И что же тогда значит "простота"?

Я же отметил, что для "простоты" возможно придётся вводить несколько предикатов. При этом можно оставить один сокращающий символ $PRM$, отвечающий одному из этих предикатов в зависимости от контекста: в $PRM.\mathbb{Z}$ или $PRM.IDL$ одинаковый сокращающий символ $PRM$, которому соответствуют разные предикаты. "Перегруженный" сокращающий символ.

$A \cdot B$ для матриц и $a \cdot b$ для чисел - это различные вещи. А обозначаются одинаково. Перегруженная операция. Компьютер умеет такие вещи распознавать по контексту, следовательно формальная строгость не нарушается.

[Pphantom]

Тема перемещена из форума «Дискуссионные темы (М)» в форум «Карантин»
Давайте все-таки приведем имеющиеся тексты к формально правильному виду. Пока в теме систематически неправильно набраны формулы и отдельные обозначения (краткие инструкции: «Краткий FAQ по тегу [math]» и видеоролик Как записывать формулы).

Исправьте все Ваши ошибки и сообщите об этом в теме Сообщение в карантине исправлено.
Настоятельно рекомендуется ознакомиться с темами Что такое карантин и что нужно делать, чтобы там оказаться и Правила научного форума.

[Pphantom]

Тема перемещена из форума «Карантин» в форум «Дискуссионные темы (М)»

[Sycamore]

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

Всё, что угодно, мне формализовать не удалось.

к примеру, чего не удалось?

[Alexandr Gavrichenko]

Sycamore в сообщении #1481210 писал(а):

к примеру, чего не удалось?

Уже феноменологию физических явлений и идейные соображения в математике мне не удаётся формализовать.

[Alexandr Gavrichenko]

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

Можно условиться буквой $x$ всегда (внутри данного текста) обозначать действительное число.

Пусть носитель интерпретации теории есть множество комплексных чисел.
Тогда оценки отображают переменную $x$ в некоторое комплексное число.
Рассмотрим подмножество оценок, отображающих переменную$х$ в некоторое действительное число.
Тогда работа с этим подмножеством эквивалентна требованию считать $x$ действительным числом.

См. Н. К. Верещагин, А. Шень "Языки и исчисления", гл. 3, пп. 3.1 - 3.2 (https://mccme.ru/free-books/shen/shen-logic-part2-2.pdf).

[Sycamore]

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

Уже феноменологию физических явлений и идейные соображения в математике мне не удаётся формализовать.

какое идейное соображение не удалось?

[Alexandr Gavrichenko]

Sycamore в сообщении #1481269 писал(а):

какое идейное соображение не удалось?

Ответил в ЛС, так как есть угроза уйти в оффтоп.

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

Рассмотрим подмножество оценок, отображающих переменную $х$ в некоторое действительное число.

Опечатка: Рассмотрим подмножество оценок, отображающих переменную $x$ в некоторое действительное число.

Другой подход: переменной $x$ присвоить другой сорт и определить область пробегания для этого сорта переменных как множество действительных чисел.

[Sycamore]

не нашёл особого смысла сверху