![[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
хм. f x = f x не годится?
"А если бы могли, это бы сделало любые утверждения ложными."
А вот здесь по-подробнее. В классической логике мы можем подставить отрицание чего-нибудь. Чем тогда A → ⊥ не отрицание? Не "A - ложно", а часть выражения "если A ложно, ..." В частности, A неопровержимо, если всё, что может следовать из "если A ложно, ..." - это только абсурд.
"Потому что больше у нас на руках ничего нет."
Ну......а программы сначала тоже на руках ничего не имеют.
no subject
Это необузданная рекурсия, порождение сотоны. В нашей кошерной конструктивной логике и теории типов нет такой штуки. Благодаря чему возможно тотальное программирование, без таких вот засад. Мы можем гарантировать завершимость программ, если их типы кошерны, не ведут в ⊥.
>Чем тогда A → ⊥ не отрицание?
Это именно оно, это прямо-таки определение отрицания. Вот только инструменты в нашем конструкторе таковы, что фиг его зациклишь. Получить ⊥ можно только если его нам дали на вход или на входе есть функция, его производящая, и мы нашли, что ей скормить. Фактически, такие программы - как мысленные эксперименты, они говорят "вот если бы ты мне дал на вход такую штуку, то вот процедура, которая сделает из нее вот эту вот другую штуку". Но на практике добыть такой аргумент может быть неоткуда. В частности, функция ⊥ → ⊥ тривиальна, это id, но где взять конкретное значение типа ⊥, чтобы передать ей на вход? Построить мы эту функцию можем, это будет валидная конструкция, но вот запустить не сможем, нечего нам ей скормить.
no subject
ок, ⊥ → ⊥ населён, ибо есть id. Да, это означает, что не-абсурд - это истина.