![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
not not (to be or not to be)
В классической логике есть закон исключения третьего, гласящий, что для любого утверждения А справедливо A | -A, т.е. либо оно верно, либо ложно. Однако это очень смелое утверждение, его можно трактовать так, что любое утверждение разрешимо (decidable), что тоже довольно нагло, и вообще герр Гёдель хмурится. Интуиционисткая логика высказываний и с ней конструктивная математика и прочая теория типов ведут себя скромнее, и такого смелого утверждения не делают. Но зато в них доказуемо вот такое:
--(A | -A)
Давайте его докажем, используя тот же Идрис, хотя ровно так же док-во записывается на Хаскеле. Отрицание определено как импликация в абсурд, т.е. отрицание утверждения А это функция, которая из доказательства А производит абсурд (_|_). Тогда наше утверждение записывается так:
((А | (A -> _|_) -> _|_) -> _|_
В теории типов в синтаксисе Идриса оно становится типом функции:
M : ((Either A (A -> _|_)) -> _|_) -> _|_
А конструктивным его доказательством служит тело этой функции. На выходе она должна произвести абсурд, а на входе у нее тоже функция, такого вот типа:
f : (Either A (A -> _|_)) -> _|_
Нам нужно, используя ее одну, произвести _|_. На вход она принимает либо А, либо -А. Взять значение типа А нам неоткуда, значит нужна функция типа A -> _|_. Как ее построить? Сделать лямбду, которая принимает значение А, и скармливает его f, а она уже произведет _|_. Имея такую функцию типа A -> _|_, ее можно опять же скормить f, и тогда получить _|_ "из ничего". Выглядит это так:
Вот так, используя только переданную на вход f, скармливая ей использующую ее же функцию, можно произвести _|_ и так получить конструктивное доказательство --(A | -A). Что это значит? Что хоть мы в интуиционизме и конструктивизме и не утверждаем, что для всякого утверждения А верно (A | -A), мы однако со всей уверенностью его активно не_отрицаем. Дословно: считаем, что было бы абсурдным считать его ложным. Так и живем.
--(A | -A)
Давайте его докажем, используя тот же Идрис, хотя ровно так же док-во записывается на Хаскеле. Отрицание определено как импликация в абсурд, т.е. отрицание утверждения А это функция, которая из доказательства А производит абсурд (_|_). Тогда наше утверждение записывается так:
((А | (A -> _|_) -> _|_) -> _|_
В теории типов в синтаксисе Идриса оно становится типом функции:
M : ((Either A (A -> _|_)) -> _|_) -> _|_
А конструктивным его доказательством служит тело этой функции. На выходе она должна произвести абсурд, а на входе у нее тоже функция, такого вот типа:
f : (Either A (A -> _|_)) -> _|_
Нам нужно, используя ее одну, произвести _|_. На вход она принимает либо А, либо -А. Взять значение типа А нам неоткуда, значит нужна функция типа A -> _|_. Как ее построить? Сделать лямбду, которая принимает значение А, и скармливает его f, а она уже произведет _|_. Имея такую функцию типа A -> _|_, ее можно опять же скормить f, и тогда получить _|_ "из ничего". Выглядит это так:
M f = f (Right g) where
g a = f (Left a)Вот так, используя только переданную на вход f, скармливая ей использующую ее же функцию, можно произвести _|_ и так получить конструктивное доказательство --(A | -A). Что это значит? Что хоть мы в интуиционизме и конструктивизме и не утверждаем, что для всякого утверждения А верно (A | -A), мы однако со всей уверенностью его активно не_отрицаем. Дословно: считаем, что было бы абсурдным считать его ложным. Так и живем.
no subject
Я бы irrefutable переводил как "неопровержимость"
Про замену классических конструктивными понятно, хотя и не прочувствовал.
"Наконец, irrefutable оно, когда его отрицание ложно."
здесь "оно" относится к "истинно" или "ложно"? Или в смысле, что не важно, вычислимо ли, главное, что отрицание ложно?
no subject
Утверждение А неопровержимо, когда у нас есть терм-доказательство --А, т.е. док-во ложности отрицания А. Док-ва самого А у нас может не быть. Если оно есть, т.е. А одновременно истинно и неопровержимо, такое утверждение называется stable. Далеко не все увтерждения stable, например А | -A не stable. Зато все отрицательные утверждения stable: ---P == -P, ----P == --P.
Возвращаясь к посту: если бы у нас было доказательство forall A. A | -A, то это получилась бы программа, которая для любого А за конечное число шагов определяет, останавливается вычисление А или виснет (-А), выдавая из ничего конструктивное док-во или А, или -А. Т.е. это было бы решением halting problem, и даже круче - кроме ответа да или нет еще и обоснование давалось бы.
no subject
Тут нужно сообразить, как теория типов изгоняет дух Де Моргана.
И что умного именно в том, что (Either A (A → ⊥)) → ⊥. Ок, A → ⊥ означает, что мы для любого типа можем построить функцию, которая виснет.
Отсюда получается, что (A → ⊥) → ⊥ было бы доказательством населённости типа A (A неопровержимо истинно), но это только если мы строим функцию, пользуясь только переданной A → ⊥, т.е. можем построить одно значение A, которое вбросим в функцию, а не строим новую виснущую функцию для этого типа (мы же можем построить такую функцию для любого типа). Вот тут вот одна заковыка - почему мы обязаны пользоваться переданной функцией.
Хм, или откуда получается, что мы не можем построить виснущую функцию для ненаселённого типа: ⊥ → ⊥
no subject
В общем случае не можем. Не из чего. А если бы могли, это бы сделало любые утверждения ложными.
>Отсюда получается, что (A → ⊥) → ⊥ было бы доказательством населённости типа A (A неопровержимо истинно)
Нет, и этот момент ключевой. Основное отличие от булевой логики в том, что --Р не означает Р. Неопровержимость не означает истинность. Если мы как-то получили доказательство --А, это еще не доказательство А, у нас по-прежнему нет док-ва населенности А.
>Вот тут вот одна заковыка - почему мы обязаны пользоваться переданной функцией.
Потому что больше у нас на руках ничего нет. У нас конструктор, и все детали, из которых мы что-то конструируем, мы должны задекларировать. Если мы для получения результата используем какую-то третью функцию-лемму, она должна быть пререквизитом: ее тип должен быть среди посылок (аргументов), наша функция-теорема должна получать на вход док-во используемой леммы.
no subject
хм. f x = f x не годится?
"А если бы могли, это бы сделало любые утверждения ложными."
А вот здесь по-подробнее. В классической логике мы можем подставить отрицание чего-нибудь. Чем тогда A → ⊥ не отрицание? Не "A - ложно", а часть выражения "если A ложно, ..." В частности, A неопровержимо, если всё, что может следовать из "если A ложно, ..." - это только абсурд.
"Потому что больше у нас на руках ничего нет."
Ну......а программы сначала тоже на руках ничего не имеют.
no subject
Это необузданная рекурсия, порождение сотоны. В нашей кошерной конструктивной логике и теории типов нет такой штуки. Благодаря чему возможно тотальное программирование, без таких вот засад. Мы можем гарантировать завершимость программ, если их типы кошерны, не ведут в ⊥.
>Чем тогда A → ⊥ не отрицание?
Это именно оно, это прямо-таки определение отрицания. Вот только инструменты в нашем конструкторе таковы, что фиг его зациклишь. Получить ⊥ можно только если его нам дали на вход или на входе есть функция, его производящая, и мы нашли, что ей скормить. Фактически, такие программы - как мысленные эксперименты, они говорят "вот если бы ты мне дал на вход такую штуку, то вот процедура, которая сделает из нее вот эту вот другую штуку". Но на практике добыть такой аргумент может быть неоткуда. В частности, функция ⊥ → ⊥ тривиальна, это id, но где взять конкретное значение типа ⊥, чтобы передать ей на вход? Построить мы эту функцию можем, это будет валидная конструкция, но вот запустить не сможем, нечего нам ей скормить.
no subject
ок, ⊥ → ⊥ населён, ибо есть id. Да, это означает, что не-абсурд - это истина.