📝 SummarXiv

Abstract

We devise a calculus of abbreviation schemes for ZF formulas. These formulas are certain words over the alphabet $$ \{x_1,\,x_2,\,\dots\}\cup \{\in,\,=,\,\neg, \,\to,\,\leftrightarrow,\,\wedge,\, \vee,\,\exists,\,\forall,\,(,\,)\} $$ and have interpretations in structures $M=\langle X,\in_M,=_M\rangle$. In them $X$ is any nonempty set, $\in_M\,\subset X\times X$ and $=_M$ is $\{\langle x,x\rangle\colon\;x\in X\}$. Using an abbreviation scheme of length 9 we produce a ZF sentence $\varphi$ with length 494 such that $\varphi$ is true in $M$ iff Cantor's theorem - for no set there is a surjection from it to its power set - holds in $M$. We prove Cantor's theorem for the family of extensive structures $M$ (which generalizes classical Cantor's theorem) and translate this result into the language of digraphs. In conclusion we discuss extension of our approach to G\"odel's completeness theorem.