Физика и теорема Геделя

[vc]

...
Но в арифметике путеводной нитью является омега непротиворечивость

Omega consistency was a specific tool used by Godel to prove his theorem. Rosser generalized Godel's result by replacing "omega-consistent" with
"consistent" so there is no need to rely on omega consistency any longer. Apparently, today, omega consistency presents only historical interest although I may be wrong about that.

К сожалению ничего такого в теории множеств нет. Разные аксиоматики, Axiom of Choice, Обобщенная гипотеза континума и гипотеза о недостижимых можностях... Количество теорий составляет десятки. Поэтому теории множеств больше напоминают игру со строками чем исследование свойств реальных объектов

I am not sure what you mean here. It's a well known fact that the bulk of 'ordinary' math relies on the ZF+C axioms and practicing mathematicians explicitly or implicitly use the same (that is if they care about this kind of stuff at all). 'Foundational' folks may explore alternative set theory axiomatics but I am not aware of any striking results in this area.

VC

[Bobo]

Нехороший Вы человек. У меня поезд TGV в 7 утра, а я вынужден Вам ответ писать

А Вы не спешите. Все равно ведь всей истины не узнаете

Но в арифметике путеводной нитью является омега непротиворечивость
То есть к аксиоматике Пеано P мы можем добавить как недоказуемое геделевское утверждение G так и его отрицание
Обе расширенные теории (P+G) и (P+ not G) будут некпротиворечивы
Но лишь одна из низ омега непротиворечива

Не могу ни согласиться, ни возразить - слишком тонкое место, моей формальной системы не хватает Но склоняюсь к тому, что incompleteness можно доказать, не обращая внимания на omega-consistency. Средствами теории алгоритмов скорее всего можно. Будет ли это доказательство выразимо в самой PA - точно не уверен.

То есть на самом деле любое утверждение о числах либо истинно либо ложно

Трудно возразить Однако этот факт никак не относится к свойствам формальной системы.

К сожалению ничего такого в теории множеств нет.....

Вы интуитивно считаете, что числа на самом деле есть, а множества - черт его знает?
На самом деле нет никаких оснований полагать, что числа есть. Более того, если ZF не имеет модели, то надо полагать, что и PA не имеет. А если даже быть уверенным, что PA имеет модель, то нет гарантии, что те "числа" о которых мы "знаем" истинность/ложность утверждений - являются моделью PA.

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

Вы же сказали "2,3 В общем да", и тут же сами вывели отрицание
Еще раз. Числа - это (предположительно) модель формальной системы, которую мы называем PA. Теорема Геделя не является утверждением о числах, она не является утверждением вообще. Это строка, выводимая в ПА. "Выводимость" и "противоречивость" выражаются в ПА. "Истинность" - нет. Впрочем, Вы это сами наверно знаете. Будучи инерпретированной в модели, строка Г приобретает смысл.
Вы хотите сказать, что строка "2*2=4" интерпретируется в модели, а строка "1234567=ProofNumber(7654321)" - нет? Таким образом Вы признаете, что Ваши "числа" - не есть модель ПА. Или Вы что-то другое имеете в виду?
Впрочем, я заранее согласен, что ТГ имеет "метасмысл", раз уж я в этом разговоре занял позицию формалиста - "смысл" мне пока до лампочки Главное - не говорите, что ТГ - "метатеорема метатеории"

5 Расскажите пожалуйста, я как то прошел мимо жтого в своем самопальном образовании по этому предмету

У меня тоже самопальное. Много рассказать не могу, боюсь много наврать.
Тарский доказал, что предикат истинности нельзя определить в сильной формальной теории. Из этого, и из того, что предикат доказуемости определить можно, быстренько следует неполнота. Рассуждения, однако, придется проводить и в терминах модели (семантика) и в терминах теории (формализм). Интересен исторический момент. Тарский и Гедель получили свои результаты одновременно. Говорят, что: Гедель знал о результате Тарского, но предпочел им не пользоваться, боясь, что не поймут и раскритикуют. И опубликовал чисто формальное доказательство. Тарский же, вроде, про Геделя не знал. Но критики тоже боялся. И в своих ранних работах избегал определенной терминологии (такой как "истина в данной модели"). Перестали бояться они, только когда к ним примкнули Сколем, Коэн, Тьюринг
Чисто семантическое док-во неполноты, которое я упоминал, придумал некто Kripke. Не знаю, когда. Он его не публиковал. Опубликовали его не так давно, когда уже существовал алгебраический аппарат теории моделей, который позволяет делать и не такие фокусы. Крипке строит не self-referring утверждение и доказывает его независимость от теории. Никакой "диагонализации". Используются нестандартные модели, но гораздо более простые, чем у Коэна в док-ве независимости ~CH. Все на "осмысленном" языке модели. Никакой арифметизации понятия формального доказательства. Правда, теорема чуть слабее, чем у Геделя, т.к. вместо непротиворечивости используется чуть более слабое, зато семантическое свойство.

[Dmitry67]

Думаете испортить мне путешествие ? А вот и не выйдет ! Я не буту тут торчать в интернет кафе Ниццы часами, а сейчас приамо выйду и уйду купаться в ночном океане ! И отвечу только в понедельник, вот (ну почему я пошел в интернет кафе ?)

[Dmitry67]

Omega consistency was a specific tool used by Godel to prove his theorem.

Да, это так. И в улучшеном доказательстве омега непротиворечивость не нужна
Но это не значит что ее можно выбрость !

Вернемся к доказательству Геделя. Как выглядит утверждение "я недоказуемо" ?

G == not exists x: proof(x очень длинное выражение )

При этом это утверждение оказывается истинным, то есть такого x не существует.

Мы теперь можем принять как G, так и not G как новую аксиому
Выберем второе, рассмотрим Peano + not G.
not G == exists x: proof(x)

Мы знаем что добавление этого высказывание не приведет к противоречию
С другой стороны, в Peano невозможно доказать что proof(K) истинно для некоторой константы K. Потому что если бы это можно было бы, то очевидно из

proof(const K) следует exists x: proof(X) == not G
Но ни G, ни not G не доказуемы

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

(*) для любого x можно доказать что not proof(X)

С другой стороны, мы принимаем как аксиому что

(**) exists x: proof(X)

Такая теория непротиворечива, но омега противоречива
Комбинация (*) и (**) делает эту теорию, на человеческий взгляд, очень плохой (интересно как у нее с моделяи ?)

[Dmitry67]

1
Вы интуитивно считаете, что числа на самом деле есть, а множества - черт его знает?

2
Более того, если ZF не имеет модели, то надо полагать, что и PA не имеет.

3
Теорема Геделя не является утверждением о числах, она не является утверждением вообще. Это строка, выводимая в ПА.

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

5
Вы хотите сказать, что строка "2*2=4" интерпретируется в модели, а строка "1234567=ProofNumber(7654321)" - нет?

6
Главное - не говорите, что ТГ - "метатеорема метатеории"

1 Да
2 Скорее наоборот, ZF сложнее, и может не обладать свойствами которые имеет PA
3 Нет, утверждение "я недоказуемо" является строкой PA
Согласитесь что истинность очень длинной строки PA никого бы так не потрясла
Суть теоремы Геделя в том что она доказывает не истинность строки, а свойство PA; то есть нечисленно свойство
4 Из там можно ЗАПИСАТЬ. Но то что эта сдлинная строка выражает истинность - только в голове а не в PA
5 Я кажется понял
Гедель построил просто еще одну модель...

6 Еще раз формально своей позиции

A. Записанное по правилам PA длинное утверждение "я недоказуемо" евляется ТЕОРЕМОЙ PA (без мета) но недоказуемо. Его истинность, однако, доказывается внешними для PA методами

B. Теорема Геделя является теоремой о выводимости, а не о числах. ПОэтмоу она является МЕТА теоремой. Упрямцы могут отобразить все высказывания теоремы Геделя на числа и сказать что она является и ПРОСТО теоремой доказанной внешними для PA методами. ФОрмально они правы, но в таком виде эта теорема никого бы не заинтересовала

C. Утверждение что аналог теоремы Геделя может быть применет также к любой непротиворечивой аксимоатической системе с рекурсивным набором аксиом, включающей в себя PA - является МЕТА МЕТА теоремой.

[vc]

Вернемся к доказательству Геделя. Как выглядит утверждение "я недоказуемо" ?

G == not exists x: proof(x очень длинное выражение )

Not quite. What Godel proved was:

If theory T is consistent, then G (sentence) is not a theorem of T

and

If T is omega-consistent, then ~G is not a theorem of T.

(Thre omega restriction was later removed by Rosser).

The G definition:

T |- G <=> ~ [] G, where []G means "G is a theorem in T"

He did not use the notion of 'truth' in his reasoning.


VC

[vc]

2 Скорее наоборот, ZF сложнее, и может не обладать свойствами которые имеет PA

PA is 'equivalent' to ZFC without the Axiom of Infinity.

VC

[Bobo]

1 Да
2 Скорее наоборот, ZF сложнее, и может не обладать свойствами которые имеет PA
3 Нет, утверждение "я недоказуемо" является строкой PA
Согласитесь что истинность очень длинной строки PA никого бы так не потрясла
Суть теоремы Геделя в том что она доказывает не истинность строки, а свойство PA; то есть нечисленно свойство
4 Из там можно ЗАПИСАТЬ. Но то что эта сдлинная строка выражает истинность - только в голове а не в PA
5 Я кажется понял
Гедель построил просто еще одну модель...

6 Еще раз формально своей позиции
...

1. Good!
2. Т.к. ZF является единственным формальным средством доказать непротиворечивость PA, то без етого средства у нас нет никаких формальных гарантий.
Интуитивные гарантии конечно есть. Но мне кажется, даже интуиционист должен быть последовательным - верить либо и в ZF и в PA, либо ни в то, ни другое.
3,4,5. Я бы сказал, ТГ демонстрирует, что в модели достаточно сложной теории есть утверждения о самой етой теории. Гедель НЕ строил модель - в етом то и ценность его доказательства - оно чисто формальное. Если бы сама ТГ не была истинным утверждением в стандартной модели, то ета модель не была бы моделью вовсе. Опять же, я согласен, что ТГ имеет мета-интерпретацию, но мета-теоремой не является.

6. Я понимаю Вашу позицию, нередко я и сам ее занимаю. Мне только кажется, Вы иногда путаете грань "теория/метатеория" с гранью "теория/модель". К примеру, слово "истинность" иногда употребляете в неподходяшем контексте.
Кстати, вопрос о том, как выглядит модель PA, к которой добавлено отрицание независимого утверждения - очень интересен. Особенно случай, когда ето утверждение "истинно" в смысле выводимо в ZF. Дело в том, что чтобы узнать как такая модель выглядит, надо пользоваться ZF на всю катушку. Сама PA построить свою модель, естественно не может. А если мы будем пользоваться ZF, то как быть с тем, что отрицание какой-то теоремы должно быть истинным в нашей модели?? Хотя, может быть ето чушь.

[Bobo]

....Такая теория непротиворечива, но омега противоречива....

Ето верно только для конкретной строки G.
Тем не менее, сушествуют строки, даюшие в результате противоречивую теорию. Они просто должны быть сложнее G.
К примеру, в теореме Крипке, которую я упоминал, непротиворечивость заменяется на сигма2-корректность: теория может вывести все истинные утверждения вида (exist n)(forall m):F(n,m).
Да, ето конечно, более сильное свойство, чем consistency, я неправильно написал, что более слабое.

[vc]

К примеру, в теореме Крипке, которую я упоминал, непротиворечивость заменяется на сигма2-корректность: теория может вывести все истинные утверждения вида (exist n)(forall m):F(n,m).
Да, ето конечно, более сильное свойство, чем consistency, я неправильно написал, что более слабое.

Actually, your first message was correct: the Kripke proof does not prove the undecidability of a Pi-1 statement and also cannot be used to prove the second incompleteness theorem which makes it *weaker*.

VC

[Bobo]

К примеру, в теореме Крипке, которую я упоминал, непротиворечивость заменяется на сигма2-корректность: теория может вывести все истинные утверждения вида (exist n)(forall m):F(n,m).
Да, ето конечно, более сильное свойство, чем consistency, я неправильно написал, что более слабое.

Actually, your first message was correct: the Kripke proof does not prove the undecidability of a Pi-1 statement and also cannot be used to prove the second incompleteness theorem which makes it *weaker*.

VC

Sure, the thoerem is weaker. But the condition is stronger. Goedel "requires" the theory to be consistent, Kripke "requires" it to be sigma-2 correct. It's a stronger requirement, isn't it?

[vc]

К примеру, в теореме Крипке, которую я упоминал, непротиворечивость заменяется на сигма2-корректность: теория может вывести все истинные утверждения вида (exist n)(forall m):F(n,m).
Да, ето конечно, более сильное свойство, чем consistency, я неправильно написал, что более слабое.

Actually, your first message was correct: the Kripke proof does not prove the undecidability of a Pi-1 statement and also cannot be used to prove the second incompleteness theorem which makes it *weaker*.

VC

Sure, the thoerem is weaker. But the condition is stronger. Goedel "requires" the theory to be consistent, Kripke "requires" it to be sigma-2 correct. It's a stronger requirement, isn't it?

Sorry, did not read carefully.

VC

[Bobo]

the Kripke proof does not prove the undecidability of a Pi-1 statement ...
VC

Hm, this question has been bothering me for some time, so maybe you can clear it out:
Can a pi-1 about numbers be proven undecidable at all?
Seems to me such a proof would prove that the statement is true.

Look:
Consider a sigma-1: (exist n):F(n).
If it is true then it's provable. Because if the n exists then we can present it and that would be a proof.
Consider a pi-1: (forall n):F(n).
Assume we have a proof of its undecidability.
It means we can't derive its negation. But the negation is a sigma-1, so if it was true, we could derive it. So the negation is false, and the statement is true.

Any mistakes in this reasoning?

[Dmitry67]

....Такая теория непротиворечива, но омега противоречива....

Ето верно только для конкретной строки G.
Тем не менее, сушествуют строки, даюшие в результате противоречивую теорию. Они просто должны быть сложнее G.

Нет
Если теория T непротиворечива
А теория T+X противоречива
То как я понимаю в теории T можно доказать not X, или я не прав ?

То есть недоказуемое высказывание или его отрицание не может стать причиной противоречия

[Bobo]

....Такая теория непротиворечива, но омега противоречива....

Ето верно только для конкретной строки G.
Тем не менее, сушествуют строки, даюшие в результате противоречивую теорию. Они просто должны быть сложнее G.

Нет
Если теория T непротиворечива
А теория T+X противоречива
То как я понимаю в теории T можно доказать not X, или я не прав ?

То есть недоказуемое высказывание или его отрицание не может стать причиной противоречия

Я имел в виду вот что:
Goedel: (Exists G) ((T |- G) -> ~Con(T)) & ((T |- ~G) -> ~OmegaCon(T))
Rosser: (Exists X) ((T |- X) -> ~Con(T)) & ((T |- ~X) -> ~Con(T))

Если вместо G взять более сложную формулу X, то способность теории доказать ее отрицание будет означать противоречивость (без омега).

[vc]

the Kripke proof does not prove the undecidability of a Pi-1 statement ...
VC

Hm, this question has been bothering me for some time, so maybe you can clear it out:
Can a pi-1 about numbers be proven undecidable at all?
Seems to me such a proof would prove that the statement is true.

Look:
Consider a sigma-1: (exist n):F(n).
If it is true then it's provable. ?

In FOL, yes, but of course not in PA.

VC

[Bobo]

the Kripke proof does not prove the undecidability of a Pi-1 statement ...
VC

Hm, this question has been bothering me for some time, so maybe you can clear it out:
Can a pi-1 about numbers be proven undecidable at all?
Seems to me such a proof would prove that the statement is true.

Look:
Consider a sigma-1: (exist n):F(n).
If it is true then it's provable. ?

In FOL, yes, but of course not in PA.

VC

Oh, I see... in PA even a quantifier-free statement can be undecidable, right?
E.g. Con(PA)

[Bobo]

In FOL, yes, but of course not in PA.

VC

Oh, I see... in PA even a quantifier-free statement can be undecidable, right?
E.g. Con(PA)

Well, Con(PA) is not really quantifier free. It's a Pi-1.
It's negation is a Sigma-1 and looks like
(exist n)(n=ProofNumber("0=1"))
that is unprovable.
But I don't believe ~Con(PA) is true.
Could you show me a really true unprovable Sigma-1?

[vc]

In FOL, yes, but of course not in PA.

VC

Oh, I see... in PA even a quantifier-free statement can be undecidable, right?
E.g. Con(PA)

Well, Con(PA) is not really quantifier free. It's a Pi-1.
It's negation is a Sigma-1 and looks like
(exist n)(n=ProofNumber("0=1"))
that is unprovable.
But I don't believe ~Con(PA) is true.
Could you show me a really true unprovable Sigma-1?

I can't 'cause PA is sigma_1 complete.

VC

[Dmitry67]

Ну так что вы думаете когда читаете что
exists такое множество X что blah blah blah (*)
Что такое множество СУЩЕСТВУЕТ или что Выводима строка (*) ?

PS
Никто не знает нет ли прогресса в токазательстве непротиворечивости теории множеств ?
Если теории, более мощные чем теория множеств, то есть относящиеся к теории множеств как последняя относится к PA ?

[vc]

Никто не знает нет ли прогресса в токазательстве непротиворечивости теории множеств ?

The second GT is sort of about impossibility of the proof.

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

I do not think so. There are alternative set axiomatizations but ZFC is the mainstream.

Also, there is so called "category theory" but it's not more powerful, just different. Besides, it's unclear whether it offers any foundational advantage in comparison to ZFC.

VC

[Bobo]

Ну так что вы думаете когда читаете что
exists такое множество X что blah blah blah (*)
Что такое множество СУЩЕСТВУЕТ или что Выводима строка (*) ?

PS
Никто не знает нет ли прогресса в токазательстве непротиворечивости теории множеств ?
Если теории, более мощные чем теория множеств, то есть относящиеся к теории множеств как последняя относится к PA ?

Я думаю, что говоряшему известны модели формальной системы, которую он использует, в которых такое множество есть. Если же говоряший приводит доказательство, то я в добавок убеждаюсь, что формула выводима.
Я никогда не буду спрашивать говоряшего, о какой конкретно модели идет речь. Ето не важно.
Но есть более интересный случай. Вы знаете об одной модели, а я о другой. В каждой из них некое утверждение истинно. Однако, с точки зрения Вашей модели ето утверждение в моей модели ложно.
К примеру, я оперирую щетной моделью ZF, и говорю Вам (у которого стандартная модель): "континуумы есть". Вы говорите: "согласен, но хочу увидеть пример". Я вам показываю континуум, а Вы говорите "никакой ето не континуум".
Теперь представьте, что Вы используете стандартную модель PA, а я - нестандартное расширение: модель PA + ~Con(PA). Вы: "2*2=4", я :"да", вы: "Великая Теорема Ферма", я:"да". И тут я чисто для поддержания разговора заявляю: "~Con(PA)". Так же и подраться можно

И как при таком раскладе с инопланетянами контакт устанавливать?

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

The second GT is sort of about impossibility of the proof.

Just "sort of". It actually says that if we do prove that (e.g. by presenting a model), that would mean ZF is inconsistent.

Btw, by "category theory" do you mean the so called "abstract nonsense" ("meta-algebra")? I never heard it was considered a Foundations thing.

[vc]

...

The second GT is sort of about impossibility of the proof.

Just "sort of". It actually says that if we do prove that (e.g. by presenting a model), that would mean ZF is inconsistent.

Well, "sort of" was a poor attempt at irony.

Actually the second GT states that a formal system cannot prove its own consistency, or in other words, the statement "T is consistent" cannot be proved in T. You're right in saying that one necessary condition is that T be consistent, otherwise everything is provable in T.

Btw, by "category theory" do you mean the so called "abstract nonsense" ("meta-algebra")? I never heard it was considered a Foundations thing.

Yep, that's the one and yes it was[is].

VC

[Dmitry67]

По поводу прогресса, недавно чуть не доказали противоречивость ZF

Это был бы полный ПЦ

ВОзвращаясь к физике.
Мы стали говорить о моделях. Математика это наука о моделях или строках ?
Если мы говорим не о чистой математике а о математике в физике, то мы подразумеваем что есть ИСТИННАЯ модель соответствующая физической реальности. Разные модели в физике называются интерпретациями.
Если есть истинная модель то видимо и числа существуют на самом деле...

[Dmitry67]

Еще одно замечание

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

Когда мы работаем на мета уровне, мы используем наивную теорию множеств. Мы можем рассуждать о нестандартных моделях.

Но насколько применимы наши рассуждения к нестандартным моделям если мыслить мы можем только в рамках стандартных моделей ?