о Гёделе и Изабелле, take 2
Aug. 31st, 2002 01:19 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avvaНаписал длинную и подробную запись о: доказательстве Гёделя от 40-го года непротиворечивости аксиомы выбора, конструктивной вселенной, V=L, и недавней формализации этого доказательства Ларри Польсоном из Кембриджа, в формальной системе Isabelle (ссылки: описание док-ва; само док-во со всеми определениями, автоматически сгенерированное, больше 200 страниц). И ещё о том, как я попытался изучить эту самую Изабеллу попристальнее, но понял, что мне не хватает адекватного понимания лямбда-исчисления (которое уже давно пора изучить, мне мешает эта дырка) и языка ML, на к-м Изабелла написана.
А ЖЖ взял да и съел мою длинную и подробную запись, и не поперхнулся. Я в шоке. Писать его заново нет сил и желания, так что пусть будет хоть это вместо него.
А ЖЖ взял да и съел мою длинную и подробную запись, и не поперхнулся. Я в шоке. Писать его заново нет сил и желания, так что пусть будет хоть это вместо него.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2002-08-30 03:55 pm (UTC)