Вопрос по теореме Геделя

[tac14]

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

Математика интересна как инструмент. Причём тут эксперименты?

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

Но увы, такая математика на практике не интересна. И математикам с этим надо считаться, и понимать что выводы математики исключительно интересны, когда они что-то прогнозируют о реальном мире. Только для этого создают формализмы, а по сути модели, и имея данные экспериментов что-то прогнозируется ... Если же теорема Геделя говорит, что "практически любой" (критерий так и не найден, надо полагать) формализм неполон, то какой смысл его строить? Чтобы описать некий частный случай некоторых наборов экспериментов? Так как наугад сделанные другие эксперименты (другим экспериментатором) с большой вероятностью, будет просто не разрешим в выбранном ранее формализме.

-- Ср июл 15, 2015 03:44:07 --

arseniiv в сообщении #1037248 писал(а):

Если теория противоречива, в ней всё подряд выводимо

и как мы отличим полную теорию без противоречий, и полную теорию с противоречиями ?

-- Ср июл 15, 2015 03:50:16 --

arseniiv в сообщении #1037248 писал(а):

не верна аксиома — это просто по глупости написано (ещё раз, читайте про то, о чём собираетесь писать)

(Оффтоп)

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

[kp9r4d]

tac14 в сообщении #1037249 писал(а):

Чтобы описать некий частный случай некоторых наборов экспериментов?

Вы наверное не до конца понимаете, о каких теориях говорит теорема Гёделя, так вот теорема Гёделя говорит о сильных теориях, даже СИЛЬНЫХ теориях. Они сильнее вас: любое математическое рассуждение которое вы когда либо сможете придумать формализуется в любой сильной теории, то же самое касается 99.9% вообще всех математических рассуждений.

tac14 в сообщении #1037249 писал(а):

и как мы отличим полную теорию без противоречий, и полную теорию с противоречиями ?

Например, в противоречивой теории выводится противоречие.

-- 15.07.2015, 02:52 --

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

[tac14]

kp9r4d в сообщении #1037252 писал(а):

Вы наверное не до конца понимаете, о каких теориях говорит теорема Гёделя, так вот теорема Гёделя говорит о сильных теориях, даже СИЛЬНЫХ теориях. Они сильнее вас: любое математическое рассуждение которое вы когда либо сможете придумать формализуется в любой сильной теории, то же самое касается 99.9% вообще всех математических рассуждений.

Конечно, не понимаю. Мне уже назвали 3 варианции судя по всему одного и того же:

1. формальная система достаточно богата
2. достаточно содержательной теорией
3. о сильных теориях

Вас ист дас?

[arseniiv]

tac14 в сообщении #1037249 писал(а):

и как мы отличим полную теорию без противоречий, и полную теорию с противоречиями ?

В противоречивой выводится вообще всё. В полной выводятся все истинные формулы и ни одна ложная.

Может, всё-таки познакомитесь уже с определениями вещей, о которых пишете? Притом они, если аккуратно смотреть, есть прямо тут под носом — несколькими страницами ранее!

tac14 в сообщении #1037249 писал(а):

"практически любой" (критерий так и не найден, надо полагать)

Надо полагать, вы даже ответы вам в этой теме не читаете:

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

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

[tac14]

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

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

Ок, хоть с кем то договорились, что это проблема системы. Мы меняем систему, и в этой новой системе, то что мы доказывали в прошлой не имеет ни какого смысла. Более того может быть снова не разрешимым. А нам хочется построить обязательно такую формальную систему, в которой и старые и новые утверждения могли бы анализироваться, согласно правилам системы. Но я не вижу ни какого "рецепта" для этого, т.е. то как строить "объединяющий формализм" и знать, что снова случайно не угодишь в неполноту по старым фактам.

Поэтому проблема есть.

Но я как то не понимаю, почему мы должны вообще пользоваться не полными формальными системами ? У полных формальных систем есть какой то изъян? Они не позволяют что-то описать? Что?

(и думаю ответ на этот вопрос позволил бы понять значение теоремы Геделя )

-- Ср июл 15, 2015 04:55:57 --

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

tac14 в сообщении #1037087 писал(а):

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

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

(Оффтоп)

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

[arseniiv]

tac14 в сообщении #1037259 писал(а):

У полных формальных систем есть какой то изъян?

Можно получить контрапозицией из теоремы Гёделя.

-- Ср июл 15, 2015 06:58:06 --

tac14 в сообщении #1037259 писал(а):

думаю вы вполне используете такого рода синонимы.

Выводимость (доказуемость) и истинность — это разные вещи, есличо.

[tac14]

arseniiv в сообщении #1037262 писал(а):

tac14 в сообщении #1037259 писал(а):

У полных формальных систем есть какой то изъян?

Можно получить контрапозицией из теоремы Гёделя.

А по русски?

[Lia]

tac14 в сообщении #1037259 писал(а):

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

tac14 в сообщении #1037087 писал(а):

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

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

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

Это не юмор.

tac14 Замечание за систематические выступления не по существу и игнорирование выступлений по существу.

Хотя Вам и кажется, что все наоборот.

[arseniiv]

tac14 в сообщении #1037263 писал(а):

А по русски?

Контрапозиция — это следование $A\to B\vDash\neg B\to\neg A$ или по-русски «Если из $A$ следует $B$, тогда из отрицания $B$ следует отрицание $A$».

Теорема Гёделя имеет вид «теория такая-то, такая-то и такая-то → теория неполна». Контрапозицией получится «теория полна → …».

[Xaositect]

tac14 в сообщении #1037259 писал(а):

Но я как то не понимаю, почему мы должны вообще пользоваться не полными формальными системами ? У полных формальных систем есть какой то изъян? Они не позволяют что-то описать? Что?

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

Ну то есть, как вариант, можно стать ультрафинитистом и сказать: меня интересуют только утерждения, в которых все числа не превышают $10^{100}$. Тогда существует полная теория, содержащая такие утверждения (правда, аксиоматика получится большая, экспоненциальная от этого ограничения).
Но это неудобно, ставить везде при переменных ограничения (причем везде разные - если в утверждении все переменные лежат в нужных пределах, то в доказательстве промежуточные результаты могут иметь разные ограничения). Легче сказать, что мы работаем со всеми числами, включая те, что практикам никогда не встретятся, и платим за это тем, что некоторые утверждения доказать не можем.

[epros]

tac14, Вы не слушаете что Вам говорят и уже несколько страниц несёте какую-то философскую пургу, не относящуюся к математике.

tac14 в сообщении #1037259 писал(а):

Но я как то не понимаю, почему мы должны вообще пользоваться не полными формальными системами ? У полных формальных систем есть какой то изъян?

Да, полнота -- это и есть изъян. Ибо она означает ограниченость выразительных средств теории.

tac14 в сообщении #1037249 писал(а):

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

Как показывает практика, такая математика интересна. И математика не занимается "прогнозированием о реальном мире". Она предоставляет инструмент для эффективного упорядочивания любых знаний (хоть о реальном, хоть о воображаемом мире). А сами эти знания о реальном мире добываются в наблюдениях и экспериментах, и никак иначе.

[mihaild]

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

mihaild в сообщении #1037207 писал(а):

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

Да, если в системе можно сформулировать, что такое доказательство. Собственно, теорема Геделя как раз об этом.

Теорема Гёделя же о том что $PA \nvdash \neg \Box \bot$, а не $PA \vdash \neg \Box \neg \Box \bot$.
Пусть $PA \vdash \neg \Box A$
$PA \vdash \bot \rightarrow A$
$PA \vdash \Box (\bot \rightarrow A)$
$PA \vdash \Box \bot \rightarrow \Box A$
$PA \vdash \neg \Box A \rightarrow \neg \Box \bot$
По modus ponens из предположения получаем $PA \vdash \neg \Box \bot$.
В каком переходе ошибка?

[Xaositect]

mihaild в сообщении #1037388 писал(а):

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

mihaild в сообщении #1037207 писал(а):

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

Да, если в системе можно сформулировать, что такое доказательство. Собственно, теорема Геделя как раз об этом.

Теорема Гёделя же о том что $PA \nvdash \neg \Box \bot$, а не $PA \vdash \neg \Box \neg \Box \bot$.
Пусть $PA \vdash \neg \Box A$
$PA \vdash \bot \rightarrow A$
$PA \vdash \Box (\bot \rightarrow A)$
$PA \vdash \Box \bot \rightarrow \Box A$
$PA \vdash \neg \Box A \rightarrow \neg \Box \bot$
По modus ponens из предположения получаем $PA \vdash \neg \Box \bot$.
В каком переходе ошибка?

Теорема Геделя формулируется "если арифметика непротиворечива, то она неполна". Т.е. $PA\nvdash \bot\Rightarrow PA\nvdash \neg\Box\bot$ и $PA\vdash \neg\Box\bot\rightarrow \neg\Box\neg\Box\bot$. В Вашем рассуждении ошибка в гипотезе - есть нестандартные модели $M$, в которых истинна противоречивость $PA$, т.е. в которых $M\vDash \Box A$ для всех $A$.

[mihaild]

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

Теорема Геделя формулируется "если арифметика непротиворечива, то она неполна". Т.е. $PA\nvdash \bot\Rightarrow PA\nvdash \neg\Box\bot$ и $PA\vdash \neg\Box\bot\rightarrow \neg\Box\neg\Box\bot$. В Вашем рассуждении ошибка в гипотезе - есть нестандартные модели $M$, в которых истинна противоречивость $PA$, т.е. в которых $M\vDash \Box A$ для всех $A$.

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

[epros]

mihaild в сообщении #1037434 писал(а):

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

Если я правильно понял, вся проблема растет от неоднозначности фразы на естественном языке, а именно: что означают слова "сформулировать в системе".

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

mihaild в сообщении #1037207 писал(а):

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

Да, если в системе можно сформулировать, что такое доказательство. Собственно, теорема Геделя как раз об этом.

Дело в том, что хотя $\neg \Box A$ формулируется в $PA$, но тот факт, что $\neg \Box A \leftrightarrow (PA \nvdash A)$ "формулируется" не в $PA$, а в $PA + \neg \Box \bot$.