"Теорема Гёделя" никогда не была доказана

[Someone]

arqady в сообщении #153163 писал(а):

можно хотя бы ссылочку на "Идиотизмы Давидюка" и на "лёгкую" формализацию на этом форуме

Насколько я помню, Давидюк здесь всем участникам дискуссии так надоел и вёл себя столь агрессивно, что его заблокировали, а все его темы удалили. Вряд ли можно считать адекватным человека, который пишет заявления в прокуратуру по поводу того, что ему не нравится рецензия, выданная математическим институтом на его работу. Если Вам интересно, наберите в Google "Давидюк Кантор" и наслаждайтесь.

"Диагональная конструкция Кантора" - это

Утверждение. Если $X\subseteq A$, $f\colon X\to 2^A$ и $Z=\{x\in X:x\notin fx\}$, то $Z\notin fX$.

Доказательство. Множество $2^A$ существует по аксиоме степени, множество $Z$ - по аксиоме выделения.
Предположим, что $Z\in fX$, то есть, существует такое $x_0\in X$, что $fx_0=Z$. Из определения множества $Z$ следует, что для $x\in X$ выполняется $x\in Z\Leftrightarrow x\notin fx$. Подставляя сюда $x=x_0$, получим противоречие: $x_0\in Z\Leftrightarrow x_0\notin fx_0=Z$. Поэтому такого $x_0$ не существует.\qed

Запишите это в каком-нибудь формальном языке ZF, и будет Вам формализация.

[маткиб]

Инт в сообщении #153248 писал(а):

Это именно тот случай, из двух, который рассматриваете Вы. Т.е. противоречия у Вас нет, но тогда, Вы получаете «логически неполноценную теорию арифметики».

Повторяетесь, батенька.
Вы не как не можете поверить в то, что логически полноценных теорий не бывает. Не в формализации Гёделя, а вообще их не бывает в принципе!
[философия]
Степень логической абстракции не ограничена, и в рамках одной теории вы все возможные уровни логической абстракции не запихаете, вот попробуйте! Вообще, уровни логической абстракции не существуют сами по себе, их ещё придумать надо (в это трудно поверить)!
[/философия]
Короче, читать парадоксы теории множеств (несуществование множества всех множеств, множества всех кардиналов, множества всех ординалов).

[naiv1]

маткиб в сообщении #153197 писал(а):

в аксиоматику Пеано можно добавить 2+2=4 и 2+3=5, а от того, что они выводимы из других, они не перестают быть аксиомами.

Тогда как Вы отличите "аксиомы" вида 2+2=4 и 2+3=5, "выводимые из других [аксиом]" от теорем(http://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0) - утверждений, которые тоже выводятся из аксиом?
Утверждение 2+3=3+2 по Вашему - это аксиома или нет?

маткиб в сообщении #153197 писал(а):

Кстати, аксиоматика Пеано не минимальна.

Не можете ли дать ссылку, где это утверждается и/или поясните сами?

[маткиб]

naiv1 в сообщении #153314 писал(а):

Тогда как Вы отличите "аксиомы" вида 2+2=4 и 2+3=5, "выводимые из других [аксиом]" от теорем(http://ru.wikipedia.org/wiki/%D0%A2%D0% ... 0%BC%D0%B0) - утверждений, которые тоже выводятся из аксиом?

Очень просто. Некоторые утверждения являются одновременно аксиомами и теоремами. Точнее, все аксиомы являются теоремами. А что в этом плохого?

naiv1 в сообщении #153314 писал(а):

маткиб в сообщении #153197 писал(а):Кстати, аксиоматика Пеано не минимальна.

Не можете ли дать ссылку, где это утверждается и/или поясните сами?

Ну, например, одна из аксиом (частных случаев схемы индукции выглядит так):
$(0=0)\ \&\ (\forall x)(x=x\rightarrow s(x)=s(x))->(\forall x)(x=x)$.
Эту формулу можно доказать и вообще без индукции.
Но если считать схему индукции (бесконечное множество аксиом) одной аксиомой, то вроде минимальность будет (по крайней мере, известен вариант аксиоматики, для которой доказана минимальность).

[naiv1]

Someone писал(а):

naiv1 в сообщении #153149 писал(а):

можно хотя бы ссылочку на "Идиотизмы Давидюка" и на "лёгкую" формализацию на этом форуме

Опять меня спутали(http://dxdy.ru/post152877.html#152877) . На это раз Someone меня перепутал с arqady.

Вот правильная ссылка на запрос:

arqady в сообщении #153163 писал(а):

Jnrty, а можно хотя бы ссылочку на "Идиотизмы Давидюка" и на "лёгкую" формализацию на этом форуме, чтобы самому оценить.
Мне по поиску ничего не удалось найти.
Спасибо!

[Someone]

Извините, naiv1, исправил ссылку. Но я не перепутал, а просто нажал не ту кнопку: здесь можно выделить текст в одном сообщении, а кнопку нажать на другом сообщении, и получится ссылка на то сообщение, в котором была кнопка, а текст цитаты - тот, который выделен.

naiv1 в сообщении #153314 писал(а):

Тогда как Вы отличите "аксиомы" вида 2+2=4 и 2+3=5, "выводимые из других [аксиом]" от теорем ... - утверждений, которые тоже выводятся из аксиом?

А зачем их отличать?

[naiv1]

Someone писал(а):

naiv1 в сообщении #153314 писал(а):

Тогда как Вы отличите "аксиомы" вида 2+2=4 и 2+3=5, "выводимые из других [аксиом]" от теорем ... - утверждений, которые тоже выводятся из аксиом?

А зачем их отличать?

Согласен, раз и "аксиомы" вида 2+2=4 и 2+3=5 "выводятся" из других аксиом и теоремы выводятся из аксиом, то их можно не отличать! Но тогда зачем дублирование названий? Может оставить какоe-то одно?

Что предлагаете оставить в качестве названия выводимых утверждений:
- аксиомы или
- теоремы?

P.S. Хотелось бы получить ответ на вопрос, который я задавал маткибу:

naiv1 в сообщении #153314 писал(а):

Утверждение 2+3=3+2 по Вашему - это аксиома или нет?

[MaximKat]

naiv1
Выводимые утверждения это теоремы, но это не значит, что аксиома должна быть невыводимой

[naiv1]

MaximKat в сообщении #153547 писал(а):

но это не значит, что аксиома должна быть невыводимой

Согласен с этим. Не могли Вы только привести пример и/или пояснить это?

[MaximKat]

в арифметику пеано можно добавить аксиому "2+2=4"

[маткиб]

naiv1 в сообщении #153542 писал(а):

P.S. Хотелось бы получить ответ на вопрос, который я задавал маткибу:

naiv1 в сообщении #153314 писал(а):Утверждение 2+3=3+2 по Вашему - это аксиома или нет?

Если в списке аксиом её нет, то не аксиома. А если есть, то аксиома. А в чём проблема?

[epros]

Инт писал(а):

Поэтому, я буду придерживаться своих обозначений

А Вы тэгом math пользоваться не пробовали? Словесные конструкции однозначно понять не всегда возможно.

Инт писал(а):

вы утверждаете, будто бы рассуждение можно провести только в метатеории

Я утверждаю, что Гёдель проводит свои рассуждения в метатеории.

Инт писал(а):

Формулу «Ф эквивалентна Prf(Ф)» обозначим как А.

Формулу «Prf(Ф) влечёт Ф» обозначим как Б.

Обе формулы принадлежат теории S.

Докажите.

Инт писал(а):

Вы рассуждаете средствами теории T, но это не означает, что нельзя рассуждать в S, используя эти же формулы.

Докажите что можно.

Инт писал(а):

Решающим фактом при выводе «противоречия или логической ограниченности теории Гёделя» является несовместимость формул А и Б в S.

Всё дальнейшее Вы зря написали, ибо:
1. Несовместимость этих формул в теории S никого не интересует, ибо Гёдель не утверждал, что они есть в теории S.
2. То, что эти формулы могут быть записаны в теории S, Вами декларировано, но не доказано.

[Инт]

Здесь дам замечание, не зависящее от возможных возражений относительно параграфов 10-12.
Рассуждения, изложенные в параграфах 10-12, можно существенно сократить.
Назовём теорию «логически ограниченной в математических средствах», если она не содержит очевидные математические аксиомы, заведомо используемые в математике.
Назовём теорию «логически ограниченной в логических средствах», если она не содержит очевидные логические аксиомы, заведомо используемые в логике.
Тогда, если в теории S отрицается содержание формулы Б среди аксиом (теорем) этой теории, то мы получаем (это подробно обсуждалось), что S можно интерпретировать как логически ограниченную в логических средствах.
Если среди аксиом теории S не содержится формула А, то S оказывается логически ограниченной в математических средствах, т.е. будет выполняться то, что выше я назвал «слабой патологией».
В самом деле. В крайнем случае, теория T будет обладать всеми правами на определения, а S всеми обязанностями для доказательств выводов из этих определений. В более мягком варианте, окажется так или иначе, что T будет сильнее чем S. Окажется, что T определены эффективно некоторые функторы, очевидно используемые в содержательной арифметике, но в S эти функторы будут «определены слабо».
В связи с этим, «доказуемость» Prf мы можем интерпретировать как очевидно «логически ограниченную в математических средствах», т.е. ограниченную в естественных аксиомах, так как мы всё-таки фактически, т.е. через содержательные рассуждения теории T, легко умеем разрешать гёделеву формулу Ф. На каком основании мы считаем, что S будет содержать достаточно богатую теорию арифметики? Ведь, построив S, мы не использовали в выстраиваемой арифметике все очевидно эффективные процедуры. Где критерии, по которым мы считаем, что эффективно для арифметики, а что нет? Именно поэтому, я утверждал, что формула А должна быть по своему естественному смыслу быть аксиомой арифметики, иначе же теряется весь содержательный смысл теории S.
Никем не доказано, например, что при помощи теории T невозможно определить некую теорию E, которая: содержит S, и использует один для всех теорий язык; хотя в S невозможно доказательство некоторых утверждений, это только означает, что к S не присоединены некоторые простые и эффективные аксиомы, которые легко доказываются в E при помощи эффективных с точки зрения содержательной арифметики процедур. При этом, E может рассматриваться как некоторая арифметика.

Добавлено спустя 6 минут 32 секунды:

epros писал(а):

Я утверждаю, что Гёдель проводит свои рассуждения в метатеории.

Инт писал(а):

Формулу «Ф эквивалентна Prf(Ф)» обозначим как А.

Формулу «Prf(Ф) влечёт Ф» обозначим как Б.

Обе формулы принадлежат теории S.

Докажите.

Инт писал(а):

Вы рассуждаете средствами теории T, но это не означает, что нельзя рассуждать в S, используя эти же формулы.

Докажите что можно.

Инт писал(а):

Решающим фактом при выводе «противоречия или логической ограниченности теории Гёделя» является несовместимость формул А и Б в S.

Всё дальнейшее Вы зря написали, ибо:
1. Несовместимость этих формул в теории S никого не интересует, ибо Гёдель не утверждал, что они есть в теории S.
2. То, что эти формулы могут быть записаны в теории S, Вами декларировано, но не доказано.

Если формулы А и Б не принадлежат теории S, и их нельзя использовать в рассуждениях S, то относительно недоказуемости их в S бессмысленно говорить. В частности, тогда никакаго смысла не имеет "теорема Гёделя", т.е. она имеет смысл тогда, когда эти формулы принадлежат S, но недоказуемы в этой теории.

[epros]

Инт писал(а):

Если формулы А и Б не принадлежат теории S, и их нельзя использовать в рассуждениях S, то относительно недоказуемости их в S бессмысленно говорить.

Относительно недоказуемости чего? Гёдель говорит о недоказуемости в $S$ некой формулы $G$, но он ничего не говорит о доказуемости или недоказуемости в $S$ "формулы А":
$G \leftrightarrow \neg (S \vdash G)$

Инт писал(а):

В частности, тогда никакаго смысла не имеет "теорема Гёделя", т.е. она имеет смысл тогда, когда эти формулы принадлежат S, но недоказуемы в этой теории.

Не знаю, какой ещё "смысл" Вы ищете, но теорема говорит именно о том, о чём говорит:
Есть такое арифметическое выражение $G$, которое истинно (что доказано метатеорией $T$), но недоказуемо средствами теории $S$.

[naiv1]

маткиб писал(а):

naiv1 в сообщении #153542 писал(а):

P.S. Хотелось бы получить ответ на вопрос, который я задавал маткибу:

naiv1 в сообщении #153314 писал(а):Утверждение 2+3=3+2 по Вашему - это аксиома или нет?

Если в списке аксиом её нет, то не аксиома. А если есть, то аксиома. А в чём проблема?

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

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