Да там диаграммы, состоящие из подобъектов представимых, из них мы строим следующий уровень... и везде надо проверять законы функторов и естественных преобразований. Надо что-то кешировать, но я еще недостаточно кеширую. Да и некогда.
Вот, вот, тут недавно оказалось, из ссылки в комментариях, что мы все стали понимать интуиционизм прагматично-современным образом (есть в классической математике алгебры открытых множеств топологических пространств и прочие алгебры Гейтинга, и с ними связана прелестная не вполне стандартная логика, а так ничего особенного, часть стандартной математики), а оказывается, основатель его имел в виду гораздо более радикальную интерпретацию: "The dependence of intuitionism on time is essential: statements can become provable in the course of time and therefore might become intuitionistically valid while not having been so before."
Я все дохожу до мысли, что как только у нас появляется логика предикатов на домене, где переменные не совсем независимы, то логика уже бац - и не булева. Но надо это как-то доформализовать.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2019-05-21 03:05 am (UTC)А как получается, что всю ночь? Какая-то автогенерация очень большого количества тестов? Или очень нетривиальные/длинные задачи?
no subject
Date: 2019-05-21 04:48 am (UTC)no subject
Date: 2019-05-21 05:04 am (UTC)no subject
Date: 2019-05-21 05:16 am (UTC)Так что, надо долго тестировать!
https://plato.stanford.edu/entries/intuitionism/
via
https://timelets.dreamwidth.org/1042186.html
no subject
Date: 2019-05-21 04:27 pm (UTC)Я все дохожу до мысли, что как только у нас появляется логика предикатов на домене, где переменные не совсем независимы, то логика уже бац - и не булева. Но надо это как-то доформализовать.
Время - частный случай такого домена.