2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3, 4, 5, 6, 7  След.
 
 Re: Формализация математических текстов
Сообщение27.08.2020, 21:31 


21/05/16
4292
Аделаида
Alexandr Gavrichenko в сообщении #1481024 писал(а):
Дело в том, что в тексте фиксированное кольцо встречается в разных контекстах: иногда "для любого кольца R", иногда "существует кольцо R".

Ну так меняйте квантор в утверждении.
Alexandr Gavrichenko в сообщении #1481024 писал(а):
По Вашему
Commutativerings для коммутативных колец,
Commutativegroups для абелевых групп.

Вы можете сократить хоть до crng и cgrp.
Alexandr Gavrichenko в сообщении #1481024 писал(а):
COM.RNG и COM.GRP более кратко и (пока ещё) прозрачно для восприятия.

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение27.08.2020, 22:02 


01/08/20
67
kotenok gav в сообщении #1481027 писал(а):
формально неправильно.

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

kotenok gav в сообщении #1481027 писал(а):
Ну так меняйте квантор в утверждении.

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение27.08.2020, 23:07 


21/05/16
4292
Аделаида
Alexandr Gavrichenko в сообщении #1481029 писал(а):
А отметив однократно в списке обозначений "R - кольцо", можно воспользоваться краткой записью $\forall R$ и $\exists R$.

Это тоже неправильно с формальной точки зрения.
Alexandr Gavrichenko в сообщении #1481029 писал(а):
Почему? Подробнее, пожалуйста.

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение28.08.2020, 07:14 


26/12/18
155
Alexandr Gavrichenko в сообщении #1480762 писал(а):
Sycamore в сообщении #1480757 писал(а):
серьёзными ошибками при интуитивной/содержательной интерпретации чужих мышлению формальных текстов.
Остаётся возможность, что эта интерпретация будет не ошибочной, а альтернативной.
интерпретация нами заведомо корректного формализма должна быть строго единственной и потому будет или правильной, или ошибочной, то бишь вводящей в заблуждение по части математической истины; если надеемся, что компьютер найдёт некоторые новые теоремы и мы узнаем о них читая (с большим, мучительным трудом) формальную абракадабру на выходе компа, то это гиблое дело: подавляющее большинство формальных выкладок будет тривиальным и неинтересным, только машинно-обученному (deep learning) искуственному интеллекту в принципе может удасться набрести на и решить действительно важные задачи, но вряд ли кто-то станет заниматься таким статистическим по существу обучением компов даже ограниченным разделам математики - успех такого начинания никак не гарантирован и вряд ли стоит усилий. Другими словами, чтение и интерпретация формальных дедуктивных выводов не стоят свеч за исключением машинной верификации/проверки особо громоздких и запутанных результатов.

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение28.08.2020, 09:31 


01/08/20
67
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 писал(а):
формализовать можно всё, что угодно

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение28.08.2020, 12:29 


21/05/16
4292
Аделаида
:facepalm:
С вами бесполезно разговаривать. Отвечаю в последний раз.
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))$

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение28.08.2020, 14:05 


01/08/20
67
kotenok gav в сообщении #1481092 писал(а):
Формально, всегда должно быть указано множество.

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

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

kotenok gav в сообщении #1481092 писал(а):
И что же тогда значит "простота"?

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

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

 Профиль  
                  
 
 Posted automatically
Сообщение28.08.2020, 14:45 
Заслуженный участник


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

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

 Профиль  
                  
 
 Posted automatically
Сообщение28.08.2020, 21:29 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение28.08.2020, 22:50 


26/12/18
155
Alexandr Gavrichenko в сообщении #1481076 писал(а):
Всё, что угодно, мне формализовать не удалось.
к примеру, чего не удалось?

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение29.08.2020, 07:41 


01/08/20
67
Sycamore в сообщении #1481210 писал(а):
к примеру, чего не удалось?

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение29.08.2020, 09:43 


01/08/20
67
Alexandr Gavrichenko в сообщении #1481116 писал(а):
Можно условиться буквой $x$ всегда (внутри данного текста) обозначать действительное число.

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

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение29.08.2020, 18:09 


26/12/18
155
Alexandr Gavrichenko в сообщении #1481220 писал(а):
Уже феноменологию физических явлений и идейные соображения в математике мне не удаётся формализовать.
какое идейное соображение не удалось?

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение30.08.2020, 13:12 


01/08/20
67
Sycamore в сообщении #1481269 писал(а):
какое идейное соображение не удалось?

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

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

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

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

 Профиль  
                  
 
 Re: Формализация математических текстов
Сообщение30.08.2020, 14:12 


26/12/18
155
не нашёл особого смысла сверху :-)

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 101 ]  На страницу Пред.  1, 2, 3, 4, 5, 6, 7  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group