Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:
  • Mood:

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

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

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

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 14 comments