avva | Гёдель, полнота, терминология

Перечитывал некоторые классические статьи Гёделя (30-го и 31-го годов - о полноте и неполноте соответственно, в основном первую). Полузабавы ради перевёл аргумент статьи 30-го года (о полноте ограниченного функционального исчисления, или, на современном языке, просто логики первого порядка) в современные термины. Оказалось (нетрудным, конечно, но) на удивление муторным делом. Вообще в логике и теории множеств (по сравнению с другими дисциплинами) особенно тяжёлым делом почему-то оказывается читать статьи 60-100 летней давности. Наверное, потому, что наука только нащупывала себя, тычками наугад высекала в некоей общей ткани границу между собой и философией. Полная смена всей нотации тоже мешает, но не настолько, насколько мешает смена способа мышения.

Детская забава: пальцем водить по доказательству (в данном случае теоремы о полноте), пока не сможешь торжествующе ткнуть в строку: ага, вот здесь существенное использование аксиомы выбора, от которого не избавиться. В данном случае оно сильно замаскировано, между прочим, неявным использованием леммы Кёнига, по имени не названной.