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

[juan-gandhi.livejournal.com]

Прикольный трюк. Определение M красивое, но я как-то упустил, а почему это тавтологическое _|_?

В топосах это известное дело, что в топологии двойного отрицания логика становится булевой.

[deni-ok.livejournal.com]

Да, это действительно прямо на Хаскеле можно рассказывать:

> let m = \f -> f $ Right $ \a -> f (Left a)
> :t m
m :: (Either a (a -> t) -> t) -> t

Ну и тогда, для верности конкретизируем

> :set -XImpredicativeTypes
> type Bot = forall t. t
> let {m :: (Either a (a -> Bot) -> Bot) -> Bot; m = \f -> f $ Right $ \a -> f (Left a)}

[helvegr.livejournal.com]

Есть ещё красивое доказательство через call/cc: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf

[-darkus-.livejournal.com]

Вы, интуиционисты-конструктивисты, — ужасные люди :).

[sassa-nf.livejournal.com]

M f = f $ Right $ f . Left

но как-то не ясно, как строить функцию f. Точнее, если её построить как const ⊥, то не ясно, зачем городить M f.

[sassa-nf.livejournal.com]

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

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

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

[sassa-nf.livejournal.com]

хм, вообще-то не очень понятно, почему доказывается именно ¬¬(A | ¬A). Потому что на самом деле доказательство перефразирует A→¬¬A (т.е. если A доказуемо, то ¬¬A доказуемо):

N : A→((A→⊥)→⊥)
N = flip id


А теперь концептуальный такой вопрос.

Как можно в принципе написать функцию f : (Either A (A → ⊥)) → ⊥ ? Она же не может быть тотальной. То есть, будет ли доказательством (Either A (A → ⊥)) → ⊥ функция, которая матчит только Left или только Right?

Если да, то не очень ясно, каким боком это доказательство (нутро требует доказательство ∀ x:(Either A (A → ⊥)), а не ∃).

Если нет, то не ясно, как можно вообще написать функцию, которая делает и (Left x) → ⊥, и (Right f) → ⊥