Корень всех проблем

[Munin]

bin в сообщении #621278 писал(а):

pointless topology не равно теории графов? у графов нет точек (в геометрическом смысле) и сплошная топология?

Нет, совсем не равно, я так понял, там обобщается общая топология (которая обсуждает открытые множества точек), а не алгебраическая (которая обсуждает всякие дырки и заплетённости). Кстати, топология графов - раздел алгебраической топологии, Прасолов "Элементы комбинаторной и дифференциальной топологии" 1-й том двухтомной серии.

epros в сообщении #621307 писал(а):

Это называется мета-метатеорией, каковой в большинстве случаев может быть практически любая достаточно сильная теория. А хотя бы и арифметика

Извините, меня не отговорки интересуют, а конкретные результаты, публикации. Если всё так тривиально, как вы говорите - то главы в учебниках.

epros в сообщении #621307 писал(а):

Но вообще-то реально такая степень формализации никому не нужна.

Отговорка, недостойная математика. И Профессор Снэйп, и вы только приводите оправдания, чтобы этим не заниматься. Когда это развитие математики останавливалось отсутствием практических заказов?

epros в сообщении #621307 писал(а):

Обычно сначала возникает некая слабо формализованная теория, потом она формализуется...

Сначала возникает интерес. Есть остро недоразработанная область математики. И ноль активности! Что за табу?

epros в сообщении #621307 писал(а):

"При условии, что принимается закон исключённого третьего" - устроит?

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

epros в сообщении #621385 писал(а):

говоря: "Из такой-то системы аксиом в рамках такой-то логики можно получить такие-то следствия", - Вы тоже изрекаете нечто, претендующее на "истинность".

Ага-а-а!.. :-)

Ну и как сей замкнутый круг предлагают разбивать конструктивисты? "Истинно только то, что мы успеем произнести за конечное время"? Но здесь не хватает детальки "истинно всё то...".

epros в сообщении #621385 писал(а):

СведЕние математики к финитной игре со значками тоже не есть отказ от истинности: Ведь мы всё равно будем какие-то комбинации значков оценивать как "истинные утверждения".

Нет, мы некоторые ходы в игре будем оценивать как сделанные по правилам. Логично, что это можно будет говорить только о явно сделанных ходах. Начинаю немного понимать "метафизику" конструктивистов.

epros в сообщении #621385 писал(а):

Есть ли "неподтверждаемые истины"? Может и есть, но каков смысл их декларировать?

Думаю, здесь математики представляли себе ситуацию наподобие физики (или любой другой естественной науки): экспериментальная проверка может обнаружить в мироздании Австралию, несмотря на то, что до экспериментальной проверки мы доказать её существование никак не могли. Так что существование Австралии можно декларировать, а иначе её истинность ввести нельзя.

Получается философский вопрос. С физическим миром всё понятно, но математики исследуют идеальный мир. И вот оказывается, что классики и конструктивисты исследуют разные миры. В классическом бывают "Австралии", которые неожиданно обнаруживаются за углом, а в конструктивистском - только то, что видно из начальной точки прямым взглядом.

[Профессор Снэйп]

Munin в сообщении #621455 писал(а):

И вот оказывается, что классики и конструктивисты исследуют разные миры. В классическом бывают "Австралии", которые неожиданно обнаруживаются за углом, а в конструктивистском - только то, что видно из начальной точки прямым взглядом.

Наверное, можно и так сказать.

У конструктивистов странный мир. Иногда говорят, что у них действительная прямая имеет счётную мощность, но это чепуха, тратить время на разоблачение которой мне сейчас лень. Гораздо интересней другое... у них все функции из $\mathbb{R}$ в $\mathbb{R}$ непрерывны! В смысле что любая непрерывна, разрывных просто не существует

-- Чт сен 20, 2012 20:46:42 --

Вообще, доказательство в математике - разновидность гипноза. Человеческий мозг устроен так, что определённым образом выстроенная последовательность символов алфавита может убедить его в истинности самых невероятных утверждений. И некоторые этим беззастенчиво пользуются...

А у конструктивистов - у них мозг более гипностойкий

[epros]

Munin в сообщении #621455 писал(а):

Извините, меня не отговорки интересуют, а конкретные результаты, публикации. Если всё так тривиально, как вы говорите - то главы в учебниках.

Какие отговорки? А какой конкретный ответ Вы надеетесь получить на такой общий вопрос? Ну, полазьте по теме «reverse mathematics» — это огромный раздел математики, посвящённый именно копанию в основаниях, и в том числе в вопросах о том, кто чьей метатеорией может быть. Насколько я знаю, в качестве базовой системы обычно используется $RCA_0$, коя изоморфна примитивно-рекурсивной арифметике. По мере добавления в эту систему тех или иных аксиом, получают различные более содержательные системы.

Munin в сообщении #621455 писал(а):

Сначала возникает интерес. Есть остро недоразработанная область математики. И ноль активности! Что за табу?

Не понял, что недоработано, почему табу?

Munin в сообщении #621455 писал(а):

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

Вы о чём? Как только принимается закон исключённого третьего, так все конструктивные методы заканчиваются и мы оказываемся в области классической логики.

Munin в сообщении #621455 писал(а):

Ну и как сей замкнутый круг предлагают разбивать конструктивисты? "Истинно только то, что мы успеем произнести за конечное время"? Но здесь не хватает детальки "истинно всё то...".

Да так же, как классическая математика: нужно принять некую аксиоматику.

Munin в сообщении #621455 писал(а):

Нет, мы некоторые ходы в игре будем оценивать как сделанные по правилам. Логично, что это можно будет говорить только о явно сделанных ходах.

Вообще-то «сделанное по правилам» — это и есть «правильное», то бишь истинное.

Munin в сообщении #621455 писал(а):

Начинаю немного понимать "метафизику" конструктивистов.

Это не метафизика конструктивистов, так устроена любая логика.

Munin в сообщении #621455 писал(а):

экспериментальная проверка может обнаружить в мироздании Австралию, несмотря на то, что до экспериментальной проверки мы доказать её существование никак не могли. Так что существование Австралии можно декларировать, а иначе её истинность ввести нельзя.

Суть конструктивного подхода в том, что существование Австралии можно НЕ декларировать до тех, пор, пока она не обнаружена явно. Закон исключённого третьего ведь не поможет нам обнаружить Австралию. Но при построении модели мира классическому логику придётся выбрать один из двух вариантов ответа про Австралию, реально ничего о ней не зная.

[Munin]

epros
Всё-таки, извините, с Профессором Снэйпом приятней было беседовать, он не срывался в огрызательства. Про reverse mathematics спасибо, но лазить не буду. В остальном вы меня не поняли.

[bin]

Глубокоуважаемые господа логики!
Разрешите, возможно, наивно-еретический с точки зрения фундаментальной логики вопрос: как с законом исключения третьего обстоит дело в вычислительной технике? - Обычно вроде там все бинарно - либо true, либо false и третьего не дано (я про стандартные подходы). Однако в некоторых классических компиляторах Паскаля, нпр., наряду с Булевыми true и false предусматривалось значение undefined: при загрузке проги все переменные приобретали значение undefined (технически ячейки заполнялись, нпр., единицами $FFFF...). Такая техника позволяет легко ловить многие типовые баги. Можно также написать оператор в проге: if undefined (myVar) then ... Кроме того, подобная техника зарекомендовала себя для условной компиляции (и не только в Паскале). Может, и в фундаментальной науке (логике) закон исключения третьего не столь большая проблема, если не доводить до абсурда? Такой вот позитивизм...

[Munin]

http://en.wikipedia.org/wiki/Heyting_algebra#Examples посмотрите третий пример, трёхзначная алгебра и таблицы истинности её операций.

[bin]

Munin в сообщении #621629 писал(а):

http://en.wikipedia.org/wiki/Heyting_algebra#Examples посмотрите третий пример, трёхзначная алгебра и таблицы истинности её операций.

Ok! Спасибо. Но м.б. будут и личные комменты?

[epros]

bin в сообщении #621616 писал(а):

Разрешите, возможно, наивно-еретический с точки зрения фундаментальной логики вопрос: как с законом исключения третьего обстоит дело в вычислительной технике? - Обычно вроде там все бинарно - либо true, либо false и третьего не дано (я про стандартные подходы). Однако в некоторых классических компиляторах Паскаля, нпр., наряду с Булевыми true и false предусматривалось значение undefined

Третье, четвёртое и любое конечное количество логических значений не помогут избавиться от общезначимости закона исключённого третьего. А что касается компьютеров, то дело не в том, сколько состояний у элемента, а в том, какие возможны ответы на вопрос: "Останавливается ли алгоритм". Классическая логика отвечает: "Останавливается" или "Не останавливается". Конструктивная логика помимо этого может предполагать и что-нибудь другое, например, что "доступными нам средствами это невозможно установить".

В этом плане на различия между классическим и конструктивным подходами можно взглянуть как на различия в интерпретациях отрицания. Классическая логика приписывает отрицанию "равные права" с утверждением. В конструтивной логике это не так. Здесь отрицание интерпретируется исключительно как сведение утверждения к противоречию, поэтому оно заведомо основано не на "прямых", а на "косвенных" аргументах: т.е. убедительность отрицания зависит от того, к противоречию с чем мы привели утверждение. Поэтому двойное отрицание и рассматривается как нечто более слабое, чем прямое утверждение, т.е. из первого не факт что следует второе.

[Munin]

bin в сообщении #621706 писал(а):

Ok! Спасибо. Но м.б. будут и личные комменты?

Откуда, я сам это пять минут как прочитал! Но вообще, использование boolean в расширительном смысле встречается в программировании нечасто, а проблема инициализации решается во многих языках иначе, не специальным значением, а специальным статусом величины undefined. Навскидку могу порекомендовать познакомиться с Лиспом и Прологом, и с каким-нибудь современным скриптовым языком.

epros в сообщении #621740 писал(а):

Третье, четвёртое и любое конечное количество логических значений не помогут избавиться от общезначимости закона исключённого третьего.

А специально определённые операции $\neg a$ и $a\to b$ - помогут.

epros в сообщении #621740 писал(а):

Конструктивная логика помимо этого может предполагать и что-нибудь другое, например, что "доступными нам средствами это невозможно установить".

Хе, боюсь, вы всё-таки в душе классик, если это "другое" так формулируете :-) Конструктивист бы сказал, что "этого ответа вообще на свете не существует".

[epros]

Munin в сообщении #621846 писал(а):

Конструктивист бы сказал, что "этого ответа вообще на свете не существует".

Нет, конструктивист так сказать не может, ибо утверждение о несуществовании ответа равносильно утверждению противоречия.

[Munin]

А утверждение о невозможности установить? Нет, врёте, вы же сказали только, что "может предполагать и что-нибудь другое, например...", а не что "будет утверждать, что...".

[bin]

epros в сообщении #621740 писал(а):

bin в сообщении #621616 писал(а):

Разрешите, возможно, наивно-еретический с точки зрения фундаментальной логики вопрос: как с законом исключения третьего обстоит дело в вычислительной технике? - Обычно вроде там все бинарно - либо true, либо false и третьего не дано (я про стандартные подходы). Однако в некоторых классических компиляторах Паскаля, нпр., наряду с Булевыми true и false предусматривалось значение undefined

Третье, четвёртое и любое конечное количество логических значений не помогут избавиться от общезначимости закона исключённого третьего. А что касается компьютеров, то дело не в том, сколько состояний у элемента, а в том, какие возможны ответы на вопрос: "Останавливается ли алгоритм". Классическая логика отвечает: "Останавливается" или "Не останавливается". Конструктивная логика помимо этого может предполагать и что-нибудь другое, например, что "доступными нам средствами это невозможно установить".

В этом плане на различия между классическим и конструктивным подходами можно взглянуть как на различия в интерпретациях отрицания. Классическая логика приписывает отрицанию "равные права" с утверждением. В конструтивной логике это не так. Здесь отрицание интерпретируется исключительно как сведение утверждения к противоречию, поэтому оно заведомо основано не на "прямых", а на "косвенных" аргументах: т.е. убедительность отрицания зависит от того, к противоречию с чем мы привели утверждение. Поэтому двойное отрицание и рассматривается как нечто более слабое, чем прямое утверждение, т.е. из первого не факт что следует второе.

Спасибо за очень четкое и лаконичное разъяснение. Сколько могу судить, оно соответствует всему, что я читал по этому вопросу. Не буду поминать спец. издания, а укажу только общий логический справочник - словарь Кондакова. Но в моем вопросе была небольшая ловушка: в тех реализациях Паскаля, о которых я спрашивал, 3х значная логика использовалась очень ограниченно, нпр., для отладки и условной компиляции. А программы при этом обычно работали по классической Булевой алгебре (за исключением, конечно, случаев, когда специально программировалась многозначная, вероятностная и прочие возможные логики). Так вот, повторю свой наивно-еретический вопрос: может, и вне области разработки программ имеет смысл использовать разные логики, при том, что ИМХО в основном (везде, где возможно и оправдано) использовать классическую?

-- Пт сен 21, 2012 22:32:20 --

Munin в сообщении #621846 писал(а):

Навскидку могу порекомендовать познакомиться с Лиспом и Прологом, и с каким-нибудь современным скриптовым языком.

Я знаю принципы этих языков, хотя и не работал в них продолжительное время. Еще можно помянуть язык Eiffel с его методом контрактного программирования. Но я спрашивал не ради языков, а использовал их как пример, где, при соблюдении определенных разумных правил, могут ужиться разные логики (см. мою реплику выше).

[Munin]

bin в сообщении #622089 писал(а):

Но я спрашивал не ради языков, а использовал их как пример, где, при соблюдении определенных разумных правил, могут ужиться разные логики (см. мою реплику выше).

Нет, я думаю, ужиться не могут, а только одна заменит другую.

[bin]

(Оффтоп)

epros в сообщении #621856 писал(а):

Munin в сообщении #621846 писал(а):

Конструктивист бы сказал, что "этого ответа вообще на свете не существует".

Нет, конструктивист так сказать не может, ибо утверждение о несуществовании ответа равносильно утверждению противоречия.

Ох мало у нас на форуме смайликов: хочу смайлик в шляпе с огромными полями, чтобы на такое снять и раскланяться

[Munin]

(Оффтоп)

Всё, мне пора сваливать, я задумался о конструктивистских смайликах...