Теорема Геделя и физика

[arseniiv]

Наверно, верно. В общем, получается, удивляет существование неполных теорий. Ну, я в таком ключе просто не думал — по мне, было бы странно, если бы существовали только противоречивые, но не существовали неполные, или наоборот. Но, опять же, я неполные теории могу как пирожки печь безо всяких глубоких теорем: берём, например, пустое множество формул. Относительно логического следования замкнуто, а вот с полнотой у него плохо. Или пример ближе к реальности: например, теория двухэлементного множества, аксиоматизируемая с помощью $\{\forall x\forall x'\forall x''(x\ne x'\to x''=x\vee x''=x'),\exists x\exists x'(x\ne x')\}$, и добавим к ней константы $a,b$. Новая теория ничего не говорит о том, $a=b$ или $a\ne b$, и совершенно естественно, что она неполна (и имеет с точностью до изоморфизма две модели, которые можно «выделить», добавляя к аксиомам $a=b$ или $a\ne b$).

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

[kp9r4d]

arseniiv
Существование неполных foundation-теорий, то есть, годящихся в качестве оснований для математики. В неполноте теории двухэлементного множества ничего удивительного не вижу. Удивляет, опять же, потому, что это серьезный контраргумент против различного платонизма и математического реализма и по сути сильно компрометирует (по крайней мере для меня) такие несепарабельные конструкции как "модель", "истинность", "стандартная модель натуральных чисел", ... Ну вот был пример с "возьмём все верные арифметические утверждения, получим непротиворечивую но не рекурсивно-аксиоматизируемую теорию", ну вот только чтобы говорить об истинности нужно зафиксировать модель, а это действие фиксации модели происходит в какой-то метатеории, к которой тоже применима теорема Гёделя - получается "стандартная модель натуральных чисел" - это вообще нечто совсем эфимерное и спекулятвное, что никакими логическими финитарными средствами не потрогаешь.

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

[arseniiv]

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

Существование неполных foundation-теорий, то есть, годящихся в качестве оснований для математики.

Ну, не факт, что нам всегда будет хватать, скажем, теории, эквивалентной ZFC. Да и сейчас, насколько помню, не всегда хватает.

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

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

Можно читать понемногу параллельно с чем-нибудь. Там ведь главная разница — в дополнительной аксиоме и ещё одном способе придавать смысл термам.

[kp9r4d]

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

Ну, не факт, что нам всегда будет хватать, скажем, теории, эквивалентной ZFC. Да и сейчас, насколько помню, не всегда хватает.

Ну для высших категорий не хватает. Но терминология не моя, я на курсе Бочарова о метаматематике её услышал.

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

Можно читать понемногу параллельно с чем-нибудь. Там ведь главная разница — в дополнительной аксиоме и ещё одном способе придавать смысл термам.

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

[arseniiv]

А как туда прикладывается точка зрения классической логики — имеется в виду «для всякого типа $A$ выводимо $a:A$ или $a:A\to\mathbf0$»?

[nazarov_m]

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

nazarov_m
Мне кажется, вы слишком платонист и именно поэтому столь сильно упрощаете ситуацию.

nazarov_m в сообщении #1166871 писал(а):

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

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

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

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

Вы уж извините, но у вас странные представления о теоремах Гёделя. Такого не утверждает ни одна из его теорем, это какие-то вольные интерпретации, которые не имеют прямого отношения к теоремам Гёделя.
Первая теорема Гёделя о неполноте утверждает, что если формальная арифметика (минимум в форме Пеано) на основе логики первого порядка непротиворечива, то в ней существует невыводимая формула.
Вторая теорема Гёделя о неполноте утверждает, что если формальная арифметика (тот же минимум Пеано) на основе логики первого порядка непротиворечива, то в ней невыводима некоторая формула, содержательно утверждающая непротиворечивость этой арифметики.
http://www.ams.org/notices/200604/fea-davis.pdf
Вы точно не путаете выводимость с истинностью? Рассуждение про разные универсумы и там добавление всяких аксиом, а потом к ним отрицания --- это всё к теореме Гёделя не имеет ну просто никакого отношения. Это очевидные азы мат логики, что мы можем собрать разные версии теорий, комбинирую аксиомы, в том числе беря отрицания каких-то аксиом, и т.д. Вы даже можете от базовых аксиом логики первого порядка отказываться на выбор, но только не нужно при этом говорить что вы это делаете по следствию из теоремы Гёделя.

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

nazarov_m в сообщении #1166871 писал(а):

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

Никто выводов и не делает, все только строят метафоры. Метафоры - вещь очень хорошая.

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

[Pphantom]

Тема перемещена из форума «Физика» в форум «Междисциплинарный раздел»
Причина переноса: вопреки заявленной теме беседы, физика закончилась где-то еще на первой странице, так что, пожалуй, тут это будет уместнее.

[kp9r4d]

nazarov_m в сообщении #1170530 писал(а):

Вы точно не путаете выводимость с истинностью?

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

nazarov_m в сообщении #1170530 писал(а):

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

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

arseniiv
Да, вопрос хороший, я сейчас прямо запутался немного. Мне нужно кое-что перечитать и я отвечу.

[nazarov_m]

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

nazarov_m в сообщении #1170530 писал(а):

Вы точно не путаете выводимость с истинностью?

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

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

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

nazarov_m в сообщении #1170530 писал(а):

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

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

Что-то вы опять наделяете теорему Гёделя не характерными для неё свойствами. Про какую такую метатеорию вы говорите? Вроде бы не секрет, что теорема Гёделя о неполноте доказана в рамках логики первого порядка, к которой аксиоматика Пеано присоединена. Она рассуждает про ту самую теорию, в рамках которой эта теория сформулирована и доказана, либо про любую другую, которая включает её как подмножество. Т.е. теорема Гёделя завязана на логику первого порядка и аксиоматику Пеано, и не является небожителем из непонятной метатеории.

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

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

Что ещё за фиксация истинности арифметических теорем, и почему вы считаете что её нельзя зафиксировать человеческими средствами? Какую истинность вы имеете ввиду: религиозную или тождественную на некой модели? Вообще в целом, у теорем обычно не фиксируется никакая истинность, а проверяется их выводимость из аксиом. Возможно что вы имели ввиду тот факт, что фиксируется некоторый набор аксиом для описания натуральных чисел в рамках логики первого порядка? И что теорема Гёделя утверждает, что его нельзя зафиксировать, чтобы получить полную и непротиворечивую теорию? Вообще это мягко говоря не так. Теоремы Гёделя работают только с аксиоматикой Пеано и только в логике первого порядка.
Контр-пример: арифметика Пресбургера для натуральных чисел. Для неё доказана полнота и непротиворечивость средствами самой теории. И никакая теорема Гёделя в этой теории не действует.
Контри-пример 2: возьмите логику высшего порядка и получите непротиворечивую теорию даже с аксиомами Пеано.

[mihaild]

nazarov_m в сообщении #1170817 писал(а):

Для неё доказана полнота и непротиворечивость средствами самой теории.

Как она там формулируется? А то стандартный $\Box$ требует умножения.

[Xaositect]

nazarov_m в сообщении #1170817 писал(а):

Контр-пример: арифметика Пресбургера для натуральных чисел. Для неё доказана полнота и непротиворечивость средствами самой теории. И никакая теорема Гёделя в этой теории не действует.

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

Но слабые теории, доказывающие в некотором смысле свою непротиворечивость, есть: http://www.cs.albany.edu/~dew/m/jsl1.pdf

[iifat]

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

Только вот теорема Гёделя доказывается в некоторой метатеории, в которой тоже верна теорема Гёделя, только этот момент заметается обычно под ковёр

А я уж подумал, что эти теория с метатеорией заявились к вам в дом в два часа ночи и водрузили немытые ноги на скатерть. Неполнота не отрицает ничего кроме полноты. Доказанное таковым остаётся, и неполнота никоим образом никаких доказательств не дискредитирует.

[nazarov_m]

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

nazarov_m в сообщении #1170817 писал(а):

Контр-пример: арифметика Пресбургера для натуральных чисел. Для неё доказана полнота и непротиворечивость средствами самой теории. И никакая теорема Гёделя в этой теории не действует.

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

Но слабые теории, доказывающие в некотором смысле свою непротиворечивость, есть: http://www.cs.albany.edu/~dew/m/jsl1.pdf

Я гляну в доказательство, но насколько помню непротиворечивость и полнота доказываются без привлечения более мощной теории у Пресбургера. А вот разрешимость алгоритмическая как раз таки да, доказывается с её привлечением (не помню что конкретно там нужно добавить).
http://cs.fit.edu/~ryan/papers/presburger.pdf

[Xaositect]

nazarov_m в сообщении #1170873 писал(а):

Я гляну в доказательство, но насколько помню непротиворечивость и полнота доказываются без привлечения более мощной теории у Пресбургера. А вот разрешимость алгоритмическая как раз таки да, доказывается с её привлечением (не помню что конкретно там нужно добавить).

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

[nazarov_m]

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

nazarov_m в сообщении #1170873 писал(а):

Я гляну в доказательство, но насколько помню непротиворечивость и полнота доказываются без привлечения более мощной теории у Пресбургера. А вот разрешимость алгоритмическая как раз таки да, доказывается с её привлечением (не помню что конкретно там нужно добавить).

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

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