Cantor digraphs and abbreviations of formulas
Martin Klazar
TL;DR
The paper reframes Cantor's theorem as a property of Cantor digraphs and constructs a ZF sentence $\varphi$ of length $|\varphi|=494$ such that, for any digraph $D$, $D\models\varphi$ iff Cantor's theorem holds in $D$. It develops a rigorous syntactic framework using ZF and ZF$'$ formulas, plus well-formed abbreviation schemes, to encode the necessary predicates (SUS, SI, SIN, DO, DOU, OPA, REL, FUN, SUR) that witness the Cantor-digraph condition. It then analyzes extensive and strongly extensive digraphs, proving Cantor's theorem in these contexts and constructing a countable strongly extensive digraph with arbitrarily large in-degrees, while also relating the results to Gödel's completeness theorem. The work provides a precise, machine-checkable encoding of a foundational set-theoretic theorem in graph-theoretic terms and advances formal methods for representing logical properties within digraphs.
Abstract
A digraph $D=\langle V,E\rangle$ ($E\subset V\times V$) is Cantor if Cantor's theorem - for no set there is a surjection from it to its power set - holds in $D$, in the sense we explain. We construct a ZF formula $\varphi$ with length $494$ such that $D\models\varphi$ iff $D$ is Cantor. In order to obtain $\varphi$, which is a word over the alphabet $$ \{x_1,\,x_2,\,\dots\}\cup \{\in,\,=,\,\neg, \,\to,\,\leftrightarrow,\,\wedge,\, \vee,\,\exists,\,\forall,\,(,\,)\}\,, $$ we devise abbreviation schemes of ZF formulas. We introduce extensive and strongly extensive digraphs and show, by the standard argument, that they are Cantor. We construct a countable strongly extensive digraph with arbitrarily large finite in-degrees.