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

[vc]

.....

2 ok, первая теорема Геделя доказывается относительно аксиоматики Пеано.
Я думаю Вы согласитесь что теорема Геделя не является теоремой, потому что в арифметике пеано теоремой является утверждение о *числах*

Well, I am sorry but I'll disagree. There is nothing "meta" about the GT with respect to how it's proved [by Goedel]. The proof shows how to construct an undecidable statement, encoded as an integer, and the proof is an ordinary mathematical proof, no different say from proving the Pythagorean Theorem..

...
Она является метатеоремой, то есть утверждением о свойствах арифметики Пеано

I am not sure what you mean by "meta" but the GT is as much about the PA's properties as the PT is about the right triangle properties. Should we call, then, the PT also a "metatheorem" ? Maybe you are using "meta" in some philosophical sense ?


VC

[vc]

That's quite a leap. The first GT makes sense only within the formal system equivalent to PA. It's unclear how you are going to map the entire world to PA.

Только сейчас ошибку заметил
1 GT (точнее ее аналог) имеет sense также в ЛЮБОЙ другой аксиоматической системе, если эта система ВКЛЮЧАЕТ в себя (а не ЭКВИВАЛЕНТНА) PA.

Sure, I was sloppy in my wording, of course any consistent extension of PA is incomplete. One can construct, though, for example, a formal system of reals, without arithmetic, which will be consistent and complete.

VC

[Bobo]

... One can construct, though, for example, a formal system of reals, without arithmetic, which will be consistent and complete.

Кстати, я совсем недавно узнал, что если из ПА выбросить умножение, то получится полная, непротиворечивая теория с вычислимым предикатом истинности. (Presburger's Arithmetic). Доказательство этого весьма нетривиально, но оно в свое время послужило причиной веры Гильберта в возможность построения Оснований.
Я-то раньше думал, что вся беда только в индукции...

[Dmitry67]

... One can construct, though, for example, a formal system of reals, without arithmetic, which will be consistent and complete.

Кстати, я совсем недавно узнал, что если из ПА выбросить умножение, то получится полная, непротиворечивая теория с вычислимым предикатом истинности. (Presburger's Arithmetic). Доказательство этого весьма нетривиально, но оно в свое время послужило причиной веры Гильберта в возможность построения Оснований.
Я-то раньше думал, что вся беда только в индукции...

А разве умножение в Пеано не определяется через сложение ?

[Dmitry67]

Well, I am sorry but I'll disagree. There is nothing "meta" about the GT with respect to how it's proved [by Goedel]. The proof shows how to construct an undecidable statement, encoded as an integer, and the proof is an ordinary mathematical proof, no different say from proving the Pythagorean Theorem..

Maybe you are using "meta" in some philosophical sense ?
VC

Понятие meta для меня означает выразимость теоремы и доказуемость теоремы не выходя за рамки некоторой теории

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

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

Любое высказывание типа 'утверждение типа ... является недоказыемым' утверждением о числах не являются а являются утверждениеми о свойствах формальной арифметики и я их отношу к метатеоремам

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

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

Более того, можно представить себе упрямого ученого, который по каким то причинам НЕ ВЕРИТ в рассуждения мета уровня. Например, если этот ученый - интуиционист.Он будет согласен с формальным слоем и всеми теоремами. Однако на мета уровне в доказательстве используется принцип от противного, и, для него доказательства не состоится

Agreed ?

P.S. Sorry, на выходных буду в Каннах, отвечу в понедельник

[Bobo]

А разве умножение в Пеано не определяется через сложение ?

Нет. Более того, сложение не определяется через основные пеановские понятия (equality, successor, induction). Более того, через ети понятия не определяется даже отношение меньше. Минимальная фундаментальная по Геделю арифметика имеет знаки "<, +, *" в языке и соответствуюшие аксиомы.
Речь идет о языке первого порядка.

теоремой формальной арифметики является утверждение о числах и ничего больше

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

[vc]

А разве умножение в Пеано не определяется через сложение ?

Нет. Более того, сложение не определяется через основные пеановские понятия (equality, successor, induction). Более того, через ети понятия не определяется даже отношение меньше. Минимальная фундаментальная по Геделю арифметика имеет знаки "<, +, *" в языке и соответствуюшие аксиомы.
Речь идет о языке первого порядка.

This is not quite true. In the first-order formulation, there is no need for LESS("<") because it can be expressed via "+":

E.g.: (a < b ) : Ex(a+x+S(0))=b


VC

[Bobo]

А разве умножение в Пеано не определяется через сложение ?

Нет. Более того, сложение не определяется через основные пеановские понятия (equality, successor, induction). Более того, через ети понятия не определяется даже отношение меньше. Минимальная фундаментальная по Геделю арифметика имеет знаки "<, +, *" в языке и соответствуюшие аксиомы.
Речь идет о языке первого порядка.

This is not quite true. In the first-order formulation, there is no need for LESS("<") because it can be expressed via "+":

E.g.: (a < b ) : Ex(a+x+S(0))=b


VC

Correct, "less" is expressible through "+". Sorry.

[Dmitry67]

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

1
Более того, сложение не определяется через основные пеановские понятия (equality, successor, induction).

2
С таким же успехом можно сказать, что теоремы формальной арифметики напротив, никакого отношения к числам не имеют - они просто строки символов, выведенные по формальным правилам.

3
И теоремa Геделя в етом смысле есть именно теорема о формальных строках, помните строгую формулировку, не испорченную популяризаторами?
типа "Сушествует строка Г, такая что если Т выводит Г, то Т противоречива, а если Т выводит ~Г, то Т омега-противоречива".

4
Ето я на мета языке сказал, конечно, но прикол в том, что ето можно и высказать и доказать (тьфу, вывести) на языке T.

5
"полусемантическое" следствие теоремы Тарского о неопределимости истины, а также не помню чье чисто семантическое модельное доказательство).

1 см http://en.wikipedia.org/wiki/Peano_axioms#The_axioms
Addition, multiplication and the usual ordering can all be defined for the natural numbers N entirely in terms of the Peano axioms.

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

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

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

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

[vc]

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

1 см http://en.wikipedia.org/wiki/Peano_axioms#The_axioms
Addition, multiplication and the usual ordering can all be defined for the natural numbers N entirely in terms of the Peano axioms.

You'll take another train ;)

1. Their definition is a second-order formulation where the addition/multiplication axioms are theorems.

VC

[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 - является МЕТА МЕТА теоремой.