Парадокс Жирара
Парадокс Жирара ("...this is equivalent to all logical propositions being provable, which makes the system inconsistent...") был обнаружен в первой версии теории типов Пера Мартина-Лёфа и был устранён им во второй с помощью иерархии типов.
Кайен Аугустссона, как и современный Хаскель, не содержат иерархии типов, в отличии от второй Агды.
Даже если Непейвода в своей (довольно слабой) книге про логику и наврал про вопрос "подчиняется ли бог законам логики?," такой вопрос весьма интересен, применительно к современному состоянию дел в этой самой логике.
PS
Религия здесь интересна через отсылку к Evangelion. Прочитанное мной описание Evangelion выглядело, как борьба за первенство (иерархия!) среди стремящихся быть Богом, и борьба эта осуществлялась детьми. Однако, посмотрите на вторую Агду. ;)
Кайен Аугустссона, как и современный Хаскель, не содержат иерархии типов, в отличии от второй Агды.
Даже если Непейвода в своей (довольно слабой) книге про логику и наврал про вопрос "подчиняется ли бог законам логики?," такой вопрос весьма интересен, применительно к современному состоянию дел в этой самой логике.
PS
Религия здесь интересна через отсылку к Evangelion. Прочитанное мной описание Evangelion выглядело, как борьба за первенство (иерархия!) среди стремящихся быть Богом, и борьба эта осуществлялась детьми. Однако, посмотрите на вторую Агду. ;)