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