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

[Инт]

Xaositect-у

Цитата:

Если я правильно понял, вы утверждаете, что в арифметике Пеано PA нельзя построить формулу, выражающую доказуемость в PA?

Почти так поняли, но точнее моё утверждение таково: Гёдель построил такое определение "доказуемости", что та должна быть или противоречивой или патологичной. Между прочим, термин "патология" - узаконенный математический термин. Мне он не нравится, я использовал его по горячности. Я использую - другой: "логическая ограниченность".

Добавлено спустя 17 минут 31 секунду:

Xaositect-у

Цитата:

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

Пусть себе согласуется. Это не отменяет доказательств в ПОСТАХ 1 и 2.

[Xaositect]

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

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

Если все-таки использовать математические термины - противоречивой или неполной.

Это определение доказуемость построил не Гедель, это сделали еще до него. Определение следующее:
1. Если утверждение является аксиомой, то оно доказуемо.(В число аксиом входят аксиомы логики предикатов)
2. Если доказуемы утверждения A->B и A, то доказуемым считается и утверждение B.
3. Если докафуемо утверждение A(x)(x-свободная переменная), то доказуемо и $\forall x A(x)$.

Для того, чтобы проходило доказательство теоремы Геделя, нужно, чтобы доказуемыми являлись аксиомы арифметики Пеано.

Чем вам не нравится это определение?

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

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

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

Это и есть утверждение теоремы Геделя! Если вы хотите сказать, что математике лучше пользоваться не классическим определением формального доказательства, а каким-то другим, то подрудитесь привести его и указать преимущества перед классическим.

[Инт]

Xaositect-у

Цитата:

Если все-таки использовать математические термины - противоречивой или неполной.

Это определение доказуемость построил не Гедель, это сделали еще до него.

Я имел ввиду "доказуемость" как предикат Prf. "Патология" теории Гёделя - это несовместимость с аксиомой, что "из доказуемости вытекает истинность". В этой связи, патологична даже та неполнота, о которой Вы говорите. Поскольку она означает невозможность вывода формулы Гёделя относительно патологичной дедуктики. Я специально для Вас Xaositect и для маткиб специально создал ПОСТ №2 посмотрите его. Там эти ньюансы и разъясняются.

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

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

[Xaositect]

btw, привет маткибу, мы с одной кафедры

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

Я специально для Вас Xaositect и для маткиб специально создал ПОСТ №2 посмотрите его. Там эти ньюансы и разъясняются.

Вам уже сказали, что теория, состоящая из аксиом арифметики+аксиомы Prf(A)->A противоречива.

[epros]

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

Хотел бы, чтобы обсуждение коснулось собственно "теоремы Гёделя"

Мда, зачем тогда было вываливать столько текста на другие темы?

Касательно первой теоремы Гёделя о неполноте: Она доказана, причём вполне конструктивно. Рассуждая в рамках метатеории, Гёдель доказывает существование в любой теории $T$, включающей арифметику, арифметического выражения $G$, равносильного недоказуемости этого же выражения $G$ в рамках данной теории $T$:
$G \leftrightarrow \neg (T \vdash G)$

Гёдель отсюда делает вывод об истинности $G$, прибегая к неконструктивному металогическому рассуждению о том, что утверждение $G$ либо истинно, либо ложно, а поскольку его ложность означала бы противоречивость теории $T$ (доказуемость в ней ложного утверждения), то выражение $G$, построенное для непротиворечивой теории $T$, должно быть истинным.

Хотя это рассуждение и неконструктивно, но истинность утверждения $G$ может быть доказана и конструктивным образом, если использовать только тот факт, что любое утверждение теории $T$ истинно (с точки зрения метатеории, естественно):
$(T \vdash S) \to S$
(и не использовать предположение о двузначности логики).

Тогда утверждение о доказуемости $G$ в теории, т.е. $T \vdash G$, сводится к противоречию, что и означает его отрицание, т.е. $\neg (T \vdash G)$, а откуда в свою очередь следует $G$.

[Инт]

Xaositect-у

Цитата:

Вам уже сказали, что теория, состоящая из аксиом арифметики+аксиомы Prf(A)->A противоречива

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

Добавлено спустя 5 минут 9 секунд:

epros-у

Согласен с Вами, что не расчитал силы на такое количество тем. Думал обсуждение будет более спокойным. Скажите, прочли ли Вы Посты 1 и 2?

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

[маткиб]

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

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

По поводу Гёделевской доказуемости. Если мы строим какую-то теорию, претендующую на полную формализацию математики, мы хотим следующего:
1) Теория позволяет доказывать хотя бы утверждения, записанные на языке формальной арифметики Пеано (она может позволять и много чего другого, но этот минимум обязателен).
2) Доказательством в этой теории является конечная строка символов в некотором фиксированном алфавите (структура этого доказательства никого не волнует, она может быть какой угодно).
3) Существует эффективная процедура проверки, является ли строка символов доказательством для заданной формулы языка формальной арифметики (вполне естественное требование, чтобы доказательства можно было проверять автоматически; формализация понятия "эффективная процедура" - машина Тьюринга, корень этой формализации в законах физики).
4) Доказать в данной теории можно только истинные формулы языка формальной арифметики.

Теорема Гёделя утверждает, что такая теория не может быть полной. Что тут не так в определении доказуемости, что оно стало патологичным? С каким из требований вы не согласны?

Xaositect в сообщении #152075 писал(а):

btw, привет маткибу, мы с одной кафедры

Опа.

[Инт]

epros-у

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

В силу доказательств, изложенных в ПОСТАХ №1 и №2 Ваш тезис о доказанности «теоремы Гёделя» ложен. Сразу могу предположить, что для обоснования тезиса «о доказанности теоремы Гёделя» Вы будете выдвигать аргументы общего характера, на которые всегда найдутся контраргументы такого же общего характера. И мы будем ходить не то по кругу, не то по логическому квадрату как с двумя предыдущими участниками темы. Это не очень интересно. Кроме того, я хорошо знаком с тем как «доказывается теорема Гёделя».

Предлагаю сосредоточиться на той детали дискуссии, на которой она в наибольшей степени оказалась заострена.

Поэтому ВСЕМ:

«Школа» уже признаёт, что соотношение, в котором участвует формула Гёделя (т.е. что формула эквивалентна собственной недоказуемости), несовместимо с такой естественной аксиомой как «доказуемость влечёт истинность». Теперь добьёмся признания другого факта: отрицание указанной естественной аксиомы означает «логическую неполноценность гёделевой арифметики». В последних постах уже предпринимались попытки дезавуировать этот мой последний тезис тем, что он якобы как раз и означает «неполноту арифметики».

Все основные аргументы по этому поводу, уже изложены в ПОСТАХ №1 и №2. Тем не менее, постараюсь более полно раскрыть аргументацию.

Я уже приводил пример для МАТКИБА, в котором указал, как может быть определён функтор г(n) так, чтобы снять явное противоречие, возникающее в связи с определениями Гёделя. Таким образом переопределённый функтор будет входить в теорию, которая: 1) тривиально разрешает «формулу Гёделя»; 2) очевидно достаточно богата; 3) непротиворечива, если непротиворечива арифметика; 4) в такой по-новому определённой теории будет выполняться оспариваемая «школой» аксиома. Другим примером теории, где такая аксиома встречается является конструктивная логика: в последней используется аксиома «DX влечёт X», где D – «оператор доказуемости», X – высказывание, которое может рассматриваться как с кванторами, так и без них.

Иными словами, естественные теории, в которых используется аксиома, что из доказуемости следует истинность, существуют.

Что же будет, если мы отрицаем эту аксиому? Если последователи Гёделя уж ввели такое высказывание как Prf(Ф), не допустимое в канонической формальной логике, то будте добры обеспечьте ваше высказывание минимальными логическими средствами. И уж во всяком случае, аксиома, что доказуемость влечёт истинность, должна рассматриваться одной из первых. На каком основании, Вы, при отрицании аксиомы, утверждаете, что тогда Ваша теория арифметики будет адекватна обычной содержательной арифметике. Если Вы ссылаетесь на теорему Гёделя, чтобы обосновать отрицание аксиомы, то это аргумент, использующий то, что ещё необходимо доказать. Ведь аксиома рассматривается нами (см. ПОСТЫ №1 и №2) именно, на этапе рассуждения «до доказательства теоремы Гёделя».

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

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

Последнее рассуждение, это пока не ответ МАТКИБу на его послений пост.

Добавлено спустя 3 минуты:

маткиб-у

Цитата:

По поводу Гёделевской доказуемости. Если мы строим какую-то теорию, претендующую на полную формализацию математики, мы хотим следующего:
1) Теория позволяет доказывать хотя бы утверждения, записанные на языке формальной арифметики Пеано (она может позволять и много чего другого, но этот минимум обязателен).
2) Доказательством в этой теории является конечная строка символов в некотором фиксированном алфавите (структура этого доказательства никого не волнует, она может быть какой угодно).
3) Существует эффективная процедура проверки, является ли строка символов доказательством для заданной формулы языка формальной арифметики (вполне естественное требование, чтобы доказательства можно было проверять автоматически; формализация понятия "эффективная процедура" - машина Тьюринга, корень этой формализации в законах физики).
4) Доказать в данной теории можно только истинные формулы языка формальной арифметики.

Всё верно. Только это никак не влечёт, что теорема Гёделя доказана. Что патологичного? см. ПОСТ №2 и это сообщение.

[epros]

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

epros-у

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

Если можно, ткните пальцем в номер "параграфа", а желательно - и в абзац "поста №2".

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

Итак, вот два формальных утверждения мета-теории:
$G \leftrightarrow \neg (T \vdash G)$
$(T \vdash G) \to G$
Продемонстрируйте формальный вывод из них противоречивого утверждения.

[маткиб]

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

Теперь добьёмся признания другого факта: отрицание указанной естественной аксиомы означает «логическую неполноценность гёделевой арифметики».

Ты добился моего признания! Я признаю этот факт!

От тебя требуется только самая малость: привести пример полноценной теории.

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

Я уже приводил пример для МАТКАБА, в котором указал, как может быть определён функтор г(n) так, чтобы снять явное противоречие, возникающее в связи с определениями Гёделя.

Это где это? Тут что ли?

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

По Вашей просьбе укажу как построить требуемую Вами теорию. Повторяю, это никак не влияет ни на отрицание, ни на подтверждение моих выводов, т.е. вопрос Ваш не по существу дела: Считаем, что формула Гёделя присоеденена к арифметике в качестве аксиомы изначально. Поэтому, существует (возможно не один) номер N доказательства для Ф. Для функтора г, о котором говорится в ПОСТЕ №1, переопределяем г(N) = 0, не смотря на то, что N - номер доказательства, для остальных номеров доказательств значения г оставляем прежними. Тогда: 1) формула Гёделя тривиально разрешима; 2) богатство теории от этого очевидно не пострадает; 3) будет снято противоречие, о котором я говорю.

Ты можешь сколько угодно переопределять функтор г, но от противоречия, связанного с выделенным жирным, ты не избивился. Формула Гёделя является утверждением о доказуемости в самой теории (т.е. той, к которой ты её уже добавил как аксиому). Поэтому её нельзя вот так вот просто так добавить. Это как сказать "считаем, что x=x+1".

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

Таким образом переопределённый функтор будет входить в теорию, которая: 1) тривиально разрешает «формулу Гёделя»; 2) очевидно достаточно богата; 3) непротиворечива, если непротиворечива арифметика; 4) в такой по-новому определённой теории будет выполняться оспариваемая «школой» аксиома. Другим примером теории, где такая аксиома встречается является конструктивная логика: в последней используется аксиома «DX влечёт X», где D – «оператор доказуемости», X – высказывание, которое может рассматриваться как с кванторами, так и без них.

В "конструктивной логике", про которую ты говоришь, D - не оператор доказуемости, а просто значок, про который мы можем просто тупо выписать аксиомы, а у тебя Prf - не значок, а просто сокращенное обозначение, вместо которого всегда подразумевается арифметическая формула, выражающая доказуемость. Поэтому если ты добавляешь в теорию аксиомы, то DX как был DX'ом, так им и остаётся, а вот Prf(X) изменяется. Поэтому твоё "считаем, что такая аксиома у нас уже есть" можно считать бессмысленным набором слов, аналогичным парадоксу лжеца.

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

Цитата:По поводу Гёделевской доказуемости. Если мы строим какую-то теорию, претендующую на полную формализацию математики, мы хотим следующего:

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

2) Доказательством в этой теории является конечная строка символов в некотором фиксированном алфавите (структура этого доказательства никого не волнует, она может быть какой угодно).

3) Существует эффективная процедура проверки, является ли строка символов доказательством для заданной формулы языка формальной арифметики (вполне естественное требование, чтобы доказательства можно было проверять автоматически; формализация понятия "эффективная процедура" - машина Тьюринга, корень этой формализации в законах физики).

4) Доказать в данной теории можно только истинные формулы языка формальной арифметики.

Всё верно. Только это никак не влечёт, что теорема Гёделя доказана. Что патологичного? см. ПОСТ №2 и это сообщение.

Для такой формулировки доказуемости (пункты 1,2,3,4) теорема Гёделя доказана, читать учебники. Если ты не согласен, то ты должен указать тот пункт, который тебе кажется не соответствующим реальному представлению о доказуемости.

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

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

Теорема Гёделя ничего не говорит о ТВОЁМ РЕАЛЬНОМ МЫШЛЕНИИ. Мышление само по себе неалгоритмично, это более или менее понятно всем, способным самостоятельно мыслить.

P.S. Коверкание ников ума не прибавляет.

[Инт]

epros-у

Цитата:

Если можно, ткните пальцем в номер "параграфа"...

Параграф 7. Но так же посмотрите предварительные определения.

Добавлено спустя 8 минут 36 секунд:

маткиб-у

Цитата:

Ты можешь сколько угодно переопределять функтор г, но от противоречия, связанного с выделенным жирным, ты не избивился. Формула Гёделя является утверждением о доказуемости в самой теории (т.е. той, к которой ты её уже добавил как аксиому). Поэтому её нельзя вот так вот просто так добавить. Это как сказать "считаем, что x=x+1"...

В "конструктивной логике", про которую ты говоришь, D - не оператор доказуемости, а просто значок, про который мы можем просто тупо выписать аксиомы, а у тебя Prf - не значок, а просто сокращенное обозначение, вместо которого всегда подразумевается арифметическая формула, выражающая доказуемость. Поэтому если ты добавляешь в теорию аксиомы, то DX как был DX'ом, так им и остаётся, а вот Prf(X) изменяется. Поэтому твоё "считаем, что такая аксиома у нас уже есть" можно считать бессмысленным набором слов, аналогичным парадоксу лжеца...

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

D эквивалентен моему Prf. D не тупой значок.

[маткиб]

Более конкретно, использование твоей "аксиомы" требует неалгоритмичной спосбности к обобщению.

Вообще, читай про ординалы, на примере ординалов можно явно увидеть это "обобщение".

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

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

Никакой аксиомы я не добавлял. Я рассуждал условно: для случая, когда она есть в теории, и для случая когда её нет.

её нет.

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

D эквивалентен моему Prf. D не тупой значок.

D - тупой значок, определяемый аксиоматически.

[epros]

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

Цитата:

Если можно, ткните пальцем в номер "параграфа"...

Параграф 7. Но так же посмотрите предварительные определения.

Отлично, давайте тогда с самого начала этого параграфа:

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

§7

Для вывода противоречия в теории S нам потребуются два утверждения.

1. Какова бы ни была S-формула Ж, средствами теории S из доказуемости Ж можно извлечь, что Ж верна. Т.е., в S верна аксиома: «Prf(Ж) влечёт Ж» (схема аксиом). Эта аксиома может быть заменена на некоторое эквивалентное правило вывода.

2. Существует формула Ф из S такая, что средствами теории S доказуемо, что «Ф равносильна формуле неPrf(Ф)».

Посмотрим также некоторые предварительные определения выше по тексту:

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

S – теория, интерпретируемая средствами теории T.

Итак, в Ваших обозначениях теория S - это не мета-теория, а интерпретируемая теория.

Каким же тогда образом средствами этой теории можно судить о доказуемости Ж (или Ф), да ещё и о выводимости из этой доказуемости чего-то или о равносильности её чему-то?

Со своей стороны хочу отметить, что теорема Гёделя доказывается не в интерпретируемой, а в интерпретирующей теории, т.е. в мета-теории. Поэтому как утверждение о равносильности $G$ с недоказуемостью $G$, так и утверждение о следовании $G$ из доказуемости $G$ - это тоже утверждения интерпретирующей теории.

[Инт]

Цитата:

Итак, в Ваших обозначениях теория S - это не мета-теория, а интерпретируемая теория.

Каким же тогда образом средствами этой теории можно судить о доказуемости Ж (или Ф), да ещё и о выводимости из этой доказуемости чего-то или о равносильности её чему-то?

Со своей стороны хочу отметить, что теорема Гёделя доказывается не в интерпретируемой, а в интерпретирующей теории, т.е. в мета-теории. Поэтому как утверждение о равносильности с недоказуемостью , так и утверждение о следовании из доказуемости - это тоже утверждения интерпретирующей теории.

Вы так и не прочли мои определения и мои доказательства. Учите меня тому, что я и сам определил в постах №1 и №2. Иными словами, там приведено рассуждение именно в метатеории, которое "доказывает теорему Гёделя". Средствами S можно судить о доказуемости формул, так как в S определён предикат Prf. Средствами T, т.е. средствами метатеории, так же можно судить о доказуемости формул, так как S - часть T. "Школой" считается, что средствами метатеории T доказана недоказуемость посредством теории S формулы Гёделя, которая есть формула теории S. Всё это в деталях я описал в соответствующих постах. Именно предвидя подобное "возможное возражение", я и создал пост №2.

[mud]

Инт, блестяще!!