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

[avva]

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

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