НГУ
http://forum.nsu.ru/

Есть ли основания для посягательств на основания?
http://forum.nsu.ru/viewtopic.php?f=18&t=22427
Страница 2 из 2

Автор:  palaisien [ Вт май 24, 2011 6:55 pm ]
Заголовок сообщения: 

Pavel E. Alaev писал(а):
Смысл был в том, что если мы хотим, например, проверять на компьютере доказательства в теории конечных графов, то в большинстве случаев можем ограничиться поиском доказательств в PA. А поскольку PA наверняка непротиворечива, то вопрос о противоречивости оснований математики оказывается тут вообще ни при чём. Точно так же во многих других областях математики используется лишь ограниченные фрагменты ZFC. Впрочем, он и в случае работы со всей ZFC не играет особой роли. Автоматический поиск доказательств на компьютерах - интересная область, в которой ключевыми являются другие проблемы.


Означает ли это, что можно эффективно отделить это "большинство случаев"?

Автор:  Alexandr [ Ср май 25, 2011 6:05 am ]
Заголовок сообщения: 

Пмсм, это `большинство случаев' не то что эффективно, его вообще хоть как-то отделить не получится. Выше я давал ссылку на теоремы теории графов, котороые ни то что в РА, они в ZFC не доказуемы. А как-то хорошо отделить доказуемые и недоказуемые в ZFC утверждения люди пытаются давно и до полной победы далеко. Единственное, что, мне кажется, можно тут сказать, что если закодировать теорию графов в арифметику, то множество её теорем, доказуемых в PA, будет эффективно перечислимо, дополнение этого множества таковым не будет. Более того, в этом дополнении будут как истинные недоказуемые теоремы, так и ложные теоремы (т.е. нетеоремы), а уж об отделимости этих множеств люди мечтают давненько.

Автор:  Pavel E. Alaev [ Чт май 26, 2011 4:19 pm ]
Заголовок сообщения: 

palaisien писал(а):
Означает ли это, что можно эффективно отделить это "большинство случаев"?

Вопрос можно превратить в задачу со строгой формулировкой. Формально PA и ZFC - теории в разных языках, хотя по смыслу PA является частью ZFC. Чтобы сделать это формально верным, можно добавить в язык ZFC предикат N(x) для множества натуральных чисел и операции сложения и умножения на этом множестве, получив теорию ZFC'. Поскольку этот предикат и операции выразимы формулами в исходном ZFC, такая добавка ничего по существу не изменит (мы получим т.н. консервативное расширение ZFC), то есть ZFC и ZFC' будут по сути одной и той же теорией. В частности, будет существовать очевидный алгоритм, сводящий вопрос об истинности предложения в одной теории к вопросу об истинности в другой.

Далее, можно немного переделать аксиомы PA так, чтобы они относились к множеству N(x) со сложением и умножением, получив теорию PA'. Вновь теории PA и PA' будут по сути одной и той же теорией. Теперь PA' будет уже формальной подтеорией ZFC', и исходную задачу можно свести к вопросу о сложности множества предложения языка PA', лежащих в ZFC' \ PA'.

Легко показать, что оно будет неразрешимо, то есть не будет существовать алгоритма, который бы, получая на вход предложение, мог бы ответить, лежит оно в этом множестве или нет. Чтобы доказать это, можно взять предложение Con(PA') языка PA', выражающее, что PA' непротиворечиво. Мы знаем, что оно лежит в ZFC', и не лежит в PA' по теореме Гёделя. Затем можно рассмотреть отображение, которое предложению B языка PA' сопоставит предложение B & Con(PA'). Если B лежит в ZFC', то второе предложение попадёт в ZFC' \ PA', если не лежит, то не попадёт. Тем самым мы сведём к нашему множеству множество следствий из ZFC' в языке PA', которое неразрешимо ещё по одной теореме Гёделя.

Автор:  Pavel E. Alaev [ Чт май 26, 2011 8:25 pm ]
Заголовок сообщения: 

Собственно, последний абзац - это доказательство того общего факта, что если T1 - неразрешимая теория и T2 - её подтеория, отличная от неё самой, то T1 \ T2 - тоже неразрешимое множество предложений.

Страница 2 из 2 Часовой пояс: UTC + 7 часов
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/