Господа, читаю у Гудстейна в «Математической логике» о многих неразрешенных проблемах математики, включая утверждение Ферма, ныне благополучно доказанное, и утверждение Гольдбаха, недоказанное поныне. В примечаниях редактор С. А. Яновская утверждает, что а) оба этих утверждения обладают тем свойством, что, если удастся доказать их неразрешимость (без уточнения формальных рамок, в которых суждение неразрешимо), то тем самым будет доказана их истинность; б) доказательство их неразрешимости невозможно в силу того, что это и означает их доказательство. Аналогично, у Успенского в «Апологии математики» читаю доказательство невозможности доказательства неразрешимости утверждения Ферма (без уточнения формальной системы, в которой такое доказательство невозможно, потому что книга популярная). У меня вопрос: почему доказательство невозможности опровергнуть некоторое утверждение в конкретной формальной системе (типа первопорядковой арифметики Пеано), если данное суждение в указанном выше смысле «если неразрешимо, то истинно», а доказательство ложности утверждения в данной формальной системе сводится к предъявлению индивидов, фальсифицирующих данное утверждение, не приравнивается к доказательству этого утверждения?

GD Star Rating
loading...

13 Responses to Господа, читаю у Гудстейна в «Математической логике» о многих неразрешенных проблемах математики, включая утверждение Ферма, ныне благополучно доказанное, и утверждение Гольдбаха, недоказанное поныне.

  1. NayRU:

    Я имею в виду, что мы легко можем убедиться в том, что отрицание утверждения Ферма не является теоремой первопорядковой арифметики Пеано. Далее, утверждение Ферма если неразрешимо, то истинно. Его отрицание недоказуемо. Остаются два варианта: либо доказуемо его утверждение, либо доказуемо, что недоказуемо не только отрицание данного утверждения, но и само утверждение, то есть утверждение неразрешимо. В первом случае, утверждение Ферма истинно в силу семантической непротиворечивости арифметики Пеано, во втором случае, оно истинно в силу своей неразрешимости. Что мешает добавить к пеановской арифметике такую схему рассуждений, чтобы все утверждения, которые «если неразрешимы, то истинны», и при этом недоказуемо их отрицание, смогли бы стать теоремами системы? Я контрпримеров пока не могу придумать.

  2. NayRU:

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

  3. Dotunes:

    Вот, кстати, про Яновскую:
    http://pustoj-zhurnal.livejournal.com/37
    http://pustoj-zhurnal.livejournal.com/37

    Это к тому, что я в посте ничего не понял, но сообщаю о том, что Юрий Неретин (пустой_журнал) пишет всякую интересную математическую публицистику и всякое ещё про математику.

  4. NayRU:

    Дело не в Яновской. Она в цитируемом мной фрагменте, видимо, вторит мыслям Литтлвуда, распространенным далее Гудстейном и прочими. У меня вопрос конкретный — почему некая схема рассуждений не может считаться правильной с точки зрения логики? Ведь схеме математической индукции все верят. А о подобной схеме я не встречал мыслей, возможно, я не прав.

  5. NayRU:

    Либо здесь недостаточно широкая научная аудитория, чтобы понять о чем речь, либо мне остается ждать… Возможно, вечно..

  6. Peein:

    Поясни, как доказывается (например для теоремы Ферма) утверждение «если удастся доказать их неразрешимость (без уточнения формальных рамок, в которых суждение неразрешимо), то тем самым будет доказана их истинность».

    Давай я тебе задам какую-нибудь тривиальнейшую формальную систему, в которой нельзя будет доказать теорему Ферма (например хотя бы потому, что в придуманной мной формальной системе нет вообще правил вывода, таким образом в ней невозможно доказать ничего).

    С какой стати вдруг окажется, что в этой системе (или в какой-то другой?) теорема Ферма выводима? Или у тебя она аж сразу истинной в любых интерпретациях станет?

  7. NayRU:

    Докажу для совсем простого и ложного утверждения, гыы, это мое последнее достижение в науке. Утверждение следующее: всякое нечетное число — простое. Допустим, мы доказали, что данное утверждение неразрешимо, то есть что невозможно ни доказать его, ни опровергнуть (невозможность здесь означает невозможность сделать это никакими средствами, поэтому и не уточняется, о какой именно формальной системе идет речь — в любой системе невозможно). Допустим также, что наше утверждение ложно. Формулировка его такова, что, если оно ложно, что и имеет место в действительности, то должно существовать число, являющееся нечетным и не являющееся простым. Поскольку мы допустили ложность суждения, такое число должно существовать. Но указание этого конкретного числа, например, числа 9, есть способ опровержения данного утверждения. Следовательно, данное утверждение не является неразрешимым, поскольку даже, если бы первое фальсифицирующее его число было очень большим, мы все равно могли бы его рано или поздно найти и разрешить утверждение. Мы пришли к противоречию, следовательно, утверждение не может быть ложным. Тогда единственный вариант заключается в том, что суждение истинно, но и этот вариант невозможен, поскольку в этом случае вышеприведенный текст становится доказательством истинности утверждения, а утверждение неразрешимо. Следовательно, доказать неразрешимость этого утверждения невозможно. Аналогично можно рассуждать и для утверждения Ферма и вообще целой горы теоретико-числовых утверждений.

    Так вот, тривиальнейшая формальная система не подойдет. В ней должна быть возможность выводить из наличия в модели фальсифицирующих суждение индивидов отрицание этого суждения. Как это можно и можно ли сделать, а, если нельзя, то почему, я себе очень слабо представляю, об этом, собственно, и был вопрос. Кстати, в системе без правил вывода теоремами будут все аксиомы и подстановки в них, если мы работаем со схемами аксиом, а это уже немало, то есть доказуемо в ней будет довольно много что. В качестве примера тривиальной, я бы брал систему с правилами вывода, но без аксиом и схем. Но и такие системы не совсем тривиальны. FDE не имеет аксиом, может, можно к ней и кванторы присобачить, и арифметику построить попытаться.

    В том и дело, что меня интересует ситуация, когда теорема невыводима, как и ее отрицание, но это может нам дать повод на основании некоторой схемы рассуждений или, возможно, метода доказательства, отличного от средств данной формальной системы, в которой суждение неразрешимо, сделать вывод о ее содержательной истинности, например, в нормальной модели для первопорядковой арифметики.

  8. Peein:

    Ты чего-то напутал. Твой пример говорит лишь о том, что выбранное тобой утверждение (как и многие другие) должно быть доказуемо (или опровергаемо) в конструктивной логике. И ты доказал это. ОК. Но это далеко не то же самое, что и
    «если удастся доказать неразрешимость, то будет доказана истинность».

  9. NayRU:

    Мне стало многое (элементарное) понятно с тех пор, как я написал пост. Там глупость есть, и еще одна глупость, ну да вы заметили. Но меня продолжает волновать вопрос. Возможно, невнятный, но попробую задать еще раз. Есть ли шанс, что доказательство подобных суждений, типа вышеназванных, удастся свести к некоторому алгоритму? Все проблемы теории чисел, которые доступны моему пониманию, странным образом обладают одним и тем же свойством — они «если неразрешимы, то истинны» (или назовите это иначе, но это их объединяет). Гипотезу о нулях дзета-функции в силу нетривиальности ее формулировки для моего образования не проверял. Остальные открытые и закрытые проблемы, кажется, все оттуда. Это, во-первых, кажется позволяет их отделить от проблем, типа континуум-гипотезы, во-вторых, предположить, что возможное доказательство их независимости от некоторых аксиоматических систем может означать нечто большее, нежели просто независимость.

  10. Peein:

    Еще раз, выражение «если неразрешимы, то истинны» кажется мне каким-то бессмысленным и очень коряво сформулированным. Если ты не можешь вывести доказательство какого-то утверждения, это не означает, что оно обязательно истинно. В частности, если ты не можешь доказать, что «не найдется какое-то там число», это абсолютно не значит, что число обязано найтись.

    Доказуемость и истинность — разные вещи. Любая интересная теория неполна и может содержать истинные, но недоказуемые утверждения, некоторые из которых вполне могут быть в форме «не найдется …».

  11. NayRU:

    Арифметика Пресбургера, вроде, полна. Она же разрешима. В ней только одна операция (либо только сложение, либо только умножение), поэтому, видимо, нужно немного переопределить кое-какие вещи, чтобы выражать в ней нужные утверждения, не рассыпав полноту и разрешимость, но может сработать. Я это к тому, что не любая интересная теория неполна. Неполнота всего интересного — это, как мне кажется, иллюзия, вызванная крахом программы Гильберта из-за теорем Геделя, сохраняющаяся по сей день. Мне кажется, что это слегка неправильно, потому что уже очень много лет прошло с тех пор, и мысли должны бы немного дальше подуматься.

  12. NayRU:

    Я это о том, что один мой знакомый хотел решить P-NP-проблему. Он начал с поисков хороших разрешимых фрагментов первопорядковой логики. Выяснилось, что эти фрагменты в основном являются расширениями модального фрагмента, который позволяет выразить чуть больше чем ничего в арифметике. И расширения сильно ситуацию не улучшают. Но есть же разрешимые арифметики, даже полные есть. Надо просто немножко нестандартно с ними поработать, возможно, вдруг что-то и получится. А знакомый сейчас забил, занялся тупым компьютер-саенсом, может, он и здесь есть.

  13. Peein:

    Ну да. Еще Булева арифметика полна, или вообще любая конечная теория. В случае с конечной теорией даже как бы очевидно, что если ты продемонстрируешь невыводимость утверждения, то оно обязано быть верным, т.к. доказательство невыводимости в рамках такой теории — тупо полный перебор. Только фигня в том, что полный перебор в случае конечной тоерии — это не столь доказательство «невыводимости», сколь просто доказательство обратного утверждения. И никакой тебе мистики и чудесных правил.

    Всякие Булевы алгебры и урезанные арифметики как раз «неинтересные» теории. Интересно — это то, где можно формулировать разные общего плана рекурсивные утверждения (например, хотя бы утверждения затрагивающие понятие «выводимости» или «невыводимости»). Но как только твоя теория способна рассуждать о «невыводимости», например, в ней тут же появляется возможность сформулировать утверждение «Это утверждение невыводимо». И всё.

Добавить комментарий