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  След.

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



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

Сейчас этот форум просматривают: Google [Bot]


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

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