Весенне обострение (P=/=NP?)

Такое ощущение, что уже создавал такую тему несколько лет назад, но найти её так и не смог. Либо не тут создавал, либо очень хотел создать, но не создал, либо просто с кем-то обсуждал, а теперь кажется, что это было на форуме. Если кто-то найдёт старую тему, я её объединю с этой.А обсудить хочется зависимость ZF(C) и P=/=NP. Интересны ваши соображения на эту тему. Может быть, есть уже канонические статьи?Для разжигания аппетита (и отчасти введения в курс дела) приведу ниже произвольный перевод отрывка из статьи Скота Аронсона, представляющий собой диалог Вас (Вы) и аксиом ZF+\neg Con(ZF) (Аксиомы). (\neg Con(ZF) --- предложение, отрицающее совместность ZF, --- его, как известно, можно сформулировать в логике (исчислении предикатов) первого порядка на языке теории множеств ZF.)Вы: Смотри, ты говоришь, что ZF несовместна, а из этого следует, что существует доказательство того, что 1+1=3. Можно мне взглянуть на это доказательство?Аксиомы: Я предпочитаю говорить о целых числах, которые кодируют доказательство. (На самом деле, о множествах, которые кодируют целые числа, которые кодируют доказательства. Но тут я позволю тебе расслабиться --- ты ведь всего лишь человек.)Вы: Тогда покажи мне целое число.Аксиомы: Без проблем, вот: Х.Вы: Какой ещё нахрен Х?Аксиомы: Просто Х, целое число, кодируемое множеством в универсуме, который я описываю.Вы: Но что такое Х как обычное целое число?Аксиомы: Нет, нет, нет! Говори-ка с аксиомами.Вы: Хорошо, позволь мне спросить тебя о числе Х. Оно больше или меньше биллиона? Аксиомы: Больше.Вы: Больше, чем 10^{10^{1,000,000,000}}-ое число Акермана?Аксиомы: Да, больше.Вы: А чему равно X^2+100?Аксиомы: Хмм, минутку... посмотрим... Y.Вы: Чёрт! Почему я не могу просто добавить аксиому для этих дурацких "нестандартных целых"? Попробую: для всех Х, Х принадлежит множеству, получающемуся из 0 при помощи...Аксиомы: Ха-Ха! Тут тебе логика первого порядка. Ты не можешь говорить о множествах объектов даже если эти объекты сами множества.Вы: Ааа! Я знаю, что ты врёшь не счёт доказательства 1+1=3, но я никогда не смогу тебя поймать.Аксиомы: Точно! Гёдель, как раз, и показал, что мы можем играть в эту игру вечно. Более того, бесконечная последовательность дурацких объектов, которые ты заставляешь меня находить --- X, Y и т.д. --- образуют потом модель этой нелепой теории ZF+\neg Con(ZF).Вы: Но откуда ты знаешь, что я рано или поздно не подловлю тебя на несовместности?Аксиомы: Потому что если ты подловишь, теорема о полноте говорит, что мы сможем обернуть это в несовместность исходных аксиом, что противоречит очевидному факту, что ZF совм... стоп, погоди! Мы не должны этого знать. [Аксиомы начали растворяться в луже несовместности.]