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

[Dmitry67]

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

Да нет, я не перемешиваю, отнюдь, я как раз стараюсь придерживаться пуританской строгости в данном вопросе

Еще раз. Выводимо обозначается таким значком |-
Это значек используется в математической логике, но в аксиоматике Пеано его НЕТ, там есть только операции определяемые аксиоматикой Пеано, а также => и not (к примеру). Мы считаем, что никакие определения не используются, то есть все обозначения типа + или > или OR раскрываются, хотя ниже я их буду использовать для краткости

Итак

A. 2+2=4 есть теорема
B. |- 2+2=4 есть метатеорема
Делаем финт ушами заменяя |- на Pf
C. Pf(2+2=4) есть теорема. Она может быть доказана чисто формальными методами и не содержит никаких мета

НО: эквивалентность B и С происходит по построению предиката Pf (существует доказательство), который так построен, чтобы работать как |-

То есть, пока Вы доказываете C, все тихо: Вы просто говорите какую аксиому и какое правило вывода использовали. Все формально. Я не могу даже слово вставить и пристыженно молчу

Вы доказали C. Я апплодирую а дальше лукаво прищурившись спрашиваю, а какое отношение это доказательство имеет к B. Тут Вы говорите - Ну как же ! По построению ! Начинаете размахивать руками и делать прочее blah-blah-blah, которое не сводимо к номерам аксиом и правил вывода.

Вот потому то оно и мета.
[/b]

[vc]

[quote="Dmitry67"]...

Еще раз. Выводимо обозначается таким значком |-
Это значек используется в математической логике, но в аксиоматике Пеано его НЕТ, там есть только операции определяемые аксиоматикой Пеано, а также => и not (к примеру). Мы считаем, что никакие определения не используются, то есть все обозначения типа + или > или OR раскрываются, хотя ниже я их буду использовать для краткости

Итак

A. 2+2=4 есть теорема
B. |- 2+2=4 есть метатеорема
Делаем финт ушами заменяя |- на Pf
C. Pf(2+2=4) есть теорема. Она может быть доказана чисто формальными методами и не содержит никаких мета

'2+2 = 4 is a theorem in PA', 'PA |- 2+2=4', 'Proof(2+2=4)' say exactly the same.

B. and C. do not make any obvious sense: ''2+2=4' is a theorem in PA' is a [meta]theorem ?

A proof in the GT can be encoded similarly to a formula encoding because a proof is just a finite sequence of formulas, there is nothing 'meta' about the encoding.

[Bobo]

Вот потому то оно и мета.
[/b]

ТГ и ее доказательство не содержат ничего, что невыразимо в теории. Значит она не мета, а обычная теорема.
Вы спрашиваете, почему выводимость формулы "Con(PA)" означает непротиворечивость арифметики? По той же причине, что выводимость "2+2=4" означает, что сумма чисел 2 и 2 есть число 4.
Потому что арифметика - модель PA.
Еще раз повторю. Если вы формулируете ТГ как "есть истинные утверждения о числах, не выводимые в PA" - то это мета-теорема по отношению к PA. Так как ее нельзя записать на языке PA.
Если же сформулировать ее как "в PA есть независимые формулы" - это будет теорема PA.

[Dmitry67]

Еще раз повторю. Если вы формулируете ТГ как "есть истинные утверждения о числах, не выводимые в PA" - то это мета-теорема по отношению к PA. Так как ее нельзя записать на языке PA.
Если же сформулировать ее как "в PA есть независимые формулы" - это будет теорема PA.

Даже второе метатеорема
"в PA есть независимые формулы" не выражается в аксиоматике Пеано, так как в ней нет понятия ни 'независимый', ни 'формула'
Приведенное утверждение можно запихнуть в ариметику с помощью геделизации построив предикаты типа Con(), Pf() итд, но тогда возникнет вопрос эквивалентности. Например, как доказать, что

из Pf(X) следует |- X ?

[Dmitry67]

'PA |- 2+2=4', 'Proof(2+2=4)' say exactly the same.

См то что я написал для BoBo
Как Вы докажете что 'PA |- 2+2=4' и 'Proof(2+2=4)' эквивалентны ?
По построению предиката Proof? Это blah blah blah, а не формализм

[vc]

'PA |- 2+2=4', 'Proof(2+2=4)' say exactly the same.

См то что я написал для BoBo
Как Вы докажете что 'PA |- 2+2=4' и 'Proof(2+2=4)' эквивалентны ?
По построению предиката Proof? Это blah blah blah, а не формализм

1. Let '%' be a synonym for '+'. Obviously, 2%2 is the same as 2+2.

Let 'Proof' be a synonym for '|-'. Obviously, Proof(x) is the same as |- x (unless by 'Proof' you mean something entirely different).


2. As was said before, a proof in PA is a sequence of formulas. Each formula is replaced with a G-number producing a sequence of numbers which is again replaced with a G-number. That's how you get from |- x to a G-number.

[vc]

...
"в PA есть независимые формулы" не выражается в аксиоматике Пеано, так как в ней нет понятия ни 'независимый', ни 'формула'

'Formula' is a word from the first-order logic vocabulary. A first-order language (variables, connectives, formulas, etc) is part of any first-order theory including PA. It's unclear what 'independent' means; the correct word is 'undecidable'.

[Bobo]

"в PA есть независимые формулы" не выражается в аксиоматике Пеано

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

Например, как доказать, что
из Pf(X) следует |- X ?

Как доказать, что из "х+2=4" следует, что если к х прибавить 2, то получится 4?
И вообще, как доказать, что символ "2" это число 2? По постороению, да?

[Dmitry67]

Господа, похоже, мы о разном говорим

proof(x) не является синонимом |- X
аргумент proof() является целым числом (геделевским кодом формулы X), а сам proof является кратким обозначением для очень длинной формулы с кванторами скобками и другими знаками (длиной в сотни, если не тысячи символов)

[vc]

Господа, похоже, мы о разном говорим

proof(x) не является синонимом |- X
аргумент proof() является целым числом (геделевским кодом формулы X), а сам proof является кратким обозначением для очень длинной формулы с кванторами скобками и другими знаками (длиной в сотни, если не тысячи символов)

Where's the G-number in 'Proof(2+2=4)' ?

If you mean, Proof(#(2+2=4)), or more generally Proof(x) where x is a G-number of some formula, then Proof(x) is an abbreviation of:

(E y) Prf(x,y)

Prf(x, y) = "y is a proof number for the formula x number". For details, see how Godel defines Prf(x,y) in about 45 steps.

[vc]

...
Как доказать, что из "х+2=4" следует, что если к х прибавить 2, то получится 4?
И вообще, как доказать, что символ "2" это число 2? По постороению, да?

x + 2 = 4 is not a theorem, but (E x) (x + 2 = 4) is. The proof is trivial.

"2" is a decimal numeral, a label for the natural number 2. It's just a convention like Roman II.

[Dmitry67]

Господа, похоже, мы о разном говорим

proof(x) не является синонимом |- X
аргумент proof() является целым числом (геделевским кодом формулы X), а сам proof является кратким обозначением для очень длинной формулы с кванторами скобками и другими знаками (длиной в сотни, если не тысячи символов)

Where's the G-number in 'Proof(2+2=4)' ?

If you mean, Proof(#(2+2=4)), or more generally Proof(x) where x is a G-number of some formula, then Proof(x) is an abbreviation of:

(E y) Prf(x,y)

Prf(x, y) = "y is a proof number for the formula x number". For details, see how Godel defines Prf(x,y) in about 45 steps.

Абсолютно верно. Я про это и говорю
Pf() есть очень длинная формула
Поэтому доказав
PF(#(X)) совершенно формально строго, сказать, что это доказывает |- X нельзя без слов про 'построение' Pf(), то есть совершив грех blah-blah-blah и взмахов руками

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

[vc]

Господа, похоже, мы о разном говорим

proof(x) не является синонимом |- X
аргумент proof() является целым числом (геделевским кодом формулы X), а сам proof является кратким обозначением для очень длинной формулы с кванторами скобками и другими знаками (длиной в сотни, если не тысячи символов)

Where's the G-number in 'Proof(2+2=4)' ?

If you mean, Proof(#(2+2=4)), or more generally Proof(x) where x is a G-number of some formula, then Proof(x) is an abbreviation of:

(E y) Prf(x,y)

Prf(x, y) = "y is a proof number for the formula x number". For details, see how Godel defines Prf(x,y) in about 45 steps.

Абсолютно верно. Я про это и говорю
Pf() есть очень длинная формула

Поэтому доказав
PF(#(X)) совершенно формально строго, сказать, что это доказывает |- X нельзя без слов про 'построение' Pf(), то есть совершив грех blah-blah-blah и взмахов руками

??? Prf(x, y) is a formalization of Hilbert's definition of derivation/proof as a sequence of formulas. Proof(X) = (E x) Prf(x, y) is a formalizm for '|-'. You are free to invent your own definitions of course but it would be hardly productive.

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

So you do not accept accept either of the incompletness theorems ?

[Dmitry67]

1
??? Prf(x, y) is a formalization of Hilbert's definition of derivation/proof as a sequence of formulas. Proof(X) = (E x) Prf(x, y) is a formalizm for '|-'. You are free to invent your own definitions of course but it would be hardly productive.

2
So you do not accept accept either of the incompletness theorems ?

1 Верно. Но 'formalization' таким образом являетися мета понятием.
То есть его результат совершенно строг
Но сам факт, что мы можем адекватно использовать данный механизм определяется на уровне 'наивной теории множеств', вот дескать если мы будет такой то значок заменять степенью i-того простого числа... ну итд

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

2 Я верю в эти теоремы

[vc]

1
??? Prf(x, y) is a formalization of Hilbert's definition of derivation/proof as a sequence of formulas. Proof(X) = (E x) Prf(x, y) is a formalizm for '|-'. You are free to invent your own definitions of course but it would be hardly productive.

2
So you do not accept accept either of the incompletness theorems ?

1 Верно. Но 'formalization' таким образом являетися мета понятием.
То есть его результат совершенно строг
Но сам факт, что мы можем адекватно использовать данный механизм определяется на уровне 'наивной теории множеств', вот дескать если мы будет такой то значок заменять степенью i-того простого числа... ну итд

The encoding/'arithmetization' Godel used is no different, in principle, than the one used to encode the letter 'A' with 33. What's 'meta' about such encoding ? Besides, no set theory, naive or otherwise, is used in the proof.

Я собственно об этом и талдычу. В ТГ есть элементы, не сводимые к формализму.

For example ?

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

The theorem is syntactic. It shows that there are strings(formulas) that cannot be derived(proved) using the theory axioms and derivation rules provided that such theory is consistent. Likewise, (A x) (x mod 2 = 0) is, by itself, a meaningless although syntactically correct string of characters unless interpreted as a statement about N.

2 Я верю в эти теоремы[/quote]

There is no need to -- there is a proof.

[Dmitry67]

1. used to encode the letter 'A' with 33. What's 'meta' about such encoding ?
2. Besides, no set theory, naive or otherwise, is used in the proof.

Я собственно об этом и талдычу. В ТГ есть элементы, не сводимые к формализму.

3. For example ?

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

Процесс доказательства выглядит так: Вы выходите к доске, молча пишете строку-доказательство. Я его проверяю, жму руку и мы расходимся, слова бессмысленны и излишни, а спорить не о чем.

Если для доказательства требуется ЛЮБОЙ другой элемент кроме дерева аксиом-правил вывода, то оно увляется МЕТА.

1. В частности "encode the letter 'A' with 33" есть blah-blah-blah, не выражаемое в виде номеров аксиом и правил вывода.
2. Отнюдь. Например, "очевидно, что всякую формулу можно геделизировать" есть мета утверждение, которое как минимум использует свойства счетных множест "наивным" образом
3. Я привел

[tau797]

Если для доказательства требуется ЛЮБОЙ другой элемент кроме дерева аксиом-правил вывода, то оно увляется МЕТА

Дима прав.

[vc]

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

There are many proof management systems, the beloved by computer folks proof tree being one of them. A proof tree can trivially be converted by topological sorting to a list/sequence with lemma/axiom Godel numbers acting as parent pointers.

Если для доказательства требуется ЛЮБОЙ другой элемент кроме дерева аксиом-правил вывода, то оно увляется МЕТА.

The proof representaion shape is irrelevant as long as it can be encoded by a natural number. In fact, Godel's proof sequence can be seen as a tree (see above).

1. В частности "encode the letter 'A' with 33" есть blah-blah-blah, не выражаемое в виде номеров аксиом и правил вывода.

In this case, the bulk of math prose is written in 'metalanguage', e.g. "Let x stand for any even natural number". Since all the expository math language is 'meta', one can easily get rid of the prefix and just use the word 'language'. What's the point of singling out one theorem proof out of many similar proofs and claiming that it alone uses a 'metalanguage' to explicate such proof while pretending that the rest somehow does not ? Besides, there is a simple formalism to express the idea that 'A' is encoded with 33 (it's called a function): ('A', 33).

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

1. It's as much of a 'metastatement' as saying that any letter can be mapped to a natural number. What's the difference ?

2. What particular axiom of any set theory do you have in mind ? Nothing except natural numbers is used for the encoding.

[Bobo]

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

[Dmitry67]

Арифметизация выражается в теории.
Арифметизатсия ето просто отображение строк теории в другие строки теории.

Дима, советую соглашаться.

Не соглашаюсь
Да, Арифметизация выражается в теории. Но сама ее идея - нет

Помните с чего начинается классическое доказательство Теоремы Геделя? С построения геделизации. Пожалуйста, постройте его не употребляя ничего кроме номеров аксиом и номеров правил Вывода, и Вы сами придете к пониманию того, что это МЕТА вещь

Чтобы было поконретнее, приведу пример
Фома неверующий утверждает что есть такая формула, что она выводима, но Pf(от ее геделевского номера) ложно. Как Вы его опровергните? Дайте идею доказательства.

[Dmitry67]

1
There are many proof management systems, the beloved by computer folks proof tree being one of them. A proof tree can trivially be converted by topological sorting to a list/sequence with lemma/axiom Godel numbers acting as parent pointers.

The proof representaion shape is irrelevant as long as it can be encoded by a natural number. In fact, Godel's proof sequence can be seen as a tree (see above).

В частности "encode the letter 'A' with 33" есть blah-blah-blah, не выражаемое в виде номеров аксиом и правил вывода.

2
In this case, the bulk of math prose is written in 'metalanguage',

3
What's the point of singling out one theorem proof out of many similar proofs and claiming that it alone uses a 'metalanguage' to explicate such proof while pretending that the rest somehow does not ?

4. What particular axiom of any set theory do you have in mind ? Nothing except natural numbers is used for the encoding.

1 Безусловно, по большому счету никакой разницы
2 Да
3 Point в том, что для теорем проза используется для лучшего понимания собеседником, комментариев и пояснения. Люди плохо понимают дерево вывода если не произнести не слова. Однако теоретически всю эту прозу можно убрать для теорем. А для метатеорем она является неотъемлемой частью доказательства и убрать ее нельзя
4 Неважно. Также не важно, использую ли я например => и Not, или not, AND, OR, есть ли у меня два квантора или Exists определен черз ALL итд

[vc]

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

Likewise, the incompleteness theorem proof can be fully written in the language of the theory whose incompleteness it proves because it does not use any constructs outside such language. It's an obvious fact for anyone who studied the original proof and its many alternative expositions.

4 Неважно. Также не важно, использую ли я например => и Not, или not, AND, OR, есть ли у меня два квантора или Exists определен черз ALL итд

Still, what particular set theory axioms have been used in the proof ?

[vc]

Да, Арифметизация выражается в теории. Но сама ее идея - нет

You can formalize a relation. Can you formalize the very idea of relation ? What's the difference ?

Помните с чего начинается классическое доказательство Теоремы Геделя? С построения геделизации. Пожалуйста, постройте его не употребляя ничего кроме номеров аксиом и номеров правил Вывода,

That's what the theorem proof does -- encodes various statements with natural numbers :

f(x) -> 76
g(t,m) -> 93
...
[f(x), g(t)] -> [76, 93] ->123
...
etc

Чтобы было поконретнее, приведу пример
Фома неверующий утверждает что есть такая формула, что она выводима, но Pf(от ее геделевского номера) ложно. Как Вы его опровергните? Дайте идею доказательства.

See the first GT proof.

[Dmitry67]

vc, есть машина Тьюринга, которой на вход поступает формальное доказательство арифметической теоремы в некоем заранее оговоренном виде, и на выходе она говорит, правильно ли доказательство или нет. То есть реальзует предикат Proof(x,y)

Такая машина может проверить только теоремы, метатеоремы она проверить не может - их нельзя подать на вход (но может однако проверить 'геделизированные' метатеоремы, например где |- X заменен на Pf(#X) )

Если ТГ не мета теорема, то ее можно подать на вход данной машине, правильно?

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

[Bobo]

Чтобы было поконретнее, приведу пример
Фома неверующий утверждает что есть такая формула, что она выводима, но Pf(от ее геделевского номера) ложно. Как Вы его опровергните? Дайте идею доказательства.

Это на каком языке Фома утверждает? Теории или модели? Вы путаете эти языки опять.
"формула выводима" - утверждение на языке модели. Оно может быть истинным или ложным.
"Pf(от ее геделевского номера)" - строка теории, которая не может быть ложной. Она может быть выводимой или нет.

Если под "Pf(от ее геделевского номера) ложно" Фома понимает "интерппретация "Pf(от ее геделевского номера)" в модели ложна", то это то же самое что "НЕ формула выводима", и Фома неправ по закону исключенного третьего.