Так всякие нестандартные модели примерно это же и делают, если смотреть только на синтаксическую часть.
В обычном нестандартном анализе надо четко отслеживать, какие утверждения формализуются в логике первого порядка, а какие - нет. Я не понимаю, как можно с этим жить. По-моему, на это уходит сил гораздо больше, чем даже постоянные проверки областей определения и критерия Лебега. А еще таскается вся эта теоретико-множественная "семантика" с ультрафильтрами (я говорю о семантике в том смысле, что под нестандартными действительными числами понимаются конкретные
понятно как построенные множества, пусть и неконструктивно). А еще напрягает, что
- поле.
Что касается Т.Тао и его
дешевой версии нестандартного анализа, то там все более-менее то же самое, просто вместо ультрафильтра берется обычный фильтр Фреше на
(который не ультрафильтр). Вроде конструктивнее, но все равно надо отслеживать, что в каком языке и как формулируется (и там какой-то прикол со связками отрицания и дизъюнкции - их вроде надо избегать и формулировать для них противоположные обратным теоремы). В общем тоже какая-то фигня с логикой. А мне хочется проще, чтобы без отслеживания всех этих формальных утверждений и связок. Пусть даже придется заплатить тем, что числа перестанут быть полем, или станут ограниченными или еще что-нибудь.
Как мне кажется, придумывали это не для упрощения обычной дифференциальной геометрии, а скорее для переноса результатов в интуиционистскую математику, в другие топосы (не
), ну и для пруфчекеров.
Вот, мне тоже так кажется. Мне наверное надо что-то не такое серьезное. Должны же быть какие-нибудь фриковатые, но строгие, версии матанализа, более урезанные по сравнению со стандартным, но зато проще на преобразования.
как нильпотент?
Я не знаю, как должен вести себя dx при перемножении на самого себя (но больше ставлю на то, что должен быть ноль, а не бесконечно малая более высокого порядка как в
). Т.е. скорее всего да, нильпотент.