Xaositect-у:
Цитата:
Эта функция может быть написана на рассматриваемом языке, и именно поэтому является эффективной
В одном из постов я пояснил, что функция перечисляет все алгоритмы некоторой фиксированной теории. Следовательно, не принадлежит этой теории. Я могу использовать в создании этой функции другой язык.
Цитата:
Не любая, а рекурсивно-перечислимая формальная теория. в которой доказуемы все аксиомы арифметики Пеано
Я нигде и не утверждал, что это любая теория. Ясно, что она должна содержать ту, о которой вы говорите.
Цитата:
Учение", "научение"
"Математика" с греческого переводится как "знание", см. энциклопедию.
Цитата:
Если Вы хотите привести контрпример, то давайте рассмотрим конкретное доказательство, например, приведенное параграфе 1 главы III учебника Колмогорова и Драгалина "Математическая логика. Дополнительные главы":
Информацию понял. Буду думать, что ответить. Может быть вы приведёте хотя бы канву рассуждения, которое я по Вашему мнению должен опроовергнуть. Вдруг я с таким рассуждением соглашусь.
Добавлено спустя 12 минут 28 секунд:маткиб-у
Цитата:
Только в этом случае получается, что все ваши основные рассуждения проводятся для противоречивой теории! Тогда зачем это всё нужно? Итак ясно, что в противоречивой теории выводится абсолютно всё. Почему тогда вы утверждаете, что Гёдель не прав?
Именно так, как вы пишите. Гёдель формулирует некоторую теорию, которую неоправдано отождествляет с классической арифметикой. Именно такая арифметика Гёделя мною имеется ввиду. Именно она противоречива, так как противоречит фундаментальной логической аксиоме, если последняя введена в арифметику. Если такая аксиома не считается введённой в арифметику Гёделя, то мы получаем логически усечённую теорию арифметики, и не можем говорить о ней как о классической теории арифметики. Т.е. не можем переносить с усечённой теории выводы, которые сделал Гёдель и отстаивают его последователи, на классическую арифметику.
Вообще же, я ввожу специальный пост №2, где детально разъясняются заданные Вами и другими участниками вопросы.
Добавлено спустя 15 минут 45 секунд:
ПОСТ №2
Xaositect-у, маткиб-у и другим.
маткиб-у: посмотрите ещё раз ПОСТ №1, там содержится доказательство (содержательное, в первом приближении) средствами теории арифметики, которую Гёдель отождествляет со своей теорией, того, что формула Ф недоказуема в такой арифметике. При доказательстве используется аксиома, что из доказуемости формул должна вытекать их истинность. Эта аксиома должна приниматься любой естественной теорией арифметики.
§5
Дам более детальные выкладки, чтобы ответить на полученные вопросы, и на возможное возражение, что «утверждение о недоказуемости гёделевой формулы доказуемо только в метатеории, поэтому, не приводит к противоречию». Для того чтобы быть точным, уточняю «исходные данные».
T – теория, в которой даются все нижеследующие определения (метатеория).
S – теория, интерпретируемая средствами теории T. Это означает, что в T: определяются отношения и функторы для теории S; доказываются теоремы, которые суть – аксиомы теории S.
В результате, средствами T даётся определение, что означает «формула принадлежит S». Теория здесь отождествляется с множеством формул, функторов и т.п., которые в ней могут быть сформулированы или заданы, и тем самым, содержатся. Если Ж – формула, то «(Ж принадлежит S) влечёт (Ж принадлежит T)», обратная импликация, вообще говоря, неверна. Если M – теория, Ж – формула, то считаем, что выражение «Ж есть M-формула» означает то же, что и «Ж принадлежит M».
В качестве S формулируем арифметику, называемую здесь GA – «арифметикой Гёделя». В теории S так или иначе можно говорить: о доказуемости S-формул, о гёделевых номерах S-формул, о гёделевых номерах цепочек S-формул, о гёделевых номерах доказательств. Для этого, средствами T определён оператор Prf так, что если Ж есть S-формула, то Prf(Ж) – так же S-формула, означающая, что «Ж доказуема средствами S». При этом, «гед.ном.(Ж)» означает гёделев номер формулы Ж. Если W – цепочка S-формул, то «гёд.ном.(W)» означает гёделев номер цепочки W.
В качестве T выберем теорию классической арифметики CA. В CA классическим способом определяются формулы и функторы, которые можно подставлять друг в друга. Считаем, что в CA невозможно говорить о доказуемости CA-формул, хотя это требование не обязательно выполнять, при соответствующих аксиомах.
В качестве T может быть выбрана и более сильная теория, например, такая, в которой можно говорить о знаках теории CA как о предметах теории T.
Арифметику Пеано обозначим PA. Эту теорию можно выбрать в качестве теории T, а можно отождествить с S = GA, как это делается в некоторых математических работах. Мы рассмотрим оба случая. В последнем случае, обозначение PA не справедливо, так как Пеано рассматривал свою арифметику совершенно в другом контексте. Естественнее считать, что PA = CA.
В любом из указанных случаев, теорию S формулируем как теорию, в которой по интерпретации речь идёт только о числах. Т.е. с формальной точки зрения, «с точки зрения теории T», «с точки зрения формального понимания теории S» разговор идёт только о числах. Но с точки зрения содержательной интерпретации, «с точки зрения содержательного понимания теории S», мы, например, можем рассматривать функторы не только от чисел, но и от формул.
§6
S-вывод формулы Ж – это цепочка S-формул, являющаяся выводом формулы Ж (т.е. выводом в теории T) из посылок, которые суть S-формулы.
S-теорема – это такая формула, которая стоит в конце хотя бы одного S-вывода из аксиом теории S (S-аксиом). S-доказательство или безусловный S-вывод – это такой S-вывод, посылки которого суть S-теоремы. Если S-вывод не является безусловным, то он является условным S-выводом.
Аналогично определяется T-вывод, T-доказательство и т.п. Каждый S-вывод является одновременно T-выводом. Обратное не верно. Каждая S-теорема есть T-теорема, но не обратное.
В теории S гёделевы номера формул даются только S-формулам, гёделевы номера цепочек формул, выводов и доказательств даются только цепочкам S-формул, только S-выводам и только S-доказательствам соответственно. Функтор, ставящий в соответствие каждой S-формуле её гёделев номер, принадлежит S. Аналогично, принадлежат S функторы, перечисляющие цепочки формул, выводы и доказательства.
В теории S вводится логическое правило вывода: если вывод формулы Ж есть S-доказательство, то мы можем отсюда заключить, что верна формула Prf(Ж).
Средствами T в теории S определяется множество формул «верных в S». Каждая числовая формула из T считается либо «верной в T», либо «неверной в T», т.е. попросту верной ли или неверной, вне зависимости от её доказуемости в T. Предполагается, что так или иначе возможно верифицировать каждую формулу. Это интуитивное требование (аксиома) классической логики. Формула теории S считается «верной в S», если эта формула верна в T, т.е., если попросту она верна. В частности, каждая S-теорема считается «верной в S». Однако, в смысле данных определений, если формула верна в S, то это не означает, что она S-теорема, т.е., что она безусловно выводима из аксиом теории S.
Замечание. Если Ж есть S-формула, полученная в результате вывода, среди посылок которого содержится формула не принадлежащая S, то мы не можем отсюда заключить средствами теории S, что Prf(Ж) верна, даже если в T формула доказуема. Таким образом, мы не сможем средствами S установить Prf(Ж) как теорему теории S. Этим, в частности, множество T-выводов отличается от множества S-выводов. Мало того, если Ж получена в результате S-вывода из теорем теории T, но хотя бы одна из посылок не является теоремой теории S (такая посылка может быть недоказуемой, но верной в S формулой), то мы не можем применить к формуле Ж определённое выше правило вывода и заключить средствами теории S, что Prf(Ж) верна, т.е. не можем установить Prf(Ж) как теорему теории S.
§7
Для вывода противоречия в теории S нам потребуются два утверждения.
1. Какова бы ни была S-формула Ж, средствами теории S из доказуемости Ж можно извлечь, что Ж верна. Т.е., в S верна аксиома: «Prf(Ж) влечёт Ж» (схема аксиом). Эта аксиома может быть заменена на некоторое эквивалентное правило вывода.
2. Существует формула Ф из S такая, что средствами теории S доказуемо, что «Ф равносильна формуле неPrf(Ф)».
Утверждение 2 доказывают, предполагая, что завершено определение предиката Prf. Пусть sb(n, m) – гёделев номер формулы, полученной подстановкой номера m вместо свободной переменной в такую формулу с одной свободной переменной, гёделев номер которой есть n. Функтор sb всегда определим в S, посредством аксиом S. Пусть U – S-формула, z – единственная свободная переменная этой формулы. Рассмотрим формулу U(sb(x, x)), где x – свободная переменная. Пусть, гёд.ном.(U(sb(x, x))) = L. Определим в качестве V формулу U(sb(L, L)). По определению sb: гёд.ном.(V) = гёд.ном.(U(sb(L, L))) = sb(L, L). Следовательно, V равносильна U(sb(L, L)) равносильна U(гёд.ном.(V)). В теории S определён предикат Pr(z) означающий: «доказуема формула с гёделевым номером z». Тогда, если X – S-формула, то Prf(X) введём как S-формулу Pr(гёд.ном.(X)). В качестве Ф возьмём формулу V, для которой U есть неPr, ч т.д.
Выведем противоречие, предполагая, что аксиома, указанная в 1, есть S-теорема. Действительно. Предположим, рассуждая в S, что Ф доказуема средствами S, т.е. в S предположим, что верно Prf(Ф). По указанной аксиоме получаем, что в S верна Ф. Тогда, из утверждения 2, (таким образом, средствами S) извлекаем, что верно неPrf(Ф). Это противоречие. Следовательно, предположение о доказуемости Ф неверно. Следовательно, (это вывод из аксиом S) верно неPrf(Ф). Но тогда, по утверждению, указанному в 2, верна Ф. Это S-доказательство формулы Ф. Применяя правило вывода из §6, получаем, что верна Prf(Ф). Снова противоречие.
Если аксиома, указанная в 1, не является теоремой S, то она должна быть хотя бы теоремой теории T (иначе, по крайней мере, простым путём, в T недоказуема недоказумость Ф, т.е. не установима собственно «теорема Гёделя», см. далее), причём эта теорема одновременно есть S-формула. Возможно так же, что в S не допустимы «рассуждения от противного». Тогда, уже средствами T, можно снова повторить приведённый выше вывод и придти к утверждению «о безусловной недоказуемости формулы Ф средствами S» – в качестве теоремы теории T, но не как S-теоремы. Из недоказуемости Ф в S извлечём истинность Ф (в силу 2). Этим установим истинность Ф S-выводом, но в силу замечания §6, не можем перейти к утверждению о верности Prf(Ф). Т.е. устанавливаем истинность Ф и одновременно не приходим к противоречию. Интересно, что при полной расшифровке, формула Ф даже графически совпадает с формулой неPrf(Ф) и выражает средствами T «недоказуемость» Ф в S.
Из такого рода «недоказуемости» формул Ф и неФ в S делают вывод (если T непротиворечива), что теория S непротиворечива (иначе все формулы выводимы) и неполна (обе формулы Ф и неФ не выводимы в S). Мало того, делают вывод, что «достаточно богатая непротиворечивая теория» должна содержать S, а потому, такая теория должна быть неполна. Поэтому, думают, что «все достаточно богатые теории или неполны, или непротиворечивы».
§8
Однако, если мы не признаём утверждение «Prf(Ж) влечёт Ж» в качестве аксиомы (схемы аксиом) теории S, или не допускаем «рассуждения от противного», то и не можем говорить о том, что доказали классическую не выводимость Ф. В самом деле, доказана не выводимость Ф в теории S, которая почему-то отождествляется с PA, но в которой, например, запрещено извлекать из доказуемости формул их истинность. Это означает, что, отрицая аксиому «Prf(Ж) влечёт Ж», мы рассматриваем усечённую, неклассическую «доказуемость». Относительно такой «доказуемости» и устанавливаем «недоказуемость формулы Ф». Получаем, что в S потеряны логические операции, ради которых создавалась S, и которыми располагает любая естественная теория. Таким образом, в содержательной интерпретации гёделева арифметика либо логически ограничена, либо противоречива.
Если считать, что T совпадает с PA, то выводы не изменятся. Чем бы ни были T и S, выводим или противоречие в S, или логическую ограниченность S.
Утверждая аксиому «Prf(Ж) влечёт Ж», приходим к отрицанию «Ф равносильна неPrf(Ф)». Т.е. ставим под сомнение гёделево определение «доказуемости» Prf, которое непредикативно и противоречиво.
В итоге, «первая теорема о неполноте», при содержательной интерпретации теории S, не может претендовать на доказанность. Так же и «при арифметической интерпретации теоремы», т.е. тогда, когда считается, что Ф чисто арифметическая формула, и отрицанию аксиомы «Prf(Ж) влечёт Ж» придаётся арифметический, а не логический смысл. В самом деле, Ф не входит в множество формул теории S, которые интерпретируются как высказывания обычной арифметики, поскольку, эти последние не используют предикат Prf, и не образуют всей S. Таким образом, в данной интерпретации Ф находится вне множества формул классической арифметики. Следовательно, гёделев вывод не касается классических формул арифметики, не влечёт того, что в достаточно развитой классической арифметике есть неразрешимая формула.
С другой стороны, «в арифметическом смысле», который приписывает формуле Ф теория T, Ф может быть формулой классической арифметики тогда, когда классическая арифметика отождествляется с T. Но Ф классически доказуема в метатеории T (при условии отрицания аксиомы «Prf(Ж) влечёт Ж» в S; если эта аксиома определена в S, то T противоречива).
§9
Нет необходимости использовать логику, искусственно ограничивающую способы доказательств, всегда можно перейти к определениям, так или иначе тривиально разрешающим Ф. Мы так же можем настаивать на аксиоме «Prf(Ж) влечёт Ж», которая порождает множество формул, не содержащее «гёделеву формулу». Почему нельзя использовать подобные переопределения всякий раз, когда предъявлена «неразрешимая гёделева формула»? Почему теория с аксиомой «Prf(Ж) влечёт Ж» не может быть полной? Новые определения, кроме «разрешения Ф», не уменьшат «богатства» S. С другой стороны, некоторые из таких определений вернут всё в рамки классической логики. Иными словами, вообще нет проблемы «разрешения формулы Ф» в плане практического знания, т.е. «узнавания, что же на самом деле». Если не выдумывать причины, по которым достаточно тривиальная формула неразрешима. Но почему именно эта формула? С таким же успехом, можно придумать причину, по которой не доказуемо, например, что 5 простое число.
Добавлено спустя 11 минут 42 секунды:
AD-у:
Так как поле Ваших вопросов обширно. Прошу конкретизировать.