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

[Alexandr Gavrichenko]

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

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

Выше утверждалось, что в формальной записи необходимо писать $\forall x \in \mathbb{R}$, а запись $\forall x$ не является достаточной.

Я показываю, что, напротив, если в начале текста указать, что "$x$ - действительное число" и уже в остальном тексте не писать про принадлежность $x$ множеству, то запись останется формально справедливой.

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

[bot]

(Оффтоп)

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

Объём текста уменьшается ориентировочно на 30%.

Всего то? Ну, тогда для шпаргалок не годится.

[hurtsy]

bot в сообщении #1482079 писал(а):

Всего то? Ну, тогда для шпаргалок не годится.

bot в сообщении #1479968 писал(а):

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

Практическая реализация предлагаемого способа в виде конспектов конкретных математических текстов в виде pdf-файлов доступна по следующим ссылкам:

Для шпаргалок годится - проверено на себе.

А для чего годится?

[fightingphysics]

Сомнительно что можно "изобрести" формальную систему одной лишь декларацией символов, без задания грамматики.

[bot]

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

А для чего годится?

Не знаю. Про шпаргалки вспомнил потому, что всегда их писал. Когда пишешь, лучше усваивается, особенно, если пишешь в переработанном, очень сжатом виде. Пользователей у моих шпор не было - мне было ни к чему, а другие в них не разбирались. Однажды на экзамене я попытался передать шпору бедствующему товарищу, её перехватили и ... отдали мне.
Зачем шпаргалку отдал? - спросил другой экзаменатор. А это не шпаргалка - это оглавление.

[Alexandr Gavrichenko]

fightingphysics в сообщении #1482470 писал(а):

"изобрести" формальную систему

Здесь нет новой формальной системы.
Здесь, скорее достраивается обычная запись до того состояния, что можно записывать формулы там, где обычно пишут текст.

fightingphysics в сообщении #1482470 писал(а):

одной лишь декларацией символов

"Декларация символов" позволяет встраивать такие понятия, как "идеалы данного кольца", "коммутативные кольца", в формулы, содержащие отношения принадлежности, подмножества.

[fightingphysics]

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

fightingphysics в сообщении #1482470 писал(а):

"изобрести" формальную систему

Здесь нет новой формальной системы.
Здесь, скорее достраивается обычная запись до того состояния, что можно записывать формулы там, где обычно пишут текст.

fightingphysics в сообщении #1482470 писал(а):

одной лишь декларацией символов

"Декларация символов" позволяет встраивать такие понятия, как "идеалы данного кольца", "коммутативные кольца", в формулы, содержащие отношения принадлежности, подмножества.

Математика это набор определенных специализированных языков, в такой язык нельзя просто так что то "встроить"

-- 08.09.2020, 18:56 --

Тем более "понятия".

-- 08.09.2020, 18:58 --

Вообще. ваша терминология страдает и хромает. Сам заголовок сформулирован как бессмыслица. Формализация относится не к "тексту", а к логической системе. Никакие "тексты" никто не "формализует".

[Someone]

Когда я только начинал читать лекции студентам, я пытался использовать хотя бы стандартную логическую символику для сокращения записи текста. Очень быстро обнаружил, что студенты перестали что-либо понимать. Больше я с этим не экспериментировал.

[fightingphysics]

Someone в сообщении #1482525 писал(а):

Когда я только начинал читать лекции студентам, я пытался использовать хотя бы стандартную логическую символику для сокращения записи текста. Очень быстро обнаружил, что студенты перестали что-либо понимать. Больше я с этим не экспериментировал.

А можно пример нестандартной символики?

[Alexandr Gavrichenko]

fightingphysics в сообщении #1482517 писал(а):

Математика это набор определенных специализированных языков

Да. Но книги и статьи пишут не на этих специализированных языках, а на естественных (русском, английском) и т. п.

fightingphysics в сообщении #1482517 писал(а):

Формализация относится не к "тексту", а к логической системе. Никакие "тексты" никто не "формализует".

Здесь идёт речь именно о формализации текста. Например, книги. В первом сообщении темы приведены конспекты математических текстов на основе книг по математике.

Someone в сообщении #1482525 писал(а):

студенты перестали что-либо понимать.

Возможно, что формальное представление будет полезно:
а) для профессиональных математиков,
б) для чтения компьютером.

(Оффтоп)

Можно рассмотреть ситуацию, когда студент не владеет ни русским, ни английским (а, скажем, китайским, хинди и французским). Тогда как ему объяснять?

mustitz в сообщении #1480701 писал(а):

Аналогично можно предложить писать все научные работы на эсперанто.

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

[fightingphysics]

А для "формализации" текстов поэта Некрасова Вы бы какие символы предложили?

[Someone]

fightingphysics в сообщении #1482527 писал(а):

А можно пример нестандартной символики?

А вот откройте, например, первое сообщение данной темы и посмотрите. Вообще, следуя путём, указанным нам топикстартером, очень легко сделать текст совершенно нечитаемым не только для студентов, но и для специалистов. Над собой, любимым, можете издеваться как хотите, но о других читателях надо позаботиться, чтобы чтение для них не превратилось в разгадывание шарад. Хватит с них обычных определений и обозначений.

[fightingphysics]

Кстати, формализация с символами даже не связана по сути. Можно и на естественном языке все писать, главное чтобы терминология была строгая и ограниченная. Эти символы играют роль компактности, а не формализации

-- 08.09.2020, 20:18 --

тут речь о чем то вроде графических символов для сокращений, вроде смайликов. Это не формализация

-- 08.09.2020, 20:21 --

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

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

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

Выше утверждалось, что в формальной записи необходимо писать $\forall x \in \mathbb{R}$, а запись $\forall x$ не является достаточной.

Я показываю, что, напротив, если в начале текста указать, что "$x$ - действительное число" и уже в остальном тексте не писать про принадлежность $x$ множеству, то запись останется формально справедливой.

Как раз формально не останется

-- 08.09.2020, 20:21 --

Не останется именно формально.

-- 08.09.2020, 20:24 --

А вот фактически она будет справедливой при любой записи, с единственным условием чтобы эта запись хотя бы понималась однозначно теми кто ее читает

-- 08.09.2020, 20:27 --

Формально корректной является та запись, которая допускается грамматикой того языка на котором она записана

-- 08.09.2020, 20:28 --

А вашем примере этого нет.

-- 08.09.2020, 20:37 --

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

-- 08.09.2020, 20:43 --

Это, видимо, мнение г-на Хомского

Лично я не вижу противоречия между строгостью и контекстозависимостью.

-- 08.09.2020, 20:45 --

Естественные языки нестроги не потому что они контекстозависимы, и контекстозависимость в разных естественных языках различна, это не влияет на их строгость

[Alexandr Gavrichenko]

Someone в сообщении #1482531 писал(а):

надо позаботиться, чтобы чтение для них не превратилось в разгадывание шарад.

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

fightingphysics в сообщении #1482532 писал(а):

Эти символы играют роль компактности

Да, компактности. А также точности.

fightingphysics в сообщении #1482532 писал(а):

Это не формализация

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

fightingphysics в сообщении #1482532 писал(а):

графических символов для сокращений

Повторюсь. Эти символы можно связывать отношениями принадлежности и подмножества.

fightingphysics в сообщении #1482532 писал(а):

Как раз формально не останется

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

fightingphysics в сообщении #1482532 писал(а):

Кстати тот случай который Вы описали похож на пример контекстозависимой грамматики.

Это скорее "полуфабрикат" регулярной. Но, может быть, "полуфабрикат регулярной" и есть КЗ-грамматика?

[Sycamore]

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

Это формализация в том смысле, что естественный язык замещается формулой... важней было показать принципиальную возможность краткой и строгой записи.

краткость ради одной самой краткости бессмысленна и никому не нужна, «Общую топологию» Келли читаешь как «Войну и мир» (формул прямо-таки не видно) и тем не менее русскому тексту строгости не занимать; непонятная башке с мозгом (краткая?) формализация нужна компу, дабы тот мог повторить и проверить логические выкладки, но нам та ни к чему, лишь увеличивает шанс ошибиться в толковании шарады и значит не будем уверены какую задачу на самом деле решал комп, хоть и заведомо/формально правильно.