Comments 88
Тут не в операциях над множествами дело, а в порядке предикатов. Предикат "X бреет того, кто не бреется сам" не имеет порядка и потому не является исчислимым. Это бесконечная рекурсия, по сути.
В математической (и обыденной) логике нет формализма, который позволял бы исчислить предикат, применяемый к самому себе. Поэтому все рассуждения о самобреющемся брадобрее, множестве всех множеств и т.п. являются просто артефактами нечёткости естественного языка. Им невозможно придать какое-либо формальное содержание.
Простите, но здесь речь идет не о математической логике, а об алгебре множеств и теории отношений, которую тоже можно изложить на основе алгебры множеств (если определить отношение как подмножество декартова произведения множеств). Там «самоприменимость» (т.е. по сути рефлексивность некоторых отношений) имеет содержание и не вызывает непонимания в естественном языке (можно привести немало ясных примеров рефлексивных бинарных отношений). В аксиоматической теории множеств, которая, кстати, формулируется на основе исчисления предикатов, такой формализм для самоприменимости имеется и часто используется. Хотя ясности, как мне представляется, это не прибавляет. Согласен с Вами в том, что множество всех множеств определяется с помощью бесконечной рекурсии, и это как раз и есть «артефакт нечеткости» в естественном языке.
Когда мы говорим, что наше утверждение о множествах (например, про брадобрея или про универсальное множество) "истинно" или "ложно" в каком-то смысле, то это именно исчисление предикатов. Утверждение про брадобрея сформулировано так, что его невозможно записать на формальном языке предикатов какого-либо порядка. А следовательно, невозможно и вывести его истинностное значение никакими известными мне правилами вывода.
Как только мы фиксируем порядок брадобреевского предиката каким-либо конкретным числом, тут же из этого можно будет вывести, что брить себя он должен. Но бреющим себя он является в языке предикатов более высокого порядка, чем тот порядок, который он анализирует для принятия решения о бритье.
Не понимаю, почему в математической логике первого порядка нельзя записать утверждение о бреющемся брадобрее? Представим отношение «брить» как предикат S(x,y). Тогда отношение «бриться» можно записать как S(x,x). Отношение «больше или равно» можно записать как предикат M(x,y). Тогда запись M(x,x) тоже правильна и для множества чисел всегда истинна. Самоприменимые предикаты не редкость в математической логике. Взять хотя бы теорему Геделя о неполноте, при доказательстве которой используется самоприменимый предикат.
бреетсясам (вася) - факт, то есть утверждение в логике высказываний нулевого порядка.
Любой (X), такой что: не (бреетсясам (X)) - квантор общности, конструирующий множество клиентов брадобрея, который является высказыванием в логике первого порядка только в том случае, когда бреетсясам - утверждение в логике нулевого порядка. Просто по определению синтаксиса предиката первого порядка.
А раз так, то утверждение о поведении брадобрея, построенное на кванторе первого порядка, может включать самобритость только в виде факта, но не в качестве вывода из квантора.
Это что-то новенькое: начинать определение самоприменимости с выражения в логике нулевого порядка, т.е. в исчислении высказываний. Но, как мне кажется, ясности это вовсе не прибавляет, наоборот, сильно усложняет и без того непростую ситуацию. В литературе по математической логике самоприменимость пляшет от двуместного предиката, а не от бесструктурного высказывания. Предложение «A бреет A», также как и предложение «A не больше A» к логике нулевого порядка никакого отношения не имеют.
Секунду, это только вы здесь выруливаете на самоприменимость через предложение "А бреет А". А я вывожу истинность конкретного утверждения "Брадобрей Фёдор бреет Фёдора" из конкретных фактов "Вася бреет себя", "Петя бреет себя", "Слава не бреет себя" и т.д. и должностной инструкции брадобрея, о чём в точности и говорится в исходной задаче. И сам этот вывод строится в логике второго порядка над фактами (т.е. содержит утверждения о кванторах). Выше второго порядка брадобрей не лезет, сам в своём поведении ограничиваясь просто кванторами, содержащими утверждения о фактах, поэтому смело бреет себя.
То есть:
1) Нам даны факты о жителях города.
2) Должностная инструкция брадобрея написана в логике первого порядка (или пусть даже N-го), и поэтому может рассматривать только факты (или предикаты до (N-1)-го порядка). Поэтому поведение брадобрея чисто синтаксически не выводится из себя самого, не совпадают типы предикатов. И если брадобрей себя бреет по инструкции, то он не становится самобритым в фактическом смысле. Поэтому брадобрей всегда должен быть выбрит – либо как первичный факт в логике нулевого порядка, либо в результате применения инструкции в логике первого порядка.
3) Вся рефлексия над этой задачей и весь необходимый для рассуждений о ней логический вывод поэтому исчерпывается вторым (или (N+1)-м) порядком.
Отдельно выскажусь по вопросу: может ли в принципе исчислимое высказывание быть самоприменимо? Может, но не как попало с мутным брадобреем, а через предикат специального вида – комбинатор неподвижной точки. Поскольку работа городского брадобрея не содержит ничего похожего на λf.(λx.f (x x)) (λx.f (x x)) , то самоприменимость для него закрыта.
бреется сам (вася) - факт, то есть утверждение в логике высказываний нулевого порядка.
Так "факт" - это истинностная оценка соответствующего предиката. Т.е. у нас есть предикат "бреет(A, B)", который true, если A бреет B, и false в противном случае. Тогда мы сразу можем определять например множества брадобреев {x: exists y. бреет(x, y) } или множество бритых {x: exists y. бреет(y, x) }
тогда "есть брадобрей, который бреет всех, кроме самого себя" - это "exists x. forall y. бреет(x, y) <=> !бреет(y, y)", или "exists x. самобреетсянонет(x)", где "самобреетсянонет(х)" = "forall y. бреет(x, y) <=> !бреет(y, y)". тогда, если добавить в теорию это высказывание как аксиому, то теория становится противоречивой, т.е. у высказывания "forall x. самобреетсянонет(х) => бреет(x, x)". нет истинностной оценки (т.к. в принципе у теории нет модели)
Это верно, но я хотел обратить внимание немного на другое - что "бреет как факт" и "бреет по принадлежности к множеству" - это разные по своей природе суждения, относящиеся к логике нулевого и первого порядка соответственно. А поскольку в естественном языке не маркируется порядок предикатов, то вот и возникает мнимый парадокс, связанный с незаметной подменой предиката нулевого порядка на предикат первого.
Тут выводы математической логики полностью соответствуют здравому смыслу.
Это верно, но я хотел обратить внимание немного на другое - что "бреет как факт" и "бреет по принадлежности к множеству"
В нашем случае нет ни каких "бреет по принадлежности к множеству" и вообще ни каких множеств нет. Только логика первого порядка и одна аксиома поверх нее.
то вот и возникает мнимый парадокс
Он не мнимый, он вполне реальный. У нас есть вполне реальная теория, которая противоречива, а потому в ней выводимо любое утверждение вместе с его отрицанием.
связанный с незаметной подменой предиката нулевого порядка на предикат первого.
Ни чего ни чем не подменяется, у нас одно конкретное утверждение:
"exists x. forall y. P(x, y) <=> !P(y, y)"
все. любая теория первого порядка с такой аксиомой для любого P противоречива.
Ну и да, ни каких "утверждений второго порядка", про которые вы выше говорили, тут и подавно нет.
Да, еще момент:
"бреет как факт"
"вася бреет петю" в логике высказываний сформулировать нельзя
Почему нельзя? Можно, если мы не будем вводить для этого ваш предикат P. Любое ни от чего не зависящее утверждение можно сформулировать в логике высказываний.
Вы здесь становитесь жертвой собственной модели. Мы же не обязаны решать проблему через ваш универсальный предикат "брить".
У вас, как и у автора статьи, есть стремление обязательно ввести наиболее физичные обозначения (в данном случае обозначить свободными переменными именно людей). Но для доказательства (не)существования логического вывода этого недостаточно. Мы же можем поступать и тоньше. Допустим, взять за свободные переменные двойки людей или что-то ещё.
А так вы доказали только то, что не существует универсального предиката бритья P, применимого как к брадобрею, так и к самобреющимся гражданам. Что я использовал как отправную точку своих дальнейших рассуждений.
А утверждением второго порядка является ваше утверждение:
любая теория первого порядка с такой аксиомой для любого P противоречива.
Не понимаю, почему в математической логике первого порядка нельзя
записать утверждение о бреющемся брадобрее? Представим отношение «брить» как предикат S(x,y). Тогда отношение «бриться» можно записать как S(x,x). Отношение «больше или равно» можно записать как предикат M(x,y). Тогда запись M(x,x) тоже правильна и для множества чисел всегда
истинна.
Очень хорошо. Теперь на самом деле запишите утверждение, что брадобрей бреет сам себя. Введение в ваш язык бинарного предиката S не наделяет его автоматически никакими свойствами, семантикой и тому подобным.
Как и введение предиката M, к слову, и сама по себе формула M(x,x) не обязана быть всегда истинной. Я, например, могу интерпретировать M(x,y) как утверждение о том, что `x = y + 1` — что ж в вашем абзаце мне это запретит делать?
Взять хотя бы теорему Геделя о неполноте, при доказательстве которой используется самоприменимый предикат.
Нет там никаких самоприменимых предикатов. Там предикат на множестве натуральных чисел, и существование определённого числа, которое при засовывании его в предикат приводит к некоторому противоречию, интерпретируется на метаязыке, а не в языке.
Почему?
в классической теории множеств на оператор принадлежности не наложено никаких ограничений, но вы можете выбрать альтtрнативную теорию множеств, Typed Set Theory (TST) или ее современное развитие: New Foundations (NF) где есть стратификация
На оператор принадлежности может и не быть наложено никаких ограничений, но конкретно множество всех небритых задано через квантор общности, а любой квантор использует предикаты меньшего порядка.
Нет такого.
В теории первого порядка кванторы работают по объектам теории (например, в формальной арифметике - по числам). Это единственное ограничение
В теории второго порядка кванторы работают по либо множествам объектов (monadic 2nd level theory) либо в общем случае по функциям или выражениям.
В теории множеств первого порядка (ZFC, NBGC, MK) есть только один тип объектов - множества. Поэтому запись
вполне валидна
Запись-то валидна, только нас просят в задаче вывести истинностное значение предиката, а не сконструировать множество, поэтому от предикатов в каком-либо виде мы не уйдём. А в объекты теории в общем случае не входят её собственные формулы.
Чисто по синтаксису в утверждении первого порядка, содержащем квантор, все символы кванторов связанные.
Вот смотрите пример:
https://en.wikipedia.org/wiki/Urelement
Quine atoms
Quine atoms (named after Willard Van Orman Quine) are sets that only contain themselves, that is, sets that satisfy the formula x = {x}.[7]
Quine atoms cannot exist in systems of set theory that include the axiom of regularity, but they can exist in non-well-founded set theory. ZF set theory with the axiom of regularity removed cannot prove that any non-well-founded sets exist
То есть вы можете ввести такие элементы аксиомами, и даже более:
Aczel's anti-foundation axiom implies that there is a unique Quine atom. Other non-well-founded theories may admit many distinct Quine atoms; at the opposite end of the spectrum lies Boffa's axiom of superuniversality, which implies that the distinct Quine atoms form a proper class.[8]
Все это, на мой взгляд, показывает невозможность полагаться на 'здравый смысл', 'очевидность' и житейскую логику. Впрочем, точно такая же ситуация, например, с теорией относительности
Тут я, к сожалению, несколько утратил нить Ваших рассуждений. Но фундаментально Вы, должно быть, правы, поскольку, раз уж логика строится из теории множеств, то разным теориям множеств, видимо, должны соответствовать разные логики.
А что думаете про этот анализ?
Выберу время и посмотрю. Но прежде был бы Вам весьма признателен, если бы Вы сами написали, что думаете об этой статье.
Я думаю автор не прав, но не могу понять в чём именно.
Жаль, мне бы было очень интересно и полезно узнать, в чем я не прав.
Ограничения подмены термина выражаются как недопустимость равенства некоторых пар множеств (например,
).
Допустим, наш универсум - это мебель в отдельно взятой комнате. Тогда вполне может быть, что все деревянные предметы - это табуретки, а все табуретки из дерева. Множество табуреток равно множеству деревянных предметов. Но где же тут подмена понятий? Это обычный экспериментальный факт
Видимо нигде.)
Вы, по-моему, путаете равенство множеств в конкретной ситуации и подмену термина в рассуждениях, в которых, допустим, говорится о «деревянных предметах», а из контекста рассуждения ясно, что речь идет всего лишь о «табуретках». В своем определении я говорю всего лишь о том, что при логическом анализе не рекомендуется отождествлять деревянные предметы и табуретки для всех возможных случаев.
Вся эта статья демагогия по одной простой причине: изначально у нас не было утверждения "все честные люди не мошенники" :). Не стоит обращаться к какому-то"здравому смыслу", с точки зрения алгебры логики это утверждение взялось из воздуха. Но, спасибо что прзнакомили меня с этим парадоксом.
Спасибо за замечание. Не стану доказывать, что моя статья не демагогия. Не мое дело. Зато Ваша заметка, по-моему, демагогия. То, что «изначально у нас не было утверждения "все честные люди не мошенники"» не означает демагогии. Это утверждение можно было вставить в задачу сразу, а не потом. Это ничего бы не изменило с точки зрения логики. И то, что «это утверждение взялось из воздуха» - это с Вашей точки зрения, а не с точки зрения алгебры логики. Алгебра логики не предписывает порядок посылок. В ней все посылки соединены операцией И (конъюнкция), а эта операция коммутативна (т.е. не зависит от порядка).
А это означает, что отношение «брить» антирефлексивно.
Это рассуждение, может быть, и верно относительно парикмахерской, но не затрагивает сущностную природу парадокса. Например, мушкетёр платит за выпивку за тех мушкетёров, кто остался должен трактирщику. Ясно, что отношение возврата долга третьему лицу рефлексивно. Также в такой формулировке задача исключает выделенную роль брадобрея (но при этом трактирщик при удачном для себя финансовом состоянии мушкетёров получит оплату многократно).
На этом примере также ясно видна бессмысленность заявления мушкетёра трактирщику: “Теперь, когда я тебе заплатил, я ничего не должен, так что верни деньги, каналья!”
Честно, сказать, мне трудно понять Ваши выкладки. Почему, например, отношение возврата долга третьему лицу рефлексивно? Возвращают долг тому, кому должны, а что тогда означает фраза «должен самому себе»?
Какая формулировка задачи исключает роль брадобрея? Как трактирщик получит оплату многократно?
И еще. Вы используете для отношения «бриться» то логику нулевого порядка, то N+1-го. Мне это тоже непонятно. Как показал наш с Вами собеседник Kergan88, для этого достаточно логики первого порядка. И в литературе то же самое говорится. Или я чего-то не знаю?
Честно, сказать, мне трудно понять Ваши выкладки. Почему, например, отношение возврата долга третьему лицу рефлексивно? Возвращают долг тому, кому должны, а что тогда означает фраза «должен самому себе»?
Все мушкетёры должны одному лицу – трактирщику, это константа. А отношение возврата долга здесь между плательщиком и должником. Нет никакой разницы для мушкетёра, возвращать свой долг или чужой, это точно такое же платёжное поручение в адрес трактирщика.
Какая формулировка задачи исключает роль брадобрея?
Именно формулировка про мушкетёров, платящих друг за друга.
Как трактирщик получит оплату многократно?
Каждый мушкетёр при деньгах, увидевший долг своего товарища, заплатит трактирщику за этого товарища. Поэтому, если у нас среди мушкетёров M богатых и N должников (это могут быть и пересекающиеся множества), то трактирщик получит M*N долгов вместо N.
И еще. Вы используете для отношения «бриться» то логику нулевого порядка, то N+1-го. Мне это тоже непонятно. Как показал наш с Вами собеседник Kergan88, для этого достаточно логики первого порядка. И в литературе то же самое говорится. Или я чего-то не знаю?
Я, в свою очередь, не понимаю, что вы называете отношением "бриться". Есть бритьё как свойство гражданина (в логике нулевого порядка), а есть бритьё как обязанность брадобрея (в логике первого порядка). Никакого парадокса здесь вообще нет, так как логика первого порядка оперирует в своих кванторах только суждениями нулевого порядка.
Но если, по вашему мнению (а не по моему), парадокс брадобрея действительно имеет содержательность, то есть имеет какое-либо синтаксическое представление в правилах логического вывода (а любой логический вывод строго синтаксичен), то тогда брадобрей будет уходить в своих рассуждениях бесконечно вверх по цепочке предикатов всё более высокого порядка в бестиповом исчислении предикатов (так как в типизированном исчислении самоприменимость невозможна по определению).
Я говорю про N-й порядок только для того, чтобы отсечь контраргумент, что парадокс невозможен в логике первого порядка, но, допустим, был бы возможен в каком-то более высоком порядке. Логикой какого бы порядка ни руководствовался брадобрей в своих рассуждениях, он всё равно не сможет судить о себе самом в рамках заданного в задаче правила, так как оно не содержит неподвижную точку (то есть синтаксическую возможность для исчислимой рекурсии).
А с точки зрения здравого смысла то же самое можно объяснить вот как. Допустим, некий человек решил каким-то образом описать все свои мысли. Если он подойдёт к этому вопросу чисто рефлексивно, то он уйдёт в бесконечную рефлексию, встав перед необходимостью описывать свои мысли по поводу мыслей, мысли по поводу мыслей по поводу мыслей и т.д. ad infinitum. Но он может (теоретически) поступить по-другому – скинуть картину электрических потенциалов своего мозга на компьютер и там уже её проанализировать отдельно от реального мозга. Это и есть неподвижная точка (программа, печатающая свой собственный исходный текст, задвоенная форма λf.(λx.f (x x)) (λx.f (x x))). Единственная исчислимая возможность для самоприменения. У брадобрея таких средств не предусмотрено.
Извините, но мне трудно вас понять. На некоторые мои вопросы я так и не получил внятного ответа. Покажу только на примере вопроса «Почему отношение возврата долга третьему лицу рефлексивно?»
Ваша первая фраза «Все мушкетёры должны одному лицу – трактирщику, это константа». Вы приводите частный случай, выраженный замкнутой формулой (потому и константа), но для естественных рассуждений отношение между должниками и заимодавцами – это просто бинарное отношение, которое не всегда можно выразить замкнутой формулой исчисления предикатов. И мушкетеры у вас по характеру такие, какие вам нужны для обоснования вашей точки зрения: «Нет никакой разницы для мушкетёра, возвращать свой долг или чужой». Но должниками могут быть не только благородные мушкетеры! А я спрашивал про возврат долга вообще, а не только применительно к придуманным вами мушкетерам, которые выплачивают свои или чужие долги, даже не удосужившись узнать, получил ли трактирщик все, что ему причитается.
С другими ответами и рассуждениями картина аналогичная.
Поэтому в силу трудностей понимания, я вынужден прервать СВОЕ участие в дискуссии с вами по данной теме. Спасибо за замечания.
Если бы вы чуть внимательнее читали, что я пишу, то заметили бы, что я говорю об отношении не между должниками и заимодавцами, а между должниками и плательщиками. И тем более не про возврат долга вообще, а про конкретную ситуацию оплаты пирушки мушкетёрами, иллюстрирующую парадокс Рассела на более понятном примере.
Брадобрей ваш тоже почему-то не спешит узнать, не побрил ли другой брадобрей его клиента. Это просто модельная ситуация же, а не рассуждения о жизни мушкетёров и галатерейщиков.
это просто бинарное отношение, которое не всегда можно выразить замкнутой формулой исчисления предикатов
То, что невозможно выразить замкнутой формулой исчисления предикатов, не имеет значения истинности, и из него нельзя выводить следствия. Математическая логика – это набор чисто синтаксических преобразований предикатов друг в друга.
Вы затронули интересную и важную для меня тему, поэтому я решил отменить свой запрет на свое участие в дискуссии с вами. Но прошу не рассказывать мне про благородных и беспечных мушкетеров и рассуждающих брадобреев, а то у меня создается впечатление, что вы с помощью словесной эквилибристики стремитесь сбить меня с толку. Если ошибся, извините.
Вы пишете:
То, что невозможно выразить замкнутой формулой исчисления предикатов, не имеет значения истинности, и из него нельзя выводить следствия. Математическая логика – это набор чисто синтаксических преобразований предикатов друг в друга.
Вот это, по-моему, и есть слабое место математической логики, из-за чего при ее использовании возникают трудности с прикладным логическим анализом (трудности с моделированием и анализом неопределенностей, выводом следствий с заранее заданными свойствами, распознаванием ошибок в рассуждении и т.д.).
Но предложена система логического анализа, с помощью которой некоторые из этих проблем решаются. Это алгебра кортежей. Если найдете время, посмотрите статью Как вычислять интересные следствия.
Из рисунка видно, что контрапозиции исходных суждений можно легко построить, используя два простых правила.
Правило 1: Если исходное суждение соединяет литералы в одной строке, то его контрапозиция соединяет противоположные литералы в другой строке, при этом направление дуги меняется на обратное.
Правило 2: Если исходное суждение соединяет литерала в разных строках, то его контрапозиция соединяет противоположные литералы, при этом направление дуги (вверх или вниз) не изменяется.
Почему не одно простое правило: контрапозиция соединяет противоположные литералы, при этом направление дуги (влево или вправо) меняется на обратное?
Автор!
Изучите наконец ZFC или другую аксиоматику. Вы продолжаете работать в рамках так называемой "наивной теории множеств", которая заведомо противоречива
Причем это известно лет так 140 как
Уважаемый, Tzimie !
Высокий рейтинг в Хабре не дает вам права принижать собеседника, тем более без достаточных оснований.
Что касается "наивной теории множеств" (Naive set theory), то появилась она в 1960-м году после публикации одноименной книги Халмоша. Сам Халмош называл наивную теорию множеств «аксиоматической теорией множеств с наивной точки зрения». В моей статье речь идет об алгебре множеств (algebra of sets), которая была описана в книге Куранта и Роббинса «Что такое математика?», впервые изданной в 1941 году. Там, кстати было высказано предположение, что законы алгебры множеств можно обосновать без аксиом.
Что касается заведомой противоречивости алгебры множеств (не «наивной теории множеств»!), то об этом, насколько я знаю, в публикациях по математике ничего нет.
Наивная теория множеств использовалось ещё Кантором в 19 веке (проверьте в Вики)
Что касается теорий без аксиом, то это лирика а не наука.
В Англоязычной Вики говорится о 40-х годах 20 века (имеется в виду термин НАИВНАЯ теория множеств, а не просто теория множеств).
Что касается «лирики», то ей почему-то не побрезговали заняться известные математики (имею в виду Куранта и Роббинса). Другое дело, что эта «лирика» мало кого из математиков заинтересовала. Но попытаться развить эту тему никто не запретил.
Нет
https://en.wikipedia.org/wiki/Naive_set_theory
The first development of set theory was a naive set theory. It was created at the end of the 19th century by Georg Cantor as part of his study of infinite sets[5]
История с наивной теорией множеств научила, что правдоподобные рассуждения могут завести куда угодно, и могут легко сгенерить противоречие. Именно поэтому считается хорошим тоном верифицировать доказательство теорем автоматическими верификаторами. Иначе получится как в широко известной истории c abc-гипотезой, которая доказана только на территории Японии: https://en.wikipedia.org/wiki/Abc_conjecture
Почти убедили по поводу дат. Но, я думаю, во времена Кантора никто не употреблял слово Наивный. А я говорил лишь о термине.
Что касается «могут сгенерировать противоречие» то это обоснование по аналогии («История научила…»). В алгебре множеств можно обойтись без признания множества элементом другого множества. А именно это лежит в основе парадоксов теории множеств + самоприменимость отношения принадлежности. И еще: известны ли парадоксы в рамках такой алгебры множеств?
Но, я думаю, во времена Кантора никто не употреблял слово Наивный. - согласен)
Если множества составлены только из "настоящих" элементов (не множеств, в терминологии теории множеств это Urelement) то вроде, как мне кажется, все парадоксы исчезают.
Но как работать с такой теорией? Рассмотрим, например, теорию где множества не могут быть элементами других множеств, а в качестве Urelements выступают целые числа, ну либо что-то другое. При этом вы должны надеяться на непротиворечивость системы Urelements, не используя саму теорию множеств. Конечно, если количество Urelements конечно, то все очевидно.
Во-первых, конечное – не так уж и плохо. Конечно множество слов, произнесенных всеми людьми во все времена со дня появления Гомо Сапиенс, также конечно множество атомов во Вселенной (по современным представлениям). Также не будет проблем, если мы воспользуемся потенциальной бесконечностью (метод математической индукции, сходимость в анализе и др.). С актуальной бесконечностью сложнее, тут уже алгебра множеств пока не тянет.
Вы спрашиваете, как работать с такой теорией? Так она же уже работает в ЭВМ с фон Неймановской архитектурой. Только многим это неприятно признать. С нейросетями – мне трудно судить – плохо знаю. Но, по-моему и у них в микропроцессорах конечный базис с булевой (троичной и т.д.) логикой.
На алгебре множеств основана алгебра кортежей. В ней разработаны методы логического анализа, которые закрывают некоторые бреши в математической логике (трудности с моделированием и анализом неопределенностей, выводом следствий с заранее заданными свойствами, распознаванием ошибок в рассуждении и т.д.).
И еще одно. Мне кажется, что во многих отношениях любую науку лучше начинать с простого и посмотреть, что из этого простого может получиться. А потом уже усложнять. Алгебру множеств можно усложнить, добавив аксиомы теории множеств (те, которые есть, или новые, усовершенствованные). И работы всем хватит и удовлетворения.
Вы спрашиваете, как работать с такой теорией? Так она же уже работает в ЭВМ с фон Неймановской архитектурой.
В ЭВМ работает конструктивное её подмножество. Аксиома (или как там у вас это называется во внеаксиоматическом мире) исключенного третьего (или снятия двойного отрицания) там не работает.
Впрочем, в любом случае то, что работает в ЭВМ, как раз основано на теории множеств и её аксиоматике. Алгебра этих множеств без инструментов теории множеств не работает (если вы занимаетесь математикой, конечно, а не упомянутой рядом лирикой).
Почему же снятие двойного отрицания в ЭВМ не работает. Как раз работает. Иначе закон контрапозиции тоже не будет работать, а как без него можно? Это в интуиционистской логике этот закон не работает. Не надо меня и читателя в заблуждение вводить.
Что касается лирики, то это всего лишь необоснованный ярлык.
Контрапозиция никак со снятием двойного отрицания не связана.
Как же не связана? Из утверждения «Если A то не B» получаем «Если B то не A», а не только «Если не не B то не A»
Уверен с доказательством от противного вы прекрасно знакомы.
Возможно, знаю кое-что еще кроме этого. А что Вы этим хотите сказать?
Почему же снятие двойного отрицания в ЭВМ не работает. Как раз работает.
Нет, не работает. Не работает потому, что снятие двойного отрицания невычислимо. Если вы имеете утверждение (A → ⊥) → ⊥, то само это утверждение не даст вам никакой объект A, с которым можно было бы работать.
Иначе закон контрапозиции тоже не будет работать, а как без него можно?
Он только в одну сторону работать не будет, но без него можно прекрасно: вон, почти весь вещественный анализ спокойно строится на конструктивной математике.
Не надо меня и читателя в заблуждение вводить.
Читателя и правда не надо, но вот вас в заблуждение ввести не получится потому, что это идемпотентная функция ;]
Вообще-то в публичной дискуссии не принято обзывать оппонента нелестными эпитетами.
ЭВМ состоит из многих деталей, в том числе микропроцессоров, а в них соблюдаются все законы булевой алгебры, в том числе и закон двойного отрицания. Что касается языка, на котором работает ЭВМ, то можно ввести много языков, правда, не во всех случаях результат получится удачный – в ЭВМ он просто не будет работать. Ваши доводы относятся к языку, а не к элементной базе ЭВМ.
Причём тут элементная база ЭВМ? ЭВМ (и равные ей по выразительной мощности) вещи можно строить из разных компонентов, но это всё совершенно неважно. Важно, что вы сможете на ней запускать.
В конце концов, всякие там транзисторы весьма активно пользуются квантовыми эффектами, но это не делает ЭВМ квантовым компьютером.
А что такое эти ваши целые числа? Вроде бы как это как раз ∅, {∅}, {{∅}} и т.д.
Боюсь, что аксиоматически определить числа без теории множеств будет весьма затруднительно.
Верно. В самом начале использовали Urelements, но потом поняли, что теория множеств не нуждается в каких либо элементах, потому что их можно изобразить подобным образом
То есть по большому счету, теория множеств это 'бестелестная' теория, теория о способах вложенности скобок, бесконечные ...{{{}{{}}}{}{{}}}}}...
Чисто философски меня колбасит от этой мысли....
Да если б только теория множеств, но и всё остальное фактически построено из этих скобок. Пустотная природа материи :)
А почему аксиоматику Пеано не рассматриваете? Там все более прозрачно, чем эти пустые скобки.
Аксиоматика Пеано обращается к семантике, то есть к нашему разуму. А математическая теория, как я глубоко убеждён, должна быть целиком чисто синтаксична, то есть доступна к выводу тупым механическим устройством вроде компьютера. Иначе возникают подозрения в каком-то тонком жульничестве.
Ну и потом, в чисто практическом смысле аксиомы Пеано мне сами по себе никак не позволят построить арифметический вычислитель средствами лямбда-исчисления (то есть вывести определение арифметических операций в виде чисто синтаксических преобразований аргуметов). А это я полагаю важной вещью.
0 - натуральное число, n+1 - тоже натуральное для любого натурального n.
Вы тут натуральное число определяете через 0 и 1, которые сами являются натуральными числами (0 на самом деле нет, но это неважно), да ещё и операцию +, которая сама задана на множестве натуральных чисел, а эту операцию ведь тоже надо как-то определять. Сразу несколько порочных кругов в определениях.
Не, если совсем глубоко копать, то дело именно в пустых скобках. Это глубокие основы исчисления предикатов, лежащие в теории множеств.
+1 - это операция, по определению дающая следующее число и всё. Можно и так записать:
1 = next(0); 2 = next(1) = next(next(0))
И это более фундаментальное определение, чем через множества, ибо последнее - это частный случай, где 0 - пустое множество, а next - заворачивание во множество.
Тогда надо вводить все аксиомы Пеано, а не только то, что Вы написали. Среди которых есть и такая, что 1 (ну или 0) не следует ни за каким натуральным числом, а это совершенно непонятно как формально выводить и проверять.
Другими словами, не построив операцию next каким-то совершенно конкретным образом, мы не можем быть уверены, что она не завернётся в цикл. А тогда и не получится рассуждать о ней абстрактно от реализации.
А вот то, что напечатанные фигурные скобочки никогда не стираются принтером – это и арифмометру “Феликс” понятно.
Аксиомы выводятся из самих себя.
Не завернётся, это следует из аксиом.
Среди которых есть и такая, что 1 (ну или 0) не следует ни за каким натуральным числом, а это совершенно непонятно как формально выводить и проверять.
Как всегда — рассмотрением случаев. Вам нужна теорема (x : M) → 0 = succ x → ⊥ , где M — какое-то ваше множество, индуктивно определённое. Вы просто рассматриваете варианты определения x и делаете выводы.
Другими словами, не построив операцию next каким-то совершенно конкретным образом, мы не можем быть уверены, что она не завернётся в цикл.
Не нужно, next/succ постулируется (или, говоря более строго, является одним из конструкторов вашего индуктивного типа).
Без теории множеств натуральные числа определить вполне можно: вам нужен простой советский natural numbers object.
Мне кажется, многие утверждения участников дискуссии, представляемые как безусловные истины, на самом деле не более, чем мнения. В качестве подтверждения приведу цитату из книги Р. Голдблатта «Топосы. Категорный анализ логики».
«Конечно, можно мыслить объекты математического изучения как множества, однако уже нет уверенности, что в будущем их будут рассматривать так». Так что алгебра множеств с этой точки зрения тоже под вопросом.
Но есть и ошибочные утверждения. Вы пишете
"В ЭВМ работает конструктивное её (т.е. алгебры множеств - AntiLogik) подмножество. Аксиома (или как там у вас это называется во внеаксиоматическом мире) (называется закон - AntiLogik) исключенного третьего (или снятия двойного отрицания) там не работает".
Может ли кто-нибудь обосновать, что принципы действия ЭВМ основаны на интуиционистской логике?
Мне кажется, многие утверждения участников дискуссии, представляемые как безусловные истины, на самом деле не более, чем мнения.
Мнением может быть принятие того или иного набора аксиом (хотя смысл таких мнений от меня ускользает). Выводы из них объективны с точностью до человеческих ошибок.
«Конечно, можно мыслить объекты математического изучения как множества, однако уже нет уверенности, что в будущем их будут рассматривать так»
Ух, какой забористый перевод. Похоже, эту книжку лучше действительно читать в оригинале. Но, впрочем, это далеко не самая интересная цитата — смысл и интуиция за теми же NNO там раскрывается куда лучше,
Может ли кто-нибудь обосновать, что принципы действия ЭВМ основаны на интуиционистской логике?
Написал рядом, но могу повториться: потому что ЭВМ по определению вычисляет. Аксиома исключённого третьего принципиально невычислима: знание истинности «a или не a» не позволит вам построить конкретный вариант, который на самом деле реализуется, и вывести его на экран.
Да, вы можете на ЭВМ формализовать язык на метаязыке, добавить в язык (не в метаязык) аксиому исключённого третьего (и любые другие неконструктивные постулаты) и дальше что-то там доказывать с его использованием, но это не сделает ваш метаязык (которым на самом деле оперирует ЭВМ) неконструктивным.
Насчет цитаты спорить трудно, может быть, перевод книги Голденблатта не совсем удачный. Оригинала у меня, к сожалению, нет.
Что касается закона исключенного третьего и двойного отрицания, то это законы не только алгебры множеств, но и булевой алгебры. А законы булевой алгебры соблюдаются в элементной базе многих ЭВМ, в частности, в цифровых. По Вашему же, выходит, что булева алгебра неконструктивна? А, по-моему, это терминологическая несообразность: интуиционистскую математику, в которой не соблюдаются эти законы, назвали «конструктивной». Тогда получается, что булева алгебра неконструктивна и ее можно на свалку выкинуть. И исчисление высказываний туда же. Ах, язык, язык!
Кстати, нашел оригинал книги Голдблатта (прошу прощения за опечатку фамилии в прошлом письме). Вот точная цитата (стр.. 15):
It may be the case that the objects of mathematical study can be thought of as sets, but it is not certain that in the future they will be so regarded. No doubt the basic language of set theory will continue to be an important tool whenever collections of things are to be dealt with. But the conception of the things themselves as sets has lost some of its prominence through the development of a natural and attractive alternative.
А законы булевой алгебры соблюдаются в элементной базе многих ЭВМ, в частности, в цифровых.
Нет, потому что вы снова рассматриваете конструктивное подмножество классической логики, но почему-то делаете вывод, что выполняется вся классическая логика.
По Вашему же, выходит, что булева алгебра неконструктивна?
Классическая — да, абсолютно верно, неконструктивно.
А, по-моему, это терминологическая несообразность: интуиционистскую математику, в которой не соблюдаются эти законы, назвали «конструктивной».
Ну мы так в спор о терминах уйдём, а такие споры скучные. Если вам так удобнее, можете читать «конструктивный» в моих сообщениях как «интуиционистский».
Просто ИМХО соответствующую математику лучше называть конструктивной, потому что интуиция-то у каждого своя, а конструктивные доказательства утверждений через прямое построение соответствующих объектов — они объективные.
Тогда получается, что булева алгебра неконструктивна и ее можно на свалку выкинуть. И исчисление высказываний туда же.
Зачем на свалку? Просто если я хочу что-то доказать и работаю с пруверами (и особенно если я хочу эстрагировать из доказательства выполняемый код), то мне, скорее всего, придётся работать в конструктивном подмножестве. Более того, в некоторых теориях исключённое третье несовместно с другими аксиомами, а между исключённым третьим и инъективными конструкторами я выберу последнее просто не задумываясь — оно полезнее по жизни.
Вот теперь у меня проблема. Дано множество S={a, c} в универсуме U = {a, b, c, d}. В ЭВМ множество S можно представить как битовый вектор 1010. Мне нужно вычислить дополнение S. Тогда я просто даю команду инвертировать вектор. Получаю 0101. А если мне нужно вычислить дополнение дополнения S? Тогда непонятно что делать: то ли инвертировать вновь полученный вектор, то ли искать конструктивного математика и просить помощи у него?
Имеется огромный класс (десятки тысяч) практически значимых задач, которые в общем случае не решаются алгоритмами полиномиальной сложности (речь идет о некоторых классах NP-полных задач)). О них можно почитать в широко известной и доступной в Интернете книге Гэри и Джонсона. Все они обладают одним замечательным свойством: с помощью полиномиальных по сложности алгоритмов сводятся к одной задаче «Выполнимость КНФ» в булевом базисе. Для этой задачи даже проводятся соревнования по скорости решения. Все известные алгоритмы их решения не выходят за пределы неконструктивной математики. Хотелось бы знать, как конструктивная математика может помочь в решении этой проблемы, т.е. найти общий полиномиальный алгоритм решения этой задачи или доказать, что такой алгоритм невозможен?
Интересно, что в теоретическом обосновании проблем, связанных с вычислительной сложностью, часто используется машина Тьюринга. Та же машина используется при определении понятия «вычислимость». Только вот почему-то эта машина, насколько мне известно, не используется в алгоритмах решения NP-полных задач и в ЭВМ, которые решают эти задачи.
Я этим делом когда-то давно занимался, даже придумал новый класс полиномиально решаемых задач «Выполнимость КНФ» .
Там, кстати в алгоритме решения использовалось мое детище: алгебра кортежей, которая основана на ругаемой тут многими алгебре множеств. Даже сделал программу, которая сравнительно быстро решала эти задачи. Недавно захотел с этой программой поучаствовать в соревнованиях, но оказалось, что моя программа не работает в новых Windows. Хотел ее переделать, но не вышло - грамотности не хватило. С алгоритмами бы справился, а вот с интерфейсом никак. Учиться поздно, да и некогда.
Тогда я просто даю команду инвертировать вектор. Получаю
Зависание, если память защищена мьютексом.
Что угодно, если память в это время менялась другим потоком.
Перезапуск, если другой поток успел изменить память раньше.
Прерывание, если данные по любой причине были выгружены из памяти.
Неконсистентность, если где либо была ссылка на исходные данные.
Падение программы, если закончился стек.
В постановке задачи я предполагал, что существует какое-то разделение труда между разработчиком алгоритмов и системным программистом. Или я отстал от жизни?
А Вы, наверное, обиделись на меня и решили увести разговор в сторону от основной темы. Ну что ж, неплохо придумано! А я приношу извинения за свое резковатое и не совсем справедливое суждение.
Добро пожаловать в мир многопоточных алгоритмов с ограниченным объёмом ресурсов.
Да куда уж мне в этот мир с моими ограниченными знаниями!
Ваша статья (https://page.hyoo.ru/#!=ixy44o_3oga48 ) мне понравилась. Кое о чем я бы поспорил, но вот с Вашей трактовкой ограниченности классической логики согласен. Только хотел бы напомнить, что с помощью этой логики получено немало замечательных результатов, без которых невозможно представить математику. Предлагаю пообщаться за пределами этой тусовки.
Тогда я просто даю команду инвертировать вектор. Получаю 0101. А если мне нужно вычислить дополнение дополнения S? Тогда непонятно что делать: то ли инвертировать вновь полученный вектор, то ли искать конструктивного математика и просить помощи у него?
Покажите, что инверсия битового вектора эквивалентна отрицанию в исчислении высказываний.
Но это, впрочем, ерунда, и я могу дать вам фору: с инверсией одного бита ваш пример будет более очевиден, и я понимаю, о чём вы говорите. Но проблема вашего примера в том, что вы берёте один частный случай, когда (A → ⊥) → ⊥ эквивалентно A для одного конкретного A, и зачем-то делаете вывод, что это работает для всех A. Мне очень стыдно такое говорить, потому что это выглядит как неуважение к собеседнику, особенно в его же статье про основания математики, но так делать нельзя.
В конструктивной математике, например, есть разрешимые предикаты (в частности, равенство двух битов разрешимо), и для такого предиката двойное отрицание действительно можно снять. Но для любого предиката его снимать нельзя, и именно это отличает классическую математику от конструктивной (я тут, конечно, абьюжу терминологию, немного смешивая предикаты и высказывания, но кто не понял, тот поймёт).
Раз вы там на Гольдблатта ссылались, то я могу и топосами изъясниться: в Sub(1) объединение любого элемента и его отрицания будет равно как подобъект id_1 только в булевых (кек) топосах, где алгебра подобъектов реализует булеву алгебру, но это не значит, что в любом небулевом топосе ( с более общей heyting algebra) объединение любых подобъектов и их отрицаний всегда не id_1.
Хотелось бы знать, как конструктивная математика может помочь в решении этой проблемы, т.е. найти общий полиномиальный алгоритм решения этой задачи или доказать, что такой алгоритм невозможен?
Это какие-то аргументы уровня «эти ваши гудронные кавайдеры на хлеб не намажешь, не нужно!» Не все задачи ограничиваются мазаньем на хлеб, равно как и решением одной конкретной NP-полной задачи, хотя теория descriptive complexity, возможно, могла бы на что-то намекнуть, но я про неё знаю только то, что она существует.
Ну и не могу воздержаться от ремарки, что видеть такие аргументы в статье вокруг оснований математики, в которой тоже и на хлеб ничего не мажется, и NP-полные задачи не решаются — это сочно.
Del
Закон парадокса в логике и математике