>Ок, A → ⊥ означает, что мы для любого типа можем построить функцию, которая виснет.
В общем случае не можем. Не из чего. А если бы могли, это бы сделало любые утверждения ложными.
>Отсюда получается, что (A → ⊥) → ⊥ было бы доказательством населённости типа A (A неопровержимо истинно)
Нет, и этот момент ключевой. Основное отличие от булевой логики в том, что --Р не означает Р. Неопровержимость не означает истинность. Если мы как-то получили доказательство --А, это еще не доказательство А, у нас по-прежнему нет док-ва населенности А.
>Вот тут вот одна заковыка - почему мы обязаны пользоваться переданной функцией.
Потому что больше у нас на руках ничего нет. У нас конструктор, и все детали, из которых мы что-то конструируем, мы должны задекларировать. Если мы для получения результата используем какую-то третью функцию-лемму, она должна быть пререквизитом: ее тип должен быть среди посылок (аргументов), наша функция-теорема должна получать на вход док-во используемой леммы.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2013-04-22 08:35 am (UTC)В общем случае не можем. Не из чего. А если бы могли, это бы сделало любые утверждения ложными.
>Отсюда получается, что (A → ⊥) → ⊥ было бы доказательством населённости типа A (A неопровержимо истинно)
Нет, и этот момент ключевой. Основное отличие от булевой логики в том, что --Р не означает Р. Неопровержимость не означает истинность. Если мы как-то получили доказательство --А, это еще не доказательство А, у нас по-прежнему нет док-ва населенности А.
>Вот тут вот одна заковыка - почему мы обязаны пользоваться переданной функцией.
Потому что больше у нас на руках ничего нет. У нас конструктор, и все детали, из которых мы что-то конструируем, мы должны задекларировать. Если мы для получения результата используем какую-то третью функцию-лемму, она должна быть пререквизитом: ее тип должен быть среди посылок (аргументов), наша функция-теорема должна получать на вход док-во используемой леммы.