Да там диаграммы, состоящие из подобъектов представимых, из них мы строим следующий уровень... и везде надо проверять законы функторов и естественных преобразований. Надо что-то кешировать, но я еще недостаточно кеширую. Да и некогда.
Вот, вот, тут недавно оказалось, из ссылки в комментариях, что мы все стали понимать интуиционизм прагматично-современным образом (есть в классической математике алгебры открытых множеств топологических пространств и прочие алгебры Гейтинга, и с ними связана прелестная не вполне стандартная логика, а так ничего особенного, часть стандартной математики), а оказывается, основатель его имел в виду гораздо более радикальную интерпретацию: "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 01:46 am (UTC)no subject
Date: 2019-05-21 03:00 am (UTC)no subject
Date: 2019-05-21 05:02 am (UTC)no subject
Date: 2019-05-21 02:54 am (UTC)no subject
Date: 2019-05-21 03:00 am (UTC)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)Я все дохожу до мысли, что как только у нас появляется логика предикатов на домене, где переменные не совсем независимы, то логика уже бац - и не булева. Но надо это как-то доформализовать.
Время - частный случай такого домена.
no subject
Date: 2019-05-21 05:10 am (UTC)no subject
Date: 2019-05-21 04:28 pm (UTC)no subject
Date: 2019-05-21 05:52 am (UTC)no subject
Date: 2019-05-21 04:30 pm (UTC)no subject
Date: 2019-05-21 04:59 pm (UTC)no subject
Date: 2019-05-21 10:32 pm (UTC)http://www.cs.man.ac.uk/~david/categories/book/book.pdf
У них там код на ML, может быть интересно сравнить подходы, наверняка все иначе сделано.
...
no subject
Date: 2019-05-22 12:20 am (UTC)no subject
Date: 2020-05-17 06:56 pm (UTC)no subject
Date: 2020-05-17 09:26 pm (UTC)