о Гёделе и Изабелле, take 2

[avva]

Написал длинную и подробную запись о: доказательстве Гёделя от 40-го года непротиворечивости аксиомы выбора, конструктивной вселенной, V=L, и недавней формализации этого доказательства Ларри Польсоном из Кембриджа, в формальной системе Isabelle (ссылки: описание док-ва; само док-во со всеми определениями, автоматически сгенерированное, больше 200 страниц). И ещё о том, как я попытался изучить эту самую Изабеллу попристальнее, но понял, что мне не хватает адекватного понимания лямбда-исчисления (которое уже давно пора изучить, мне мешает эта дырка) и языка ML, на к-м Изабелла написана.

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

Comments

Re: Извиняюсь за занудство,

[avva.livejournal.com]

По мат. логике в целом очень рекомендую A Mathematical Introduction to Logic (кажется, так) Enderton'а.

По теории множеств есть хорошая книга Levy "Set Theory" -- но большая и нелёгкая. Есть Кунена (Kunen) с тем же названием -- короче, покрывает немало материала, читабельная. Есть Jech'а с тем же названием - самая полная, но очень лаконичная и формальная. Это всё книги по теории множеств вообще.

Ещё вспоминается "Set Theory and the Continuum Problem" Смульяна (Smullyan) -- если я правильно помню, содержит и введение в теорию множеств. Смульяну нет равных в ясности и интересности изложения. Его же "Goedel's Incompleteness Theorems" - идеальная книга по теоремам о неполноте Гёделя -- light on formalism, yet suitably rigorous; and wonderfully readable and engaging.

Re: Извиняюсь за занудство,

[iliat.livejournal.com]

Уже нашел все в каталоге библиотеки Торонтского университета.
Побегу брать.
Спасибо большое !

Re: Извиняюсь за занудство,

[malenkiy-scot.livejournal.com]

Простая (но в достаточной степени формальная) книга по теории множеств: Patrick Suppes, Axiomatic Set Theory. Последняя глава там как раз про Аскиому Выбора.