Теорема Геделя и вера

[Tigrius]

Можно, неформально, определить функцию как правило сопоставляющее каждому значению аргумента значение функции. Это определение имеет смысл.

It's not a definition. What's an 'argument' ? What's a 'function' ?

If you want to say that a function is a rule mapping one value to another (assuning there is an agreement as to what a 'value' and a 'rule' are), then according to your definition

1->2, 1->3, 1->4

is a 'function' which is clearly not true.

Нужно объяснить что такое аргумент и т.д. Но суть не в этом, конечно. Если Вы даёте строгое формальное определение объекта, не объясняя его смысл, человеку никогда не работавшему с этим объектом, то он ничего не поймет.

Можно объяснить теорему Геделя о неполноте неспециалисту на пальцах, совсем не пользуясь формальными определениями. С другой стороны, требование к простоте изложения не оправдывает ошибки в тексте (тот факт, что теория аксиоматизируемая, ключевой для теоремы Геделя).

Все, ухожу дифференцировать ростки функций (c) г-н. Вектор.

[Dmitry67]

GT is an ordinary theorem, there is nothing "meta" about it. The Enderton book or "Torkel Franzén. Gödel's Theorem: An Incomplete Guide to its Use and Abuse" might help in understanding it.

The theorem says nothing about 'truth' (although it can be interpreted in this way); the concepts of completness/consistency are purely syntactical, and the theorem 'talks' about provability, not truth (see the original, or any of the two books above).

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

Частично Вы правы

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

Итак у нас есть два паралельных языка, все утверждения теории отображены в числа

Наконец, апофеоз, два языка сталкиваются. Нечто вроде диагонального метода. Все это наращивается до понятия выводимости, и далее строится утверждение, которого говорит 'я недоказуемо' (я упрощаю опуская момент о w-непротиворечивости). На языке числе же это утверждение просто неинтересное и длинное утверждение о числах

Если оно доказуемо, то оно истинно, но оно как раз говорит о своей невыводимости. значит, оно должно быть ложно. Противоречие. Значит, оно недоказуемо

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

На мета языке это будет утчерждение о неполноте теории, а на эквивалентном арифметическом - просто утверждение о числах. В этом смысле Теорема Геделя может быть названа арифметической теоремой. Однако, эта арифметическая теорема не может бsть доказана арифметически !

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

[MaxSt]

хмм... а вера-то тут причем?

[Bobo]

Наконец, теорема, приведенная в Wikipedia, ложна:

For any consistent formal theory that proves basic arithmetical truths, it is possible to construct an arithmetical statement that is true but not provable in the theory. That is, any consistent theory of a certain expressive strength is incomplete.

Теория должна быть конечно аксиоматизируемой (или скажем, множество аксиом должно быть перечислимым). Слово "formal" такого смысла не несет (оно обычно значит, что теория рассматривается с точки зрения мат. логики).

Вы неправы.
Достаточно, чтоб теория содержала аксиомы Пеано, и именно это там и сказано: proves basic arithmetical truths.

[Bobo]

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

Дима, есть 3 принципиально разные формулировки и доказательства ТГ.
Одно из них полностью формально. Его Вы читали?
Там нет ничего подобного тому, что Вы написали про "истинность". Слова "истинность" там вообще нет.
Con(T) => Exists G: ~(T|-G) AND ~(T|-~G)
Где здесь что-то про истинность?
Непротиворечивость - понятие чисто формальное.
Не путать с корректностью. А корректности ТГ не требует.

Есть другая формулировка, которую обычно подают популярно. Это уже не ТГ, а ее интерпретация на теор-модельном языке:
Correct(T) => Exists "G": G AND ~(T|-"G")
где "G"- строка, G - ее интерпретация, высказываение, которое может быть истинным.
Смешивают модельные и формальные термины, не предупреждая читателя, и у читателя создается ложное впечатление, что ТГ - это "метатеорема". И википедия вот тоже в мета-форме подает.

[Bobo]

И, еще:
Если почитать доказательство Второй ТГ, то можно увидеть, что там требуется, чтоб доказательство Первой ТГ формализовалось в данной теории.
То есть все доказательство Первой ТГ формально и не содержит ничего про "истинность".
Таким образом, требования к теории формальны, утверждение теоремы - формально, доказательство - формально.
Чем же она "мета" теорема?

[Bobo]

...
Итак у нас есть два паралельных языка, все утверждения теории отображены в числа...

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

[Tigrius]

Наконец, теорема, приведенная в Wikipedia, ложна:

For any consistent formal theory that proves basic arithmetical truths, it is possible to construct an arithmetical statement that is true but not provable in the theory. That is, any consistent theory of a certain expressive strength is incomplete.

Теория должна быть конечно аксиоматизируемой (или скажем, множество аксиом должно быть перечислимым). Слово "formal" такого смысла не несет (оно обычно значит, что теория рассматривается с точки зрения мат. логики).

Вы неправы.
Достаточно, чтоб теория содержала аксиомы Пеано, и именно это там и сказано: proves basic arithmetical truths.

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

[vc]

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

There is no such 'theory'. A formal theory is suposed to have a recursively enumerable set of axioms. While a set of all true statements in N is complete and consistent, it's not r.e.

[Tigrius]

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

There is no such 'theory'. A formal theory is suposed to have a recursively enumerable set of axioms. While a set of all true statements in N is complete and consistent, it's not r.e.

I wrote about that in my previous post. The words "formal theory" usually just mean a theory considered in formal logic. They do not mean that the set of axioms is enumerable.

[vc]

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

There is no such 'theory'. A formal theory is suposed to have a recursively enumerable set of axioms. While a set of all true statements in N is complete and consistent, it's not r.e.

I wrote about that in my previous post. The words "formal theory" usually just mean a theory considered in formal logic. They do not mean that the set of axioms is enumerable.

What specific theory do you have in mind whose axiom set is not recursively enumerable and its model is N ?

[Tigrius]

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

There is no such 'theory'. A formal theory is suposed to have a recursively enumerable set of axioms. While a set of all true statements in N is complete and consistent, it's not r.e.

I wrote about that in my previous post. The words "formal theory" usually just mean a theory considered in formal logic. They do not mean that the set of axioms is enumerable.

What specific theory do you have in mind whose axiom set is not recursively enumerable and its model is N ?

Множество всех утверждений истинных в стандартной модели арифметики.

[Bobo]

Наконец, теорема, приведенная в Wikipedia, ложна:

For any consistent formal theory that proves basic arithmetical truths, it is possible to construct an arithmetical statement that is true but not provable in the theory. That is, any consistent theory of a certain expressive strength is incomplete.

Теория должна быть конечно аксиоматизируемой (или скажем, множество аксиом должно быть перечислимым). Слово "formal" такого смысла не несет (оно обычно значит, что теория рассматривается с точки зрения мат. логики).

Вы неправы.
Достаточно, чтоб теория содержала аксиомы Пеано, и именно это там и сказано: proves basic arithmetical truths.

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

Да, согласен, надо требовать перечислимость множества аксиом.
Еще, в эту формулировку надо добавить "theory that proves basic arithmetical truths... and does not prove any falsehoods", т.е. потребовать корректности. Иначе нельзя будет построить истинное недоказуемое высказывание - consistency для этого недостаточно.
Тогда теорема вроде станет верной, но это все равно не теорема Геделя, а более слабая теорема, следствие из ТГ для корректных теорий.

[Dmitry67]

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

Дима, есть 3 принципиально разные формулировки и доказательства ТГ.
Одно из них полностью формально. Его Вы читали?
Там нет ничего подобного тому, что Вы написали про "истинность". Слова "истинность" там вообще нет.
Con(T) => Exists G: ~(T|-G) AND ~(T|-~G)
Где здесь что-то про истинность?
Непротиворечивость - понятие чисто формальное.

Интересно, если в сети формальное доказательство ТГ? Если найдете хорошее, киньте ссылкой PLS, я там выделю место, где используются мета методы.

А, пока Вы ищите, согласитесь пока с тем что, если мы не выходим в мета уровень, то Con(T) является лишь очень длинным утверждением о числах, НИКАК не связанным с противоречивостью или непротиворечивостью Пеано

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

[Bobo]

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

Дима, есть 3 принципиально разные формулировки и доказательства ТГ.
Одно из них полностью формально. Его Вы читали?
Там нет ничего подобного тому, что Вы написали про "истинность". Слова "истинность" там вообще нет.
Con(T) => Exists G: ~(T|-G) AND ~(T|-~G)
Где здесь что-то про истинность?
Непротиворечивость - понятие чисто формальное.

Интересно, если в сети формальное доказательство ТГ? Если найдете хорошее, киньте ссылкой PLS, я там выделю место, где используются мета методы.

А, пока Вы ищите, согласитесь пока с тем что, если мы не выходим в мета уровень, то Con(T) является лишь очень длинным утверждением о числах, НИКАК не связанным с противоречивостью или непротиворечивостью Пеано

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

Доказательство есть в сети конечно есть, но мне лень для Вас его искать. Я скачал когда-то оригинальное доказательство Геделя, точнее его перевод на английский. Оно малопонятное из-за устаревшей и нестандартной символики и терминологии. Впридачу, вообще непросто в тонкостях разобраться в формальном доказательстве ТГ. Оно намного сложнее, чем доказательство тех "модельных суррогатов" ТГ, в которых говорится про "истинное, но недоказуемое утверждение" (и которые действительно мета-теоремы) .
Я не знаю, что Вы понимаете под мета-методами, но модельных (семантических) методов в формальном доказательстве ТГ нет.

Вы считаете, что если теория может сказать что-то о себе - то это "мета" утверждение? Почему? Ведь теория говорит о строках и выражается в строках. Утверждение о строках может быть утверждением о теории.

[Dmitry67]

Вы считаете, что если теория может сказать что-то о себе - то это "мета" утверждение? Почему? Ведь теория говорит о строках и выражается в строках. Утверждение о строках может быть утверждением о теории.

Если теория строк, то да
Но мы говорили о аксимматики Пеано, которая говоряит о числах и ни о чем больше
Все слова непротиворечимо выводимо недоказуемо истинно 'имеет модель' итд не являются утвержениями о числах, и следовательно, являются выходом в мета уровень

[vc]

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

There is no such 'theory'. A formal theory is suposed to have a recursively enumerable set of axioms. While a set of all true statements in N is complete and consistent, it's not r.e.

I wrote about that in my previous post. The words "formal theory" usually just mean a theory considered in formal logic. They do not mean that the set of axioms is enumerable.

What specific theory do you have in mind whose axiom set is not recursively enumerable and its model is N ?

Множество всех утверждений истинных в стандартной модели арифметики.

Ok, so you insist, as you did earlier, on calling such formal system a theory. That's fine, but what's the use of the theory if you cannot prove anything in it in a finite number of steps ?

[vc]

Наконец, теорема, приведенная в Wikipedia, ложна:

For any consistent formal theory that proves basic arithmetical truths, it is possible to construct an arithmetical statement that is true but not provable in the theory. That is, any consistent theory of a certain expressive strength is incomplete.

Теория должна быть конечно аксиоматизируемой (или скажем, множество аксиом должно быть перечислимым). Слово "formal" такого смысла не несет (оно обычно значит, что теория рассматривается с точки зрения мат. логики).

Вы неправы.
Достаточно, чтоб теория содержала аксиомы Пеано, и именно это там и сказано: proves basic arithmetical truths.

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

Да, согласен, надо требовать перечислимость множества аксиом.

I think you misunderstood the author -- he apparently insists on just the opposite: that r.e. is not needed.

Еще, в эту формулировку надо добавить "theory that proves basic arithmetical truths... and does not prove any falsehoods", т.е. потребовать корректности. Иначе нельзя будет построить истинное недоказуемое высказывание - consistency для этого недостаточно.
Тогда теорема вроде станет верной, но это все равно не теорема Геделя, а более слабая теорема, следствие из ТГ для корректных теорий.

I am not sure what you trying to say by the above.

[vc]

Вы считаете, что если теория может сказать что-то о себе - то это "мета" утверждение? Почему? Ведь теория говорит о строках и выражается в строках. Утверждение о строках может быть утверждением о теории.

Если теория строк, то да
Но мы говорили о аксимматики Пеано, которая говоряит о числах и ни о чем

PA do not 'talk' about anything, they are just a set of axioms inspired by what's known about N. There are a number of alternative models satisfying PA, in fact, infinitely many, and N is just one of them.

[Bobo]

Наконец, теорема, приведенная в Wikipedia, ложна:

For any consistent formal theory that proves basic arithmetical truths, it is possible to construct an arithmetical statement that is true but not provable in the theory. That is, any consistent theory of a certain expressive strength is incomplete.

Теория должна быть конечно аксиоматизируемой (или скажем, множество аксиом должно быть перечислимым). Слово "formal" такого смысла не несет (оно обычно значит, что теория рассматривается с точки зрения мат. логики).

Вы неправы.
Достаточно, чтоб теория содержала аксиомы Пеано, и именно это там и сказано: proves basic arithmetical truths.

Множество всех утверждений истинных в стандартной модели арифметики --- полная непротиворечивавая теория, являющаяся расширением PA.

Да, согласен, надо требовать перечислимость множества аксиом.

I think you misunderstand the author -- he apparently insists on just the opposite: that r.e. is not needed.

I hope I did not misunderstand. He was saying that the wiki version of GT is wrong because it does not demand enumerability of the axiom set. And he gave a counterexample to prove that enumerability is a necessary condition.
Am I correct, Tigrius?

Еще, в эту формулировку надо добавить "theory that proves basic arithmetical truths... and does not prove any falsehoods", т.е. потребовать корректности. Иначе нельзя будет построить истинное недоказуемое высказывание - consistency для этого недостаточно.
Тогда теорема вроде станет верной, но это все равно не теорема Геделя, а более слабая теорема, следствие из ТГ для корректных теорий.

I am not sure what you trying to say by the above.

I am trying to say that the following (that is often offered as semantical version of GT) is not generally true:
Con(T) => Exists "G": G and ~(T|-"G")
There exist consistent theories that have the same model of the language as PA, but can prove falsehoods. For such theory the above statement is false.
The correct statement would be
Correct(T) => Exists "G": G and ~(T|-"G")
where Correct(T) means Forall "F": T|-"F" => F.
Of course neither the condition nor the implication of the theorem is expressible in T.
Note that obviously Correct(T) => Con(T), but not the other way.
The genuine (formal) GT says nothing about "unquoted" (pun intended) statements. And it doesn't demand correctness, only consistency.

[Bobo]

Вы считаете, что если теория может сказать что-то о себе - то это "мета" утверждение? Почему? Ведь теория говорит о строках и выражается в строках. Утверждение о строках может быть утверждением о теории.

Если теория строк, то да
Но мы говорили о аксимматики Пеано, которая говоряит о числах и ни о чем больше

Я вынужден повторять vc:
Аксиоматика Пеано говорит о строках типа s(s(0))+s(s(0))=s(s(s(s(s(0))))).

Все слова непротиворечимо выводимо недоказуемо истинно 'имеет модель' итд не являются утвержениями о числах, и следовательно, являются выходом в мета уровень

"непротиворечимо", "выводимо", "недоказуемо" - утверждения о строках языка, т.е. утверждения теории.
А вот "истино" - нет. "Истино" не формализуется, а "доказуемо" - формализуется.
Истинность в ПА не выразима в ПА, но выразима в ZFC(ZF?).
Слово "истинно" действительно является выходом на мета-уровень.
Но ТГ его не использует.

Вы еще заметили, что в "теории множеств нет такой путеводной нити как истинность". Это интересное наблюдение.
Дело в том, что у ZFC просто нет общепринятой модели. Под "истинностью" в ZFC обычно понимают доказуемость.
ТГ верна для ZFC. Но в виде "существует истинное, но недоказуемое высказывание" ее формулировать для ZFC просто неприлично.

[Dmitry67]

Oh-la-la, у нас даже не два языка появилось, а три.

1. Утверждения о числах (то есть я рассматриваю теорию и ее стандартную модель)
2. Строки. То есть можно вообще забыть что перед нами числа и просто рассматривать выводимость строк. Что обозначают переменные, в этом случае можно вообще не интересоваться
3. Веря в то, что за всем этим стоит некая объективная реальность, говорить о выводимости и истинности. На этом уровне появляются интересные феноменты типа геделевского 'Я недоказуемо' - это утверждение недоказуемо, но на самом деле истинно

Однако, возвращаясь к тому что Вы написали,

"непротиворечимо", "выводимо", "недоказуемо" - утверждения о строках языка, т.е. утверждения теории.

совершенно неправильно
Для простоты ограничимся словом "выводимо". Оно по отношении к теории является Мета.

Говоря языком 1, высказыванием теории Пеано является некое утверждение о числах
Говоря языком 2, высказыванием теории Пеано является строка (составлянная определенным образом)

Утверждение ''2+2=4' выводимо' не является ни числом, ни корректной строкой теории (потому что среди символов теории нет символа 'выводимо' (только не говорите про Con(T), хорошо? ))

Поэтому, 2+2=4 является теоремой
2+2=4 доказуемо является метатеоремой

[Bobo]

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

совершенно неправильно
Для простоты ограничимся словом "выводимо". Оно по отношении к теории является Мета.

да нет же, оно выразимо в теории. это чисто синтаксическое высказывание, о свойствах строк.

Говоря языком 1, высказыванием теории Пеано является некое утверждение о числах
Говоря языком 2, высказыванием теории Пеано является строка (составлянная определенным образом)

Язык 2 обычно называют теорией, а Язык 1 - моделью.

Утверждение ''2+2=4' выводимо' не является ни числом, ни корректной строкой теории (потому что среди символов теории нет символа 'выводимо' (только не говорите про Con(T), хорошо? ))

Конечно же оно является корректной строкой. Как бы Гедель доказал некорректную строку??

""2+2=4" истинно" - вот это уже метатеорема.

[tau797]

2+2=4 доказуемо является метатеоремой

""2+2=4" истинно" - вот это уже метатеорема

Вы, по-моему, с Дмитрием говорите об одном и том же (я не имею в виду, что истинность и выводимость - это одно и то же, я просто о том, что и то, и другое высказывание - это высказывание о формальной теории, причем ни символ выводимости, ни символ истинности в саму нее не входят), но просто не хотите понять друг друга (лишь бы поспорить )

[Bobo]

Нет, Тау, разница принципиальная.