vag vagoff cнова подкинул очень интересную статью Is...

vag_vagoff cнова подкинул очень интересную статью: " Is ZF a hack? ", в которой ищется самый короткий способ формально описать основания математики для нужд автопруверов и пруф ассистантов. В качестве кандидатов исследуются: ZFC HOL Martin-Lof Type Theory Calculus of Constructions NF: Quine’s set theory of New Foundations McLarty’s axiomatization of a well-pointed topos with natural numbers and choice read more