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

[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 ?