НГУ

Форумы НГУ
Текущее время: Сб окт 19, 2019 10:28 pm

Часовой пояс: UTC + 7 часов




Начать новую тему Ответить на тему  [ Сообщений: 19 ]  На страницу Пред.  1, 2
Автор Сообщение
 Заголовок сообщения:
СообщениеДобавлено: Вт май 24, 2011 6:55 pm 
Не в сети
Частый гость

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


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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Ср май 25, 2011 6:05 am 
Не в сети
Плодовитый автор

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

_________________
Ненужность матана — не повод его не осилить


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Чт май 26, 2011 4:19 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
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', которое неразрешимо ещё по одной теореме Гёделя.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения:
СообщениеДобавлено: Чт май 26, 2011 8:25 pm 
Не в сети
Весьма плодовитый автор

Зарегистрирован: Чт сен 27, 2001 7:00 am
Сообщения: 1637
Собственно, последний абзац - это доказательство того общего факта, что если T1 - неразрешимая теория и T2 - её подтеория, отличная от неё самой, то T1 \ T2 - тоже неразрешимое множество предложений.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 19 ]  На страницу Пред.  1, 2

Часовой пояс: UTC + 7 часов


Кто сейчас на конференции

Сейчас этот форум просматривают: MSN [Bot] и гости: 4


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Перейти:  
Создано на основе phpBB® Forum Software © phpBB Group
Русская поддержка phpBB