Definition 6.1 — Complete matching

For every type $V$, every simple undirected loopless graph $G$ on $V$, every subgraph $M$ of $G$, and every set $S \subseteq V$, the proposition $\operatorname{CompleteMatching}(M,S)$ means precisely that every vertex belonging to the vertex set of $M$ has exactly one neighbor in $M$, and that every element of $S$ belongs to the vertex set of $M$. Here a subgraph consists of a chosen set of vertices together with a symmetric adjacency relation whose edges are edges of $G$ and whose endpoints belong to the chosen vertex set. Thus each vertex of $S$ has exactly one neighbor in $M$, and every vertex of $M$ outside $S$ must also have exactly one neighbor in $M$; the definition does not require the vertex set of $M$ to equal $S$, does not require every vertex of $G$ to belong to $M$, and does not assert the existence or uniqueness of such a subgraph. There are no finiteness, nonemptiness, decidable-equality, or bipartiteness assumptions: $V$, $S$, and the vertex set of $M$ may be finite, infinite, or empty. If $S$ is empty, the definition still requires every vertex of $M$ to have exactly one neighbor in $M$. If the vertex set of $M$ is empty, the definition holds exactly when $S$ is empty; in particular, it holds for the empty graph on an empty vertex type. No cardinality operation occurs in this definition.