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

.

Вот именно!

у вас триггер по ключевому слову, что ли

А статью прочту обязательно. Спасибо еще раз.

То, что в канве моих воззрений, то одобряю.

Да у меня тоже какое-то время было убеждение, что семантика не отличима от синтаксиса, потому что мы же описываем её с помощью (другого) синтаксиса. Но потом меня ткнули носом, что математическая структура существует независимо от её (синтаксического) описания. Которых — описаний — может вообще быть несколько эквивалентных (описывают-то они все одно и то же).

Но у некоторых нос настолько крепкий, что сколько не тыкай — до мозга не доходит. 🤷‍♀️

О! Спасибо, что разъяснили! А то мы-то думали, всё с точностью до наоборот, ведь никакие другие люди так не поступают.

***Но потом меня ткнули носом

Ну дык вас требовалось ткнуть носом, меня не требуется. )

я может чего-то не понимаю, но как синтаксическая модель языка влияет на типизацию?

HoTT где-то рядом

я могу сотней синтаксисов (диалектов) описать одно и то же на одном и том же япе, система типов, вывод и тд никак не поменяются

Меня просто вот этот товарищ нормально учил )
https://people.maths.ox.ac.uk/zilber/

Каким образом?

Нет, синтаксис-то сам по себе тоже может быть "математической структурой", объектом изучения и описания (синтаксического в том числе). Но не наоборот. 😊

Мы говорим "синтаксис" в смысле AST.

***Но потом меня ткнули носом, что математическая структура существует независимо от её (синтаксического) описания. Которых — описаний — может вообще быть несколько эквивалентных (описывают-то они все одно и то же).

Не знаю, кто вас тыкал носом, но его самого бы ткнуть носом куда-либо... ))
Дык вот, любое описание есть синтаксис.
Но инварианты они конечно есть.

Другой момент, что вы согласились с его аргументом... ну дело такое, это не ваша специальность.
Ну и кроме того, спроси большинство математиков, они тоже начнут ерунду городить по поводу синтаксиса и семантики.

ну почему же, возьмите факторизацию по отношению эквивалентности описаний и получились ваши математические структуры :D

другой вопрос, что это отношение, скорее всего, неразрешимо, ну да ладно

А там, после независимости математических структур следующим шагом маячит Платония и с ее пророком Тегмарком и его матем.вселенной, та еще бредятина. )