![[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
Осмыслять этот код стоит с т.з. логики. В булевой логике любое утверждение либо истинно, либо ложно, его можно просто заменить одной из этих двух констант. В конструктивной логике жизнь разнообразней. Есть разница между true и irrefutable. Утверждение истинно, когда у меня есть его конструктивное доказательство в виде конкретного объекта, программы. Пока такое доказательство не получено, утверждение не истинно, но и не ложно, оно просто еще не решено. Ложно оно тогда, когда у меня опять же есть конкретная программа, которая из предполагаемого док-ва этого утверждения производит _|_, виснет. Ложные утверждения - это типы плохих, негодных, виснущих программ. Наконец, irrefutable оно, когда его отрицание ложно. Т.е. у нас нет конструктивного доказательства данного утверждения, мы не называем его истинным, но у нас есть конструктивное доказательство, что предположение о его ложности ведет к абсурду, т.е. его отрицание ложно. В посте как раз такое.
В принципе, есть определенная процедура, позволяющая конвертировать классические доказательства в конструктивные, но не один в один, а ценой замены для некоторых утверждений истинности на бесспорность (так по русски irrefutable?). Если конкретнее, в импликациях перед следствиями появляются двойные отрицания.
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. Да, это означает, что не-абсурд - это истина.
no subject
В виде чего угодно, главное, чтобы оно было конструктивным :)
А записывать его на русском языке, английском, языке классической логики + ZF, наивной теории множеств или каком-то языке программирования - дело вкуса конкретного математика, от этого совершенно ничего не изменится. Разница примерно та же, как писать ручкой или другой ручкой :)
no subject
no subject
Да кто же вам это сказал? :)
Вы путаете два совершенно разных понятия - идею, которая у математика в голове, и запись этой идеи. Вот идея (которая вне любых формальных систем, это то, как, и о чем математик рассуждает, собственно, это и есть математика, доказательство, сидящее в голове до того, как его переложили на бумагу), она может быть конструктивной или нет. А как записываете (в какой формальной системе) - это не важно. Конструктивная идея будет иметь конструктивный вид, на каком языке не напиши. И наоборот. Другое дело, что есть некоторые языки, в которых вы просто не сможете выразить неконструктивные идеи. Но какие-то конструктивные идеи вы на нем тоже выразить не сможете.
Напомню, что конструктивизм и интуитивизм вообще появились из-за отказа от формальных систем, убеждения математиков в их ненужности. Единственный критерий конструктивности - мнение математика. Если математик видит алгоритм в вашем доказательстве - оно конструктивное. Других критериев не придумали.
Что до A | -A - формально говоря, это утверждение вовсе нельзя сформулировать в рамках констурктивизма, т.к. тут не говорится ни о существовании объектов ни об их свойствах.
no subject
Один type-theorist у доски, семи пядей во лбу, из видео в соседнем посте. :)
no subject
Не надо только забывать, что и другие подходы тут тоже бывают (разным людям может нравиться разное :)), хотя бы исторически. Изначально никаких специальных формальных теорий для конструктивизма не было.