not not (to be or not to be)
Apr. 18th, 2013 09:19 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonВ классической логике есть закон исключения третьего, гласящий, что для любого утверждения А справедливо 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), мы однако со всей уверенностью его активно не_отрицаем. Дословно: считаем, что было бы абсурдным считать его ложным. Так и живем.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2013-04-18 03:27 pm (UTC)В топосах это известное дело, что в топологии двойного отрицания логика становится булевой.
no subject
Date: 2013-04-18 03:56 pm (UTC)no subject
Date: 2013-04-18 04:02 pm (UTC)no subject
Date: 2013-04-18 06:14 pm (UTC)Ну и тогда, для верности конкретизируем
> :set -XImpredicativeTypes > type Bot = forall t. t > let {m :: (Either a (a -> Bot) -> Bot) -> Bot; m = \f -> f $ Right $ \a -> f (Left a)}no subject
Date: 2013-04-18 07:23 pm (UTC)no subject
Date: 2013-04-18 08:11 pm (UTC)no subject
Date: 2013-04-21 05:32 pm (UTC)но как-то не ясно, как строить функцию f. Точнее, если её построить как const ⊥, то не ясно, зачем городить M f.
no subject
Date: 2013-04-21 06:19 pm (UTC)Осмыслять этот код стоит с т.з. логики. В булевой логике любое утверждение либо истинно, либо ложно, его можно просто заменить одной из этих двух констант. В конструктивной логике жизнь разнообразней. Есть разница между true и irrefutable. Утверждение истинно, когда у меня есть его конструктивное доказательство в виде конкретного объекта, программы. Пока такое доказательство не получено, утверждение не истинно, но и не ложно, оно просто еще не решено. Ложно оно тогда, когда у меня опять же есть конкретная программа, которая из предполагаемого док-ва этого утверждения производит _|_, виснет. Ложные утверждения - это типы плохих, негодных, виснущих программ. Наконец, irrefutable оно, когда его отрицание ложно. Т.е. у нас нет конструктивного доказательства данного утверждения, мы не называем его истинным, но у нас есть конструктивное доказательство, что предположение о его ложности ведет к абсурду, т.е. его отрицание ложно. В посте как раз такое.
В принципе, есть определенная процедура, позволяющая конвертировать классические доказательства в конструктивные, но не один в один, а ценой замены для некоторых утверждений истинности на бесспорность (так по русски irrefutable?). Если конкретнее, в импликациях перед следствиями появляются двойные отрицания.
no subject
Date: 2013-04-21 09:15 pm (UTC)Я бы irrefutable переводил как "неопровержимость"
Про замену классических конструктивными понятно, хотя и не прочувствовал.
"Наконец, irrefutable оно, когда его отрицание ложно."
здесь "оно" относится к "истинно" или "ложно"? Или в смысле, что не важно, вычислимо ли, главное, что отрицание ложно?
no subject
Date: 2013-04-22 03:33 am (UTC)Утверждение А неопровержимо, когда у нас есть терм-доказательство --А, т.е. док-во ложности отрицания А. Док-ва самого А у нас может не быть. Если оно есть, т.е. А одновременно истинно и неопровержимо, такое утверждение называется stable. Далеко не все увтерждения stable, например А | -A не stable. Зато все отрицательные утверждения stable: ---P == -P, ----P == --P.
Возвращаясь к посту: если бы у нас было доказательство forall A. A | -A, то это получилась бы программа, которая для любого А за конечное число шагов определяет, останавливается вычисление А или виснет (-А), выдавая из ничего конструктивное док-во или А, или -А. Т.е. это было бы решением halting problem, и даже круче - кроме ответа да или нет еще и обоснование давалось бы.
no subject
Date: 2013-04-22 07:00 am (UTC)Тут нужно сообразить, как теория типов изгоняет дух Де Моргана.
И что умного именно в том, что (Either A (A → ⊥)) → ⊥. Ок, A → ⊥ означает, что мы для любого типа можем построить функцию, которая виснет.
Отсюда получается, что (A → ⊥) → ⊥ было бы доказательством населённости типа A (A неопровержимо истинно), но это только если мы строим функцию, пользуясь только переданной A → ⊥, т.е. можем построить одно значение A, которое вбросим в функцию, а не строим новую виснущую функцию для этого типа (мы же можем построить такую функцию для любого типа). Вот тут вот одна заковыка - почему мы обязаны пользоваться переданной функцией.
Хм, или откуда получается, что мы не можем построить виснущую функцию для ненаселённого типа: ⊥ → ⊥
no subject
Date: 2013-04-22 08:35 am (UTC)В общем случае не можем. Не из чего. А если бы могли, это бы сделало любые утверждения ложными.
>Отсюда получается, что (A → ⊥) → ⊥ было бы доказательством населённости типа A (A неопровержимо истинно)
Нет, и этот момент ключевой. Основное отличие от булевой логики в том, что --Р не означает Р. Неопровержимость не означает истинность. Если мы как-то получили доказательство --А, это еще не доказательство А, у нас по-прежнему нет док-ва населенности А.
>Вот тут вот одна заковыка - почему мы обязаны пользоваться переданной функцией.
Потому что больше у нас на руках ничего нет. У нас конструктор, и все детали, из которых мы что-то конструируем, мы должны задекларировать. Если мы для получения результата используем какую-то третью функцию-лемму, она должна быть пререквизитом: ее тип должен быть среди посылок (аргументов), наша функция-теорема должна получать на вход док-во используемой леммы.
no subject
Date: 2013-04-22 08:46 am (UTC)хм. f x = f x не годится?
"А если бы могли, это бы сделало любые утверждения ложными."
А вот здесь по-подробнее. В классической логике мы можем подставить отрицание чего-нибудь. Чем тогда A → ⊥ не отрицание? Не "A - ложно", а часть выражения "если A ложно, ..." В частности, A неопровержимо, если всё, что может следовать из "если A ложно, ..." - это только абсурд.
"Потому что больше у нас на руках ничего нет."
Ну......а программы сначала тоже на руках ничего не имеют.
no subject
Date: 2013-04-22 09:02 am (UTC)Это необузданная рекурсия, порождение сотоны. В нашей кошерной конструктивной логике и теории типов нет такой штуки. Благодаря чему возможно тотальное программирование, без таких вот засад. Мы можем гарантировать завершимость программ, если их типы кошерны, не ведут в ⊥.
>Чем тогда A → ⊥ не отрицание?
Это именно оно, это прямо-таки определение отрицания. Вот только инструменты в нашем конструкторе таковы, что фиг его зациклишь. Получить ⊥ можно только если его нам дали на вход или на входе есть функция, его производящая, и мы нашли, что ей скормить. Фактически, такие программы - как мысленные эксперименты, они говорят "вот если бы ты мне дал на вход такую штуку, то вот процедура, которая сделает из нее вот эту вот другую штуку". Но на практике добыть такой аргумент может быть неоткуда. В частности, функция ⊥ → ⊥ тривиальна, это id, но где взять конкретное значение типа ⊥, чтобы передать ей на вход? Построить мы эту функцию можем, это будет валидная конструкция, но вот запустить не сможем, нечего нам ей скормить.
no subject
Date: 2013-04-22 09:12 am (UTC)ок, ⊥ → ⊥ населён, ибо есть id. Да, это означает, что не-абсурд - это истина.
no subject
Date: 2013-04-23 07:46 am (UTC)В виде чего угодно, главное, чтобы оно было конструктивным :)
А записывать его на русском языке, английском, языке классической логики + ZF, наивной теории множеств или каком-то языке программирования - дело вкуса конкретного математика, от этого совершенно ничего не изменится. Разница примерно та же, как писать ручкой или другой ручкой :)
no subject
Date: 2013-04-23 07:58 am (UTC)no subject
Date: 2013-04-23 08:36 am (UTC)Да кто же вам это сказал? :)
Вы путаете два совершенно разных понятия - идею, которая у математика в голове, и запись этой идеи. Вот идея (которая вне любых формальных систем, это то, как, и о чем математик рассуждает, собственно, это и есть математика, доказательство, сидящее в голове до того, как его переложили на бумагу), она может быть конструктивной или нет. А как записываете (в какой формальной системе) - это не важно. Конструктивная идея будет иметь конструктивный вид, на каком языке не напиши. И наоборот. Другое дело, что есть некоторые языки, в которых вы просто не сможете выразить неконструктивные идеи. Но какие-то конструктивные идеи вы на нем тоже выразить не сможете.
Напомню, что конструктивизм и интуитивизм вообще появились из-за отказа от формальных систем, убеждения математиков в их ненужности. Единственный критерий конструктивности - мнение математика. Если математик видит алгоритм в вашем доказательстве - оно конструктивное. Других критериев не придумали.
Что до A | -A - формально говоря, это утверждение вовсе нельзя сформулировать в рамках констурктивизма, т.к. тут не говорится ни о существовании объектов ни об их свойствах.
no subject
Date: 2013-04-23 08:53 am (UTC)Один type-theorist у доски, семи пядей во лбу, из видео в соседнем посте. :)
no subject
Date: 2013-04-23 09:01 am (UTC)Не надо только забывать, что и другие подходы тут тоже бывают (разным людям может нравиться разное :)), хотя бы исторически. Изначально никаких специальных формальных теорий для конструктивизма не было.
no subject
Date: 2013-04-22 03:53 pm (UTC)∀ A B . (A → ⊥) → (A → B)
Т.е. когда A = ⊥, мы говорим о существовании стрелки из ⊥ во все объекты. Тогда если стрелок из других A в ⊥ нет, выходит, что ⊥ → (A → B), т.е. истинно (ибо есть стрелки из ⊥ во все объекты).
no subject
Date: 2013-04-22 04:48 pm (UTC)FalseElim : _|_ -> a
Аналогичная есть в Агде. Из абсурда следует все что угодно.
Последнюю вашу фразу не понял, что именно истинно, и в чем основная мысль.
no subject
Date: 2013-04-22 05:15 pm (UTC)последнее "истинно" относилось к тому, что когда стрелки A → ⊥ нет, то получаем множество таким стрелок не населено, и выражение сводится к ⊥ → (A → B). Это множество населено, т.к. есть стрелки из ⊥ во что угодно из рассуждений о A = ⊥. Тут забавно также, что доказывается существование стрелки из любого типа в любой другой. А маленькая находка в том, как правила импликации тоже выходят сами собой (из абсурда следует что угодно).
no subject
Date: 2013-04-22 05:41 pm (UTC)no subject
Date: 2013-04-22 06:16 pm (UTC)FalseElim гласит, что есть стрелка из ⊥ в любой тип. Так что, существует и стрелка из ⊥ в (A → B).
no subject
Date: 2013-04-22 06:35 pm (UTC)no subject
Date: 2013-04-22 08:13 pm (UTC)no subject
Date: 2013-04-23 05:02 am (UTC)no subject
Date: 2013-04-23 06:55 am (UTC)Я ещё как-то пытался соединять объекты оптоволокном :) по одному кабелю на стрелку, и по одному волокну в кабеле на каждую точку объекта домена - так тогда можно суръекции от инъекций отличать; например, можно визуализировать, что за эквалайзер такой и как это вообще квадраты коммутируют. "Включил свет" - посмотрел, где и какие точки засветились, да ещё каким цветом. :)
В категорном смысле есть ещё один занятный факт: для стрелок zA: 0 → A zB: 0 → B и двух стрелок f, g: A → B верно следующее: f . zA = g . zA = zB Так вот, здесь аналогии с трубами и кабелями заканчиваются :)
no subject
Date: 2013-04-23 07:39 am (UTC)В ситуации с композицией, имхо, аналогия еще держится: закон композиции говорит, что если у нас два таких кабеля, один идет из 0 в А, второй из А в В, то должен быть и третий кабель из 0 в В. Нет никаких проблем в том, что для f и g этим третьим кабелем оказывается один и тот же zB: 0 → B.
Конечно, очень далеко на таких метафорах не уедешь, но для простых вещей могут быть полезны.
Еще важная отдельная тема возникает, если начать спрашивать, что именно означает f1 = f2. Возникают разные виды equality, intensional vs. extensional теории, двумерные и бесконечномерные теории типов, а там и до гомотопий докатиться можно.
no subject
Date: 2013-04-25 09:32 am (UTC)N : A→((A→⊥)→⊥)
N = flip id
А теперь концептуальный такой вопрос.
Как можно в принципе написать функцию f : (Either A (A → ⊥)) → ⊥ ? Она же не может быть тотальной. То есть, будет ли доказательством (Either A (A → ⊥)) → ⊥ функция, которая матчит только Left или только Right?
Если да, то не очень ясно, каким боком это доказательство (нутро требует доказательство ∀ x:(Either A (A → ⊥)), а не ∃).
Если нет, то не ясно, как можно вообще написать функцию, которая делает и (Left x) → ⊥, и (Right f) → ⊥
no subject
Date: 2013-04-25 09:50 am (UTC)Мы привыкли к | как дизъюнкции, не отрицающей возможность, что обе стороны являются истиной. Так вот, именно в случае (A | ¬A) связка | имеет более сильное значение - здесь "или" исключающее. И, между прочим, интуиционистское доказательство доказывает эту более сильную форму "или".
То есть, если бы "или" было в слабом смысле, то можно было бы написать тотальную функцию f:(Either A (A→⊥))→⊥.
Высказывание ((Either A (A→⊥))→⊥)→⊥ можно перефразировать, что если бы функция f существовала, то мы бы могли опровергнуть её существование - с помощью её же. Вот в чём смысл доказательства M f = f $ Right $ f . Left.
no subject
Date: 2013-04-25 11:25 am (UTC)Именно! А точнее, мы бы получили на руки тот заветный инициальный объект, обладание которым делает одновременно существующими Кришну, Зевса, ЛММ, черепах, на которых стоит мир, Деда Мороза, единорогов, Винни Пуха и все-все-все... Только от санитаров пришлось бы скрываться.
no subject
Date: 2013-04-25 11:17 am (UTC)Потому что таков тип у той функции. Или вопрос "зачем"? Чтобы сравниться с классической логикой.
>Как можно в принципе написать функцию f : (Either A (A → ⊥)) → ⊥ ?
Как было доказано выше, если бы мы могли ее написать, это привело бы к абсурду, неконсистентности всей нашей логики, можно было бы сразу идти домой. Ибо мы описали процедуру получения ⊥ из f.
В принципе, в Идрисе для таких вещей есть слово impossible, которое ставят в недостижимых ветвях паттерн-матчинга. Например, там есть такой вот тип для decidable equality:
data Dec : Type -> Type where Yes : {A : Type} -> A -> Dec A No : {A : Type} -> (A -> _|_) -> Dec Aи пишут так, например:
Здесь trueNotFalse - функция из кое-чего в ⊥. Если бы у нас нашелся для нее подходящий аргумент, она вернула бы ⊥, но система типов нам гарантирует, что такой аргумент не найдется, поэтому ее единственный clause никогда не будет задействован, что и помечается ключевым словом impossible.
no subject
Date: 2013-04-25 01:39 pm (UTC)неее, плохая причина. Здесь был невидимый контекст. :) я начал писать тот ответ с "дык, сейчас я докажу просто с помощью X→¬¬X", потому что показалось, что дело в том, что нужно доказать это высказывание для X=(A | ¬A). В результате обнаружилась проблема с функцией f. А потом дошло, в чём разница и тонкость с дизъюнкцией в именно этом выражении.
NA является доказательством того, что нельзя одновременно иметь доказательство A и ¬A. (одновременно населить типы A и A→⊥)
А MA является доказательством того, что нельзя одновременно опровергнуть A и ¬A. (одновременно населить типы A→⊥ и (A→⊥)→⊥ - результат доказательства такой же, как и у N, т.е. MA=NA→⊥; разница в предпосылке)
Таким образом мы определяем исключающее "или". Вот это, по-моему, причина, почему нам нужно доказать и A→¬¬A, и (A | ¬A)→¬¬(A | ¬A) :)
no subject
Date: 2013-04-25 03:16 pm (UTC)интересно. Но в этом случае не подходит, потому что в построении M мы пользуемся f и с Left, и с Right - поэтому f и должна быть тотальна.
no subject
Date: 2013-04-25 05:41 pm (UTC)вот теперь я таки готов так заявить :)
У A | B = Either A B всегда есть "разложение" на проекции, то есть, наоборот, стрелки из компонент в "сумму". В данном случае это Left: A → Either A B и Right: B → Either A B. Натурально, для всех f: (Either A B)→C есть пара стрелок g: A→C и h: B→C таких, что f=[g, h], и наоборот, для каждой пары g: A→C и h: B→C есть стрелка f такая, что g=f . Left, и h=f . Right.
Это всего лишь многословное заявление того простого факта, что f: (Either A (A→⊥))→⊥ всегда можно разложить на некоторые g:A→⊥ и h:(A→⊥)→⊥, и наоборот, её всегда можно собрать из g и h, если таковые даны.
Тогда при N=flip id доказывающем в частности A→¬¬A, получаем M f = N g h = N (f . Left) (f . Right)
no subject
Date: 2013-04-26 02:18 pm (UTC)Почему, собственно?
no subject
Date: 2013-04-26 03:43 pm (UTC)no subject
Date: 2013-04-26 09:53 pm (UTC)no subject
Date: 2013-04-27 02:46 am (UTC)f : (Either A (A → ⊥)) → ⊥
Отрицание А | -A приводит к абсурду, а не утверждение.
no subject
Date: 2013-04-27 04:34 am (UTC)no subject
Date: 2013-04-28 09:28 am (UTC)В интуиционизме ничего странного тоже не заявляется. Всего лишь, мы можем доказать ненаселённость опровержения (A | -A) не зависимо от доказательства A и доказательства -A. Это на мой взгляд очень сильное утверждение.
И ещё замечательное свойство интуиционисткого построения доказательства - Either A B всегда "исключающее" - в том смысле, что каждое значение этого типа может содержать только одно из A и B, хотя не отрицается населённость обоих. Поэтому нужно доказать также -(A & -A), то есть, что A и -A не могут быть населены одновременно. Выходит, что -(A & -A) можно доказать с помощью пары -(-A → A) и -(A → -A), а это есть ничто иное как первый и второй закон классики: -A → -A и A → --A.
Таким образом, на пальцах понятно, что Either A (A→⊥) населён, но для consistency мы считаем это недоказанным, пока не будет построено доказательство - т.е. предоставлены конкретные стрелки Left и Right; одна из них будет ⊥→⊥, но чтобы выяснить, какая, нужно доказательство населённости второго.
no subject
Date: 2013-04-28 01:13 pm (UTC)Тут совсем просто:
f : (a, a -> ⊥) -> ⊥
f (a, na) = na a
no subject
Date: 2013-04-28 09:04 pm (UTC)я хотел перевести разговор на вторые два закона.
no subject
Date: 2013-05-14 09:44 am (UTC)а как тогда пишется в идрисе FalseElim?
FalseElim : ⊥ → A
FalseElim impossible
что ли?
no subject
Date: 2013-05-14 10:20 am (UTC)