not not (to be or not to be)

[thedeemon]

В классической логике есть закон исключения третьего, гласящий, что для любого утверждения А справедливо A | -A, т.е. либо оно верно, либо ложно. Однако это очень смелое утверждение, его можно трактовать так, что любое утверждение разрешимо (decidable), что тоже довольно нагло, и вообще герр Гёдель хмурится. Интуиционисткая логика высказываний и с ней конструктивная математика и прочая теория типов ведут себя скромнее, и такого смелого утверждения не делают. Но зато в них доказуемо вот такое:
--(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), мы однако со всей уверенностью его активно не_отрицаем. Дословно: считаем, что было бы абсурдным считать его ложным. Так и живем.

Comments

[sassa-nf.livejournal.com]

тут ещё интересный момент. В интуиционизме выбрасывают law of excluded middle, но ещё и добавляют law of contradiction: ¬A → (A → B). А это не что иное, как объявление ⊥ инициальным объектом:

∀ A B . (A → ⊥) → (A → B)

Т.е. когда A = ⊥, мы говорим о существовании стрелки из ⊥ во все объекты. Тогда если стрелок из других A в ⊥ нет, выходит, что ⊥ → (A → B), т.е. истинно (ибо есть стрелки из ⊥ во все объекты).

[thedeemon.livejournal.com]

Да, это инициальный объект. В Идрисе это отражено функцией
FalseElim : _|_ -> a
Аналогичная есть в Агде. Из абсурда следует все что угодно.
Последнюю вашу фразу не понял, что именно истинно, и в чем основная мысль.

[sassa-nf.livejournal.com]

да это я вслух радуюсь своим маленьким находкам :)

последнее "истинно" относилось к тому, что когда стрелки A → ⊥ нет, то получаем множество таким стрелок не населено, и выражение сводится к ⊥ → (A → B). Это множество населено, т.к. есть стрелки из ⊥ во что угодно из рассуждений о A = ⊥. Тут забавно также, что доказывается существование стрелки из любого типа в любой другой. А маленькая находка в том, как правила импликации тоже выходят сами собой (из абсурда следует что угодно).

[thedeemon.livejournal.com]

Если у нас есть док-во f : ⊥ → (A → B), то чтобы получить стрелку из А в В нам придется откуда-то достать ⊥ как объект и передать его f, а с этим проблема - ⊥ не населен. Стрелку из любого типа в любой можно взять только, когда мы конкретно напортачили и нарушили консистентность всей нашей логики, произведя откуда-то ⊥.

[sassa-nf.livejournal.com]

Я не вижу, в чём проблема.

FalseElim гласит, что есть стрелка из ⊥ в любой тип. Так что, существует и стрелка из ⊥ в (A → B).

[thedeemon.livejournal.com]

Все правильно, эта стрелка существует. Я про (A → B), ее существование не доказано.

[sassa-nf.livejournal.com]

да, в формальном виде понятно: не зависимо от того, населен или нет (A → B), стрелка в него существует. А как на голову надеть возможность выбрать какую-то (A → B) - вот это весело :) Видимо, как и с нулевыми стрелками в категориях, сам смысл стрелки охватить умом не получится - можно понять только в контексте композиции.

[thedeemon.livejournal.com]

Мне мысленно стрелки представляются такими трубами, а типы - эдакими бочками. В бочке может что-то находится, тогда она населена. Тогда это что-то может по трубе перейти в другую бочку, трансформируясь по дороге, и другая бочка станет населена. Но некоторые бочки и трубы всегда остаются пустыми. Вот бочка ⊥ пустая, и по трубам из нее ничего не идет. :)

[sassa-nf.livejournal.com]

О, это ещё не всё :)

Я ещё как-то пытался соединять объекты оптоволокном :) по одному кабелю на стрелку, и по одному волокну в кабеле на каждую точку объекта домена - так тогда можно суръекции от инъекций отличать; например, можно визуализировать, что за эквалайзер такой и как это вообще квадраты коммутируют. "Включил свет" - посмотрел, где и какие точки засветились, да ещё каким цветом. :)

В категорном смысле есть ещё один занятный факт: для стрелок z_A: 0 → A z_B: 0 → B и двух стрелок f, g: A → B верно следующее: f . z_A = g . z_A = z_B Так вот, здесь аналогии с трубами и кабелями заканчиваются :)

[thedeemon.livejournal.com]

C оптоволокном прикольно, да. :)
В ситуации с композицией, имхо, аналогия еще держится: закон композиции говорит, что если у нас два таких кабеля, один идет из 0 в А, второй из А в В, то должен быть и третий кабель из 0 в В. Нет никаких проблем в том, что для f и g этим третьим кабелем оказывается один и тот же z_B: 0 → B.

Конечно, очень далеко на таких метафорах не уедешь, но для простых вещей могут быть полезны.

Еще важная отдельная тема возникает, если начать спрашивать, что именно означает f1 = f2. Возникают разные виды equality, intensional vs. extensional теории, двумерные и бесконечномерные теории типов, а там и до гомотопий докатиться можно.