Extension axioms for an unrestricted binary relation

For a binary relation with no symmetry or loop restrictions, an extension axiom demands a fresh element realizing any prescribed choices of incoming edges, outgoing edges and its own loop relative to a finite list of distinct parameters. All such axioms together eliminate quantifiers: the quantifier-free type of a parameter tuple determines which witness patterns can occur. These axioms differ from the undirected loop-free theory of the random graph.